Struct Solver 

pub struct Solver { /* private fields */ }

The CDCL solver.

Implementations

impl Solver

pub fn new(num_vars: usize) -> Self

A fresh solver over num_vars variables and no clauses.

pub fn subsume(&mut self) -> bool

Run one subsumption + self-subsuming-resolution round over the learned clauses (Phase 4 inprocessing). Returns false if it proves the formula UNSAT. Verdict-invariant.

pub fn subsumptions(&self) -> u64

Learned clauses deleted or strengthened by subsumption during this solver’s life.

pub fn set_inprocess(&mut self, on: bool)

Enable or disable the between-restart inprocessing schedule (default on). For A/B benchmarking; verdict-invariant either way.

pub fn set_inprocess_interval(&mut self, conflicts: u64)

Set the conflict interval between inprocessing rounds (default [INPROCESS_INTERVAL]). Tuning / test knob; verdict-invariant.

pub fn vivify(&mut self) -> bool

Run one vivification round over the learned clauses, strengthening each shortenable clause in place (Phase 2 inprocessing). Returns false if vivification proves the formula UNSAT. Verdict-invariant; intended to be scheduled at decision level 0 between restarts.

pub fn vivifications(&self) -> u64

Learned clauses strengthened by vivification during this solver’s life. Pure observability.

pub fn probe(&mut self) -> bool

Run one failed-literal probing round (Phase 3 inprocessing): try each phase of each free variable as a level-0 assumption; if propagation conflicts, the opposite literal is a forced unit, learned permanently. Returns false if probing proves the formula UNSAT. Verdict-invariant; scheduled at decision level 0.

pub fn probes(&self) -> u64

Units derived by failed-literal probing during this solver’s life. Pure observability.

pub fn set_restart_mode(&mut self, mode: RestartMode)

Select the restart heuristic (default RestartMode::Glucose). Search-order only — a verdict is unaffected, so this is for A/B tuning.

pub fn restart_mode(&self) -> RestartMode

The restart heuristic in force.

pub fn blocked_restarts(&self) -> u64

Restarts suppressed by Glucose blocking during the last solve.

pub fn set_decision_vars(&mut self, vars: &[usize])

Restrict branching to vars (DPLL(XOR): the engine’s non-pivot variables; the theory forces the rest). A model is still complete because theory propagation assigns every excluded variable before all decision variables are exhausted.

pub fn conflicts(&self) -> u64

Total conflicts during the last solve — the search-work metric.

pub fn decisions(&self) -> u64

Total decisions during the last solve.

pub fn propagations(&self) -> u64

Total BCP propagations during the last solve — the throughput metric.

pub fn restarts(&self) -> u64

Total restarts during the last solve.

pub fn set_reduce(&mut self, on: bool)

Enable or disable LBD-based learned-clause deletion (default on). For A/B benchmarking.

pub fn set_reduce_limit(&mut self, limit: usize)

Set the live-learned-clause count that triggers a reduction (tuning / stress-testing).

pub fn set_initial_phase(&mut self, phases: &[bool])

Seed the saved-phase polarities (the order decisions try first) from an external assignment. Purely a search-order hint — it never changes which models exist, so it cannot affect the verdict — but starting decisions on, e.g., a GF(2)-consistent assignment lets the hybrid XOR route begin on the linear system’s solution manifold and only repair the residual clauses.

pub fn live_learned(&self) -> usize

The number of learned clauses currently live in the database (originals excluded).

pub fn learned(&self) -> &[LearnedClause]

The learned clauses produced during the last solve (the DRAT/LRAT proof skeleton).

pub fn original_clauses(&self) -> &[Vec<Lit>]

The ORIGINAL clauses (those present before solving), borrowed in place — so a RUP checker can replay over them without copying the clause set.

pub fn add_clause(&mut self, lits: Vec<Lit>)

Add a clause. An empty clause makes the formula trivially unsatisfiable; a unit clause is enqueued as a top-level fact.

pub fn solve(&mut self) -> SolveResult

Solve, optionally under a list of theory propagators (DPLL(T)). Returns a model or Unsat. The learned-clause log is available afterwards via Solver::learned.

pub fn solve_budgeted(&mut self, max_conflicts: u64) -> BudgetedResult

Solve but give up after max_conflicts conflicts, returning BudgetedResult::Budget with the learned clauses (Self::learned) intact — the hook dynamic symmetry breaking needs to interleave bounded search with symmetric clause amplification. A max_conflicts of 0 means unlimited (equivalent to Self::solve).

pub fn solve_with(&mut self, theories: &mut [Box<dyn Theory>]) -> SolveResult

Solve with theory propagators. Each is consulted at every Boolean fixpoint; a returned clause is added to the formula (and may immediately propagate or conflict).

pub fn solve_under_assumptions(&mut self, assumptions: &[Lit]) -> SolveResult

Solve under temporary assumptions (literals forced true for THIS query only), reusing every clause learned so far. The permanent clause database is untouched, so a later call with different assumptions may well be satisfiable — successive queries on the same solver (e.g. BMC at increasing depths) amortise learning. This is the incremental-SAT (IPASIR) pattern. Unsat here means “unsatisfiable UNDER these assumptions”.

Soundness of reuse: conflict analysis keeps decision-level literals (assumptions are decisions) and drops level-0 facts, so each learned clause is a consequence of the PERMANENT clauses alone — valid no matter which assumptions a future query makes.

Restarts are disabled in this path: the assumptions occupy the bottom decision levels, and skipping restarts keeps them pinned without a restart-floor dance. The small, bounded queries this serves do not need restarts; correctness beats the heuristic. (Does not touch n_original; do not mix with Solver::original_clauses/RUP on the same solver.)