Struct Cdcl 

pub struct Cdcl<Config: SolverConfig = DefaultConfig> {
    pub cnf: Cnf<Config::Literal, Config::LiteralStorage>,
    /* private fields */
}

Represents a CDCL SAT solver instance.

The solver iteratively makes decisions (assigns a truth value to a variable), propagates their logical consequences, and if a conflict (a clause that becomes false under the current assignment) arises, it analyses the conflict to learn a new clause. This learned clause helps prune the search space and guide the solver towards a solution or a proof of unsatisfiability.

The solver’s behavior can be customised via the Config generic parameter, which defines the specific implementations for various components like literal representation, assignment tracking, propagation engine, variable selection heuristic, restart strategies, and clause database management.

Fields

cnf: Cnf<Config::Literal, Config::LiteralStorage>

The Conjunctive Normal Form (CNF) formula being solved. This stores both the original clauses provided by the user and clauses learned by the solver during conflict analysis.

Implementations

impl<Config: SolverConfig> Cdcl<Config>

pub const fn all_assigned(&self) -> bool

Checks if all variables in the CNF have been assigned a truth value.

The number of variables is determined by self.cnf.num_vars, which typically corresponds to the highest variable index used in the problem + 1. The trail length (self.trail.len()) reflects the number of currently assigned literals.

Returns

true if the number of assigned literals in the trail equals the total number of variables considered by the solver, false otherwise.

pub fn add_clause( &mut self, clause: Clause<Config::Literal, Config::LiteralStorage>, )

Adds a new clause to the solver’s CNF database.

Clauses that are empty (and thus trivially unsatisfiable if encountered this way) or tautological (e.g. (x OR -x OR y)) are typically ignored as they provide no useful constraints or can be simplified. The new clause is added to the Cnf store and then registered with the Propagator (e.g. for setting up watched literals).

Arguments

• clause: The clause to add.

Trait Implementations

impl<Config: Clone + SolverConfig> Clone for Cdcl<Config>

where Config::Assignment: Clone, Config::Propagator: Clone, Config::Literal: Clone, Config::LiteralStorage: Clone, Config::VariableSelector: Clone, Config::Restarter: Clone, Config::ClauseManager: Clone,

fn clone(&self) -> Cdcl<Config>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<Config: Debug + SolverConfig> Debug for Cdcl<Config>

where Config::Assignment: Debug, Config::Propagator: Debug, Config::Literal: Debug, Config::LiteralStorage: Debug, Config::VariableSelector: Debug, Config::Restarter: Debug, Config::ClauseManager: Debug,

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

Formats the value using the given formatter.

impl<Config: SolverConfig> Solver<Config> for Cdcl<Config>

fn new<L: Literal, S: LiteralStorage<L>>(cnf: Cnf<L, S>) -> Self

Creates a new Cdcl solver instance for the given CNF formula.

Initialises all internal components of the solver:

• Assignment: To store variable assignments (initialised to Undefined).
• Trail: To track decisions and propagations.
• Propagator: Set up with the initial clauses for watched literal schemes.
• Cnf: Stores the clauses of the problem.
• VariableSelector: Initialised with variable information (e.g. for VSIDS).
• Restarter: Initialised with default restart strategy parameters.
• Analyser: For conflict analysis.
• ClauseManager: For managing learned clauses. The decision level is initialised to 0.

Arguments

• cnf: The Conjunctive Normal Form (CNF) formula to be solved.

fn solve(&mut self) -> Option<Solutions>

Attempts to solve the SAT problem for the loaded CNF formula using the CDCL algorithm.

The main loop proceeds as follows:

1. Initial Check & Propagation:

   • If the CNF is empty, it’s trivially SAT.
   • Perform initial unit propagation (BCP) at decision level 0. If a conflict occurs, the formula is UNSAT.
   • If any clause becomes empty (after initial setup or propagation), formula is UNSAT.

2. Main Loop: a. Propagation: Propagate assignments based on the current partial assignment.

   • If propagation leads to a conflict (a clause becomes falsified): i. Notify ClauseManager about the conflict (e.g. to adjust clause activities). ii. Perform ConflictAnalysis:

     • Generate a learned clause (lemma).
       • Determine variables involved for activity bumping (e.g. VSIDS).

     iii. Handle the conflict result:

     • Conflict::Ground: Conflict at level 0 implies the formula is UNSAT.
       • Conflict::Restart or Conflict::Unit: These might also indicate UNSAT or special handling.
       • Conflict::Learned(assert_idx, learned_clause):
         • The learned clause is processed (e.g. LBD calculation, activity bump).
         • Determine backtrack level (bt_level) from the learned clause.
         • Bump activities of clauses involved in the conflict.
         • Backtrack: Undo assignments on the trail up to bt_level. Update decision_level.
         • Add the learned clause to the database.
         • Enqueue the asserting literal from the learned clause for propagation.
         • Optionally, clean the clause database (manager.clean_clause_db).

     iv. Update variable selection heuristics (selector.bumps, selector.decay). v. Check for restart (should_restart). If so, reset trail, assignments, and decision level.

   b. Decision (No Conflict): i. Increment decision_level. ii. Check if all variables are assigned (all_assigned). If yes, a model is found; return SAT. iii. Select an unassigned variable using selector.pick().

   • If a literal is picked, push it onto the trail as a decision.
     • If no literal can be picked (e.g. all assigned but all_assigned was false, or selector gives up), it might imply a solution is found (though all_assigned should be the primary check). Return current solutions.

The loop continues until a satisfying assignment is found (returns Some(Solutions)) or the formula is proven unsatisfiable (returns None).

Returns

• Some(Solutions): If a satisfying assignment is found. Contains the model.
• None: If the formula is unsatisfiable.

fn solutions(&self) -> Solutions

Retrieves the current satisfying assignment if one has been found.

This method should typically be called after solve() returns Some(_). If called before solving, or if the formula is unsatisfiable, the returned assignment might be incomplete, empty, or reflect some intermediate state. The Solutions object usually maps variable indices to their truth values.

Returns

A Solutions object representing the variable assignments in a model.

fn stats(&self) -> SolutionStats

Gathers statistics about the solving process.

These statistics can be useful for analysing solver performance and heuristics.

Returns

A SolutionStats struct containing:

• conflicts: Total number of conflicts encountered.
• decisions: Total number of decisions made.
• propagations: Total number of propagations performed.
• restarts: Total number of restarts performed.
• learnt_clauses: Number of clauses currently in the learnt clause database.
• removed_clauses: Number of learnt clauses removed during database cleaning.

fn debug(&mut self)

Placeholder for a debugging function.

This function is intended for future use, possibly to print internal solver state or enable more verbose logging for debugging purposes. Currently, it is unimplemented.

fn from_parts<L: Literal, S: LiteralStorage<L>>( cnf: Cnf<L, S>, assignment: Config::Assignment, manager: Config::ClauseManager, propagator: Config::Propagator, restarter: Config::Restarter, selector: Config::VariableSelector, ) -> Self

Creates a solver instance from its components.