[−][src]Trait splr::SatSolverIF

pub trait SatSolverIF {
    pub fn add_assignment(
        &mut self, 
        val: i32
    ) -> Result<&mut Solver, SolverError>;

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

    pub fn add_var(&mut self) -> usize;

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

    pub fn reset(&mut self);
}

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]

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

Loading content...

Implementors

impl SatSolverIF for Solver[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());
Loading content...