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§

source

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])));

source

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

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));

source

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])));

source

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.

source