Struct Dpll 

pub struct Dpll<Config: SolverConfig + Clone = DefaultConfig> {
    pub trail: Trail<Config::Literal, Config::LiteralStorage>,
    pub assignment: Config::Assignment,
    pub decision_level: DecisionLevel,
    pub cnf: Cnf<Config::Literal, Config::LiteralStorage>,
    pub selector: Config::VariableSelector,
    pub propagator: Config::Propagator,
}

Represents a DPLL SAT solver.

This struct encapsulates the state of the solver, including the CNF formula, current assignment, decision level, and components for propagation and variable selection. It is generic over Config, which defines the specific types and strategies used by the solver.

Fields

trail: Trail<Config::Literal, Config::LiteralStorage>

The trail of assignments and decisions made by the solver. It’s used by the propagator to manage assignments and detect conflicts.

assignment: Config::Assignment

The current assignment of truth values to variables.

decision_level: DecisionLevel

The current decision level in the DPLL search tree. Incremented each time a new variable is chosen for branching.

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

The Conjunctive Normal Form (CNF) formula being solved.

selector: Config::VariableSelector

The variable selection heuristic. Used to pick the next unassigned variable for a decision.

propagator: Config::Propagator

The unit propagator. Responsible for performing unit propagation based on the current assignment.

Trait Implementations

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

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

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<Config: Debug + SolverConfig + Clone> Debug for Dpll<Config>

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

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

Formats the value using the given formatter.

impl<Config: SolverConfig + Clone> Solver<Config> for Dpll<Config>

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

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

Arguments

• cnf: The CNF formula to be solved.

Returns

A new Dpll instance initialised with the provided formula and default components (propagator, assignment tracker, trail, variable selector) based on the Config.

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

Attempts to solve the SAT formula.

This method implements the core DPLL algorithm:

1. It first performs unit propagation (self.propagate()).
2. Then, it checks if the formula is already satisfied (self.is_sat()). If so, it returns the current assignment.
3. It checks if the formula is unsatisfiable (self.is_unsat()) due to a conflict. If so, it returns None.
4. If the formula is neither satisfied nor unsatisfiable, it selects an unassigned variable using self.selector.pick().
5. It increments the decision level.
6. It creates two branches: one where the chosen variable is assigned true, and one where it’s assigned false. These branches are explored recursively by calling solve() on cloned solver states.
7. If the ‘true’ branch finds a solution, it’s returned.
8. Otherwise, if the ‘false’ branch finds a solution, it’s returned.
9. If neither branch finds a solution, the formula is unsatisfiable from the current state, and None is returned.

Returns

• Some(Solutions): If the formula is satisfiable, containing the satisfying assignment.
• None: If the formula is unsatisfiable.

fn solutions(&self) -> Solutions

Returns the current satisfying assignment if the formula is SAT.

This method should typically be called after solve() returns Some(...). It retrieves the model (variable assignments) from the assignment component. Variables not assigned a value in the model might be “don’t care” variables.

fn stats(&self) -> SolutionStats

Returns statistics about the solving process.

Note: Some statistics, like propagations, might be estimations or specific to this simple DPLL implementation rather than a general count of propagation steps. conflicts, restarts, learnt_clauses, removed_clauses are currently placeholders.

fn debug(&mut self)

Placeholder for a debugging function.

Currently, this function is not implemented and will panic if called.

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.