Struct Solver 

pub struct Solver { /* private fields */ }

CDCL SAT Solver

Implementations

impl Solver

pub fn new() -> Self

Create a new solver

pub fn with_config(config: SolverConfig) -> Self

Create a new solver with configuration

pub fn new_var(&mut self) -> Var

Create a new variable

pub fn ensure_vars(&mut self, n: usize)

Ensure we have at least n variables

pub fn add_clause(&mut self, lits: impl IntoIterator<Item = Lit>) -> bool

Add a clause

pub fn add_clause_dimacs(&mut self, lits: &[i32]) -> bool

Add a clause from DIMACS literals

pub fn solve(&mut self) -> SolverResult

Solve the SAT problem

pub fn solve_with_assumptions( &mut self, assumptions: &[Lit], ) -> (SolverResult, Option<Vec<Lit>>)

Solve with assumptions and return unsat core if UNSAT

This is the key method for MaxSAT: it solves under assumptions and if the result is UNSAT, returns the subset of assumptions in the core.

Arguments

• assumptions - Literals that must be true

Returns

• (SolverResult, Option<Vec<Lit>>) - Result and unsat core (if UNSAT)

pub fn solve_with_theory<T: TheoryCallback>( &mut self, theory: &mut T, ) -> SolverResult

Solve with theory integration via callbacks

This implements the CDCL(T) loop:

1. BCP (Boolean Constraint Propagation)
2. Theory propagation (via callback)
3. On conflict: analyze and learn
4. Decision
5. Final theory check when all vars assigned

pub fn model(&self) -> &[LBool]

Get the model (if sat)

pub fn model_value(&self, var: Var) -> LBool

Get the value of a variable in the model

pub fn stats(&self) -> &SolverStats

Get statistics

pub fn memory_opt_stats(&self) -> &MemoryOptStats

Get memory optimizer statistics

pub fn num_vars(&self) -> usize

Get number of variables

pub fn num_clauses(&self) -> usize

Get number of clauses

pub fn push(&mut self)

Push a new assertion level (for incremental solving)

This saves the current state so that clauses added after this point can be removed with pop(). Automatically backtracks to decision level 0 to ensure a clean state for adding new constraints.

pub fn pop(&mut self)

Pop to previous assertion level

pub fn backtrack_to_root(&mut self)

Backtrack to decision level 0 (for AllSAT enumeration)

This is necessary after a SAT result before adding blocking clauses to ensure the new clauses can trigger propagation correctly. Uses phase-saving backtrack to properly re-insert unassigned variables into the decision heaps (VSIDS, CHB, LRB).

pub fn reset(&mut self)

Reset the solver

pub fn trail(&self) -> &Trail

Get the current trail (for theory solvers)

pub fn decision_level(&self) -> u32

Get the current decision level

pub fn debug_print_learned_clauses(&self)

Debug method: print all learned clauses

pub fn debug_print_binary_graph(&self)

Debug method: print binary implication graph entries

Trait Implementations

impl Debug for Solver

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Self

Returns the “default value” for a type.