Trait splr::solver::SatSolverIF
source · pub trait SatSolverIF: Instantiate {
// Required methods
fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>;
fn add_clause<V>(&mut self, vec: V) -> Result<&mut Solver, SolverError>
where V: AsRef<[i32]>;
fn add_var(&mut self) -> VarId;
fn build(config: &Config) -> Result<Solver, SolverError>;
fn reset(&mut self);
fn save_certification(&mut self);
fn dump_cnf(&self, fname: &Path);
}
Expand description
API for SAT solver creation and modification.
Required Methods§
sourcefn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>
fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>
add an assignment to Solver.
§Errors
SolverError::Inconsistent
if it conflicts with existing assignments.SolverError::InvalidLiteral
if it is out of range for var index.
§Example
use crate::splr::*;
use crate::splr::assign::VarManipulateIF; // for s.asg.assign()
use std::path::Path;
let mut s = Solver::try_from(Path::new("cnfs/uf8.cnf")).expect("can't load");
assert!(s.add_assignment(1).is_ok());
assert_eq!(s.asg.assign(1), Some(true));
assert!(s.add_assignment(2).is_ok());
assert!(s.add_assignment(3).is_ok());
assert!(s.add_assignment(4).is_ok());
assert!(s.add_assignment(5).is_ok());
assert!(s.add_assignment(8).is_ok());
assert!(matches!(s.add_assignment(-1), Err(SolverError::RootLevelConflict(_))));
assert!(matches!(s.add_assignment(10), Err(SolverError::InvalidLiteral)));
assert!(matches!(s.add_assignment(0), Err(SolverError::InvalidLiteral)));
assert_eq!(s.solve(), Ok(Certificate::SAT(vec![1, 2, 3, 4, 5, -6, 7, 8])));
sourcefn add_clause<V>(&mut self, vec: V) -> Result<&mut Solver, SolverError>
fn add_clause<V>(&mut self, vec: V) -> Result<&mut Solver, SolverError>
add a literal to Solver.
§Errors
SolverError::Inconsistent
if a given clause is unit and conflicts with existing assignments.SolverError::InvalidLiteral
if a literal in it is out of range for var index.
§Example
use crate::splr::*;
use std::path::Path;
let mut s = Solver::try_from(Path::new("cnfs/uf8.cnf")).expect("can't load");
assert!(s.add_clause(vec![1, -2]).is_ok());
assert!(s.add_clause(vec![2, -3]).is_ok());
assert!(s.add_clause(vec![3, 4]).is_ok());
assert!(s.add_clause(vec![-2, 4]).is_ok());
assert!(s.add_clause(vec![-4, 5]).is_ok());
assert!(s.add_clause(vec![-5, 6]).is_ok());
assert!(s.add_clause(vec![-7, 8]).is_ok());
assert!(matches!(s.add_clause(vec![10, 11]), Err(SolverError::InvalidLiteral)));
assert!(matches!(s.add_clause(vec![0, 8]), Err(SolverError::InvalidLiteral)));
assert_eq!(s.solve(), Ok(Certificate::UNSAT));
sourcefn add_var(&mut self) -> VarId
fn add_var(&mut self) -> VarId
add a var to solver and return the number of vars.
§Example
use crate::splr::*;
use std::path::Path;
let mut s = Solver::try_from(Path::new("cnfs/uf8.cnf")).expect("can't load");
assert_eq!(s.asg.num_vars, 8);
assert!(matches!(s.add_assignment(9), Err(SolverError::InvalidLiteral)));
s.add_assignment(1).expect("panic");
s.add_assignment(2).expect("panic");
s.add_assignment(3).expect("panic");
s.add_assignment(4).expect("panic");
s.add_assignment(5).expect("panic");
s.add_assignment(8).expect("panic");
assert_eq!(s.add_var(), 9);
assert!(s.add_assignment(-9).is_ok());
assert_eq!(s.solve(), Ok(Certificate::SAT(vec![1, 2, 3, 4, 5, -6, 7, 8, -9])));
sourcefn build(config: &Config) -> Result<Solver, SolverError>
fn build(config: &Config) -> Result<Solver, SolverError>
make a solver and load a CNF into it.
§Errors
SolverError::IOError
if it failed to load a CNF file.SolverError::Inconsistent
if the CNF is conflicting.SolverError::InvalidLiteral
if any literal used in the CNF is out of range for var index.
sourcefn reset(&mut self)
fn reset(&mut self)
reinitialize a solver for incremental solving. Requires ‘incremental_solver’ feature
sourcefn save_certification(&mut self)
fn save_certification(&mut self)
dump an UNSAT certification file
Object Safety§
This trait is not object safe.