Skip to main content

SatSolver

sat_interface

Trait SatSolver 

Source 
pub trait SatSolver: AddConstraints<Clause> + AddConstraints<Formula> {
    type Status: SolverState;

    // Required methods
    fn new() -> Self;
    fn solve(&mut self) -> Self::Status;
    fn val(&mut self, lit: i32) -> bool;
    fn load_model(&mut self) -> Model;
    fn block_model(&mut self);
}
Expand description

This trait captures the interface of a SAT solver.

Its trait constraints require that its implementation is able to add clauses and formulas as constraints.

Required Associated Types§

Source

type Status: SolverState

Required Methods§

Source

fn new() -> Self

Create a new SAT solver

Source

fn solve(&mut self) -> Self::Status

Decide whether current constraints are satisfiable or not

Source

fn val(&mut self, lit: i32) -> bool

After Self::solve returns sat, query the solver for the boolean value of the SAT variable lit.

Requirement: lit must be a SAT variable present in the constraints.

Source

fn load_model(&mut self) -> Model

After Self::solve returns sat, obtain the full model.

Source

fn block_model(&mut self)

After Self::solve returns sat, block the current model. It is useful for model enumeration.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§