Trait Solver

Source

pub trait Solver<C: SolverConfig = DefaultConfig> {
    // Required methods
    fn new<L: Literal, S: LiteralStorage<L>>(cnf: Cnf<L, S>) -> Self;
    fn from_parts<L: Literal, S: LiteralStorage<L>>(
        cnf: Cnf<L, S>,
        assignment: C::Assignment,
        manager: C::ClauseManager,
        propagator: C::Propagator,
        restarter: C::Restarter,
        selector: C::VariableSelector,
    ) -> Self;
    fn solve(&mut self) -> Option<Solutions>;
    fn solutions(&self) -> Solutions;
    fn stats(&self) -> SolutionStats;
    fn debug(&mut self);
}

Expand description

A trait that defines the general interface for a SAT solver.

This trait is generic over a configuration C which must implement SolverConfig. This allows different solver implementations to adhere to a common API while being configurable with various underlying strategies and data structures.

Required Methods§

Source

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

Creates a new instance of the solver, initialised with the given CNF formula.

§Arguments

cnf: The Cnf formula to be solved.

Source

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

Creates a solver instance from its components.

§Arguments

cnf: The Cnf formula to be solved.
assignment: The assignment data structure.
manager: The clause management scheme.
propagator: The unit propagation scheme.
restarter: The restart strategy.
selector: The variable selection strategy.

Source

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

Attempts to solve the CNF formula provided at construction.

§Returns

Some(Solutions) if a satisfying assignment (model) is found.
None if the formula is determined to be unsatisfiable.

Source

fn solutions(&self) -> Solutions

Returns the current satisfying assignment if one has been found.

If solve() has not been called, or if it returned None (unsatisfiable), the returned Solutions object might be empty or reflect some solver-internal state. It’s typically called after solve() returns Some.

Source