Struct splr::solver::Solver

pub struct Solver {
    pub asg: AssignStack,
    pub cdb: ClauseDB,
    pub state: State,
}

The SAT solver object consisting of 6 sub modules.

use crate::splr::*;
use crate::splr::{assign::{AssignIF, VarManipulateIF}, state::{State, StateIF}, types::*};
use std::path::Path;

let mut s = Solver::try_from(Path::new("cnfs/sample.cnf")).expect("can't load");
assert_eq!(s.asg.derefer(assign::property::Tusize::NumVar), 250);
assert_eq!(s.asg.derefer(assign::property::Tusize::NumUnassertedVar), 250);
if let Ok(Certificate::SAT(v)) = s.solve() {
    assert_eq!(v.len(), 250);
    // But don't expect `s.asg.var_stats().3 == 0` at this point.
    // It returns the number of vars which were assigned at decision level 0.
} else {
    panic!("It should be satisfied!");
}
assert_eq!(Solver::try_from(Path::new("cnfs/unsat.cnf")).expect("can't load").solve(), Ok(Certificate::UNSAT));

Fields

asg: AssignStack

assignment management

cdb: ClauseDB

clause container

state: State

misc data holder

Trait Implementations

impl Clone for Solver

fn clone(&self) -> Solver

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Solver

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

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Solver

Returns the “default value” for a type.

impl Instantiate for Solver

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

use crate::{splr::config::Config, splr::types::*};
use splr::solver::Solver;
let s = Solver::instantiate(&Config::default(), &CNFDescription::default());

fn handle(&mut self, _e: SolverEvent)

update by a solver event.

impl SatSolverIF for Solver

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

Examples

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

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

fn save_certification(&mut self)

dump an UNSAT certification file

fn dump_cnf(&self, fname: &Path)

dump all active clauses and assertions as a CNF file.

fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>

add an assignment to Solver.

fn add_clause<V>(&mut self, vec: V) -> Result<&mut Solver, SolverError>where V: AsRef<[i32]>,

add a literal to Solver.

fn add_var(&mut self) -> VarId

add a var to solver and return the number of vars.

fn reset(&mut self)

reinitialize a solver for incremental solving. Requires ‘incremental_solver’ feature

impl SolveIF for Solver

fn solve(&mut self) -> SolverResult

Examples

use splr::*;

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

impl TryFrom<&Path> for Solver

fn try_from(s: &Path) -> Result<Self, Self::Error>

return a new solver build for a CNF file.

Example

use crate::splr::solver::{SatSolverIF, Solver};
use std::path::Path;

let mut s = Solver::try_from(Path::new("cnfs/sample.cnf")).expect("fail to load");

type Error = SolverError

The type returned in the event of a conversion error.

impl<V> TryFrom<(Config, &[V])> for Solverwhere V: AsRef<[i32]>,

Example

 use crate::splr::*;

 let v: Vec<Vec<i32>> = vec![];
 assert!(matches!(
     Solver::try_from((Config::default(), v.as_ref())),
     Ok(_)
 ));
 assert!(matches!(
     Solver::try_from((Config::default(), vec![vec![0_i32]].as_ref())),
     Err(Err(SolverError::InvalidLiteral))
 ));

type Error = Result<Certificate, SolverError>

The type returned in the event of a conversion error.

fn try_from((config, vec): (Config, &[V])) -> Result<Self, Self::Error>

Performs the conversion.

impl ValidateIF for Solver

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

inject an assignment set into solver. An assignment set is represented by a list of i32.

#Example

use crate::{splr::config::Config, splr::types::*};
use splr::solver::{Solver, ValidateIF};

let cnf = CNFDescription {
        num_of_variables: 4,
        ..CNFDescription::default()
    };
let mut s = Solver::instantiate(&Config::default(), &cnf);
assert_eq!(s.inject_assignment(&[1i32, -2, 3]), Ok(()));

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.

#Example

use crate::{splr::config::Config, splr::types::*};
use splr::solver::{Solver, ValidateIF};

let cnf = CNFDescription {
        num_of_variables: 4,
        ..CNFDescription::default()
    };
let mut s = Solver::instantiate(&Config::default(), &cnf);
s.inject_assignment(&[1i32, -2, 3]);
assert_eq!(s.validate(), None);