Struct screwsat::screwsat::Solver

pub struct Solver {
    pub assigns: Vec<bool>,
    // some fields omitted
}

Fields

assigns: Vec<bool>

Implementations

impl Solver

pub fn enqueue(&mut self, var: Var, assign: bool, reason: Option<usize>)

Enqueue a variable to assign a value to a boolean assign

pub fn new_var(&mut self)

pub fn add_clause(&mut self, clause: &[Lit])

Add a new clause to clauses and watch a clause. If a variable is greater than the size of array, grow it.

pub fn new(n: usize, clauses: &[Vec<Lit>]) -> Solver

pub fn reserve_clause(&mut self, cla_num: usize)

pub fn reserve_variable(&mut self, var_num: usize)

pub fn solve(&mut self, msec: Option<u64>) -> Status

Solve a problem and return true if solver finds a SATISFIABLE assignments false if solver finds a given problem is UNSATISFIABLE or reach the time limit

Trait Implementations

impl Debug for Solver

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

Formats the value using the given formatter.

impl Default for Solver

pub fn default() -> Solver

Returns the "default value" for a type.