[−][src]Trait splr::SatSolverIF
API for SAT solver creation and modification.
Required methods
pub fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>
[src]
add an assignment to Solver.
Errors
SolverError::Inconsistent
if it conflicts with existing assignments.SolverError::OutOfRange
if it is out of range for var index.
Example
use crate::splr::*; use std::convert::TryFrom; use crate::splr::assign::VarManipulateIF; // for s.asg.assign() let mut s = Solver::try_from("tests/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::Inconsistent))); assert!(matches!(s.add_assignment(10), Err(SolverError::OutOfRange))); assert!(matches!(s.add_assignment(0), Err(SolverError::OutOfRange))); assert_eq!(s.solve(), Ok(Certificate::SAT(vec![1, 2, 3, 4, 5, -6, 7, 8])));
pub fn add_clause<V>(&mut self, vec: V) -> Result<&mut Solver, SolverError> where
V: AsRef<[i32]>,
[src]
V: AsRef<[i32]>,
add a literal to Solver.
Errors
SolverError::Inconsistent
if a given clause is unit and conflicts with existing assignments.SolverError::OutOfRange
if a literal in it is out of range for var index.
Example
use crate::splr::*; use std::convert::TryFrom; let mut s = Solver::try_from("tests/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::OutOfRange))); assert!(matches!(s.add_clause(vec![0, 8]), Err(SolverError::OutOfRange))); assert_eq!(s.solve(), Ok(Certificate::UNSAT));
pub fn add_var(&mut self) -> usize
[src]
add a var to solver and return the number of vars.
Example
use crate::splr::*; use std::convert::TryFrom; let mut s = Solver::try_from("tests/uf8.cnf").expect("can't load"); assert_eq!(s.asg.num_vars, 8); assert!(matches!(s.add_assignment(9), Err(SolverError::OutOfRange))); 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])));
pub fn build(config: &Config) -> Result<Solver, SolverError>
[src]
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::OutOfRange
if any literal used in the CNF is out of range for var index.
pub fn reset(&mut self)
[src]
reinitialize a solver for incremental solving. Requires 'incremental_solver' feature
Implementors
impl SatSolverIF for Solver
[src]
pub fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>
[src]
pub fn add_clause<V>(&mut self, vec: V) -> Result<&mut Solver, SolverError> where
V: AsRef<[i32]>,
[src]
V: AsRef<[i32]>,
pub fn add_var(&mut self) -> usize
[src]
pub fn build(config: &Config) -> Result<Solver, SolverError>
[src]
Examples
use splr::config::Config; use splr::solver::{SatSolverIF, Solver}; let config = Config::from("tests/sample.cnf"); assert!(Solver::build(&config).is_ok());