Struct splr::solver::Solver

pub struct Solver {
    pub asgs: AssignStack,
    pub cdb: ClauseDB,
    pub elim: Eliminator,
    pub state: State,
    pub vdb: VarDB,
}

SAT solver consisting of 5 sub modules.

Fields

asgs: AssignStack

cdb: ClauseDB

elim: Eliminator

state: State

vdb: VarDB

Trait Implementations

impl SatSolverIF for Solver

fn new(config: &Config, cnf: &CNFDescription) -> Solver

make a solver for debug. Probably you should use build instead of this.

fn solve(&mut self) -> SolverResult

Examples

use splr::traits::SatSolverIF;
use splr::config::Config;
use splr::solver::{Solver, Certificate};

let config = Config::from("tests/sample.cnf");
if let Ok(mut s) = Solver::build(&config) {
    let res = s.solve();
    assert!(res.is_ok());
    assert_ne!(res.unwrap(), Certificate::UNSAT);
}

fn build(config: &Config) -> Result<Solver>

Examples

use splr::traits::SatSolverIF;
use splr::config::Config;
use splr::solver::Solver;

let config = Config::from("tests/sample.cnf");
assert!(Solver::build(&config).is_ok());

fn add_unchecked_clause(&mut self, v: &mut Vec<Lit>) -> Option<ClauseId>

add a vector of Lit as a clause to the solver.

impl ValidatorIF for Solver

fn inject_assigmnent(&mut self, vec: &[i32]) -> MaybeInconsistent

load a assignment set into solver.

fn validate(&self) -> Option<Vec<i32>>

returns None if the given assignment is a model of a problem. Otherwise returns a clause which is not satisfiable under a given assignment.

impl Debug for Solver

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

Formats the value using the given formatter.