scuttle_core/
lib.rs

1//! # Scuttle
2//!
3//! A multi-objective MaxSAT solver with multiple algorithms implemented.
4#![feature(try_trait_v2)]
5
6use std::fmt;
7
8use rustsat::solvers::{SolverResult, SolverStats};
9
10pub mod options;
11pub use options::{CoreBoostingOptions, KernelOptions, Limits};
12
13pub mod types;
14use types::NonDomPoint;
15
16pub mod prepro;
17
18pub mod algs;
19pub use algs::{
20    CoreBoost, Init, InitCert, InitCertDefaultBlock, InitDefaultBlock, KernelFunctions, Solve,
21};
22
23// Reexport algorithms
24pub use algs::bioptsat::BiOptSat;
25pub use algs::lowerbounding::LowerBounding;
26pub use algs::pminimal::PMinimal;
27
28pub(crate) mod termination;
29pub use termination::MaybeTerminated;
30pub use termination::MaybeTerminatedError;
31pub use termination::Termination;
32
33/// Trait for getting statistics from the solver
34pub trait ExtendedSolveStats {
35    /// Gets statistics from the internal oracle
36    fn oracle_stats(&self) -> SolverStats;
37    /// Gets statistics from the objective encodings
38    fn encoding_stats(&self) -> Vec<EncodingStats>;
39}
40
41/// Algorithm phases that the solver can be in
42#[derive(Clone, Copy, Debug, PartialEq, Eq)]
43pub enum Phase {
44    /// Outer loop
45    OuterLoop,
46    /// $P$-minimization of a model
47    Minimization,
48    /// Enumeration of solutions at a Pareto point
49    Enumeration,
50    /// Linsu sub algorithm
51    Linsu,
52}
53
54impl fmt::Display for Phase {
55    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
56        match self {
57            Phase::OuterLoop => write!(f, "outer-loop"),
58            Phase::Minimization => write!(f, "minimization"),
59            Phase::Enumeration => write!(f, "enumeration"),
60            Phase::Linsu => write!(f, "linsu"),
61        }
62    }
63}
64
65/// Statistics of the solver
66#[derive(Debug, PartialEq, Eq, Clone, Copy, Default)]
67pub struct Stats {
68    /// The number of calls to [`Solve::solve`]
69    pub n_solve_calls: usize,
70    /// The number of Pareto-optimal solutions found
71    pub n_solutions: usize,
72    /// The number of non-dominated points found
73    pub n_non_dominated: usize,
74    /// The number of candidates explored
75    pub n_candidates: usize,
76    /// The number of calls to the SAT oracle
77    pub n_oracle_calls: usize,
78    /// The number of objectives in the solver
79    pub n_objs: usize,
80    /// The number of non-constant objectives in the solver
81    pub n_real_objs: usize,
82    /// The number of original clauses
83    pub n_orig_clauses: usize,
84}
85
86/// Statistics of a used cardinality or pseudo-boolean encodings
87#[derive(Debug, PartialEq, Eq, Clone, Copy, Default)]
88pub struct EncodingStats {
89    /// The number of clauses in the encoding
90    pub n_clauses: usize,
91    /// The number of variables in the encoding
92    pub n_vars: u32,
93    /// The objective offset
94    pub offset: isize,
95    /// The unit weight, if the objective is unweighted
96    pub unit_weight: Option<usize>,
97}
98
99/// A logger to attach to a solver
100pub trait WriteSolverLog {
101    /// Adds a candidate cost point to the log
102    fn log_candidate(&mut self, costs: &[usize], phase: Phase) -> anyhow::Result<()>;
103    /// Adds an oracle call to the log
104    fn log_oracle_call(&mut self, result: SolverResult) -> anyhow::Result<()>;
105    /// Adds a solution to the log
106    fn log_solution(&mut self) -> anyhow::Result<()>;
107    /// Adds a non-dominated point to the log
108    fn log_non_dominated(&mut self, pareto_point: &NonDomPoint) -> anyhow::Result<()>;
109    #[cfg(feature = "sol-tightening")]
110    /// Adds a heuristic objective improvement to the log
111    fn log_heuristic_obj_improvement(
112        &mut self,
113        obj_idx: usize,
114        apparent_cost: usize,
115        improved_cost: usize,
116    ) -> anyhow::Result<()>;
117    /// Adds a fence change in the lower-bounding algorithm to the log
118    fn log_fence(&mut self, fence: &[usize]) -> anyhow::Result<()>;
119    /// Adds a new routine starting to the log
120    fn log_routine_start(&mut self, desc: &'static str) -> anyhow::Result<()>;
121    /// Adds a new routine ending to the log
122    fn log_routine_end(&mut self) -> anyhow::Result<()>;
123    /// Adds end of solving to the log
124    fn log_end_solve(&mut self) -> anyhow::Result<()>;
125    /// Adds an updated ideal point to the log
126    fn log_ideal(&mut self, ideal: &[usize]) -> anyhow::Result<()>;
127    /// Adds an updated nadir point to the log
128    fn log_nadir(&mut self, nadir: &[usize]) -> anyhow::Result<()>;
129    /// Adds an extracted core to the log
130    fn log_core(&mut self, weight: usize, len: usize, red_len: usize) -> anyhow::Result<()>;
131    /// Adds a core exhaustion to the log
132    fn log_core_exhaustion(&mut self, exhausted: usize, weight: usize) -> anyhow::Result<()>;
133    /// Adds an inprocessing step to the log
134    fn log_inprocessing(
135        &mut self,
136        cls_before_after: (usize, usize),
137        fixed_lits: usize,
138        obj_range_before_after: Vec<(usize, usize)>,
139    ) -> anyhow::Result<()>;
140    /// Logs any string
141    fn log_message(&mut self, msg: &str) -> anyhow::Result<()>;
142}
scuttle_core/lib.rs

scuttle_core/
lib.rs
