Struct screwsat::solver::Solver

pub struct Solver {
    pub models: Vec<LitBool>,
    pub status: Option<Status>,
    // some fields omitted
}

Fields

models: Vec<LitBool>

status: Option<Status>

Implementations

impl Solver

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

Create a new Solver struct

Arguments

• n - The number of variable
• clauses - All clauses that solver solves

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.

Arguments

• clause - a clause has one or some literal variables

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

Reserve the space of a clause database

Arguments

• cla_num - The number of clause

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

Arguments

• var_num - The number of variable

pub fn solve(&mut self, time_limit: Option<Duration>) -> Status

Solve a problem and return a enum Status.

Arguments

• time_limit - The time limitation for searching. Exceeding the time limit returns Indeterminate

Trait Implementations

impl Debug for Solver

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

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Solver

Returns the "default value" for a type.