Struct SatisfiabilityChecker 

pub struct SatisfiabilityChecker {
    pub n_vars: usize,
    pub clauses: Vec<Vec<Literal>>,
}

A propositional formula in Conjunctive Normal Form (CNF).

Clauses are disjunctions; the formula is the conjunction of all clauses.

Fields

n_vars: usize

Number of propositional variables.

clauses: Vec<Vec<Literal>>

CNF clauses.

Implementations

impl SatisfiabilityChecker

pub fn new(n_vars: usize) -> Self

Create an empty SAT checker with n_vars variables.

pub fn add_clause(&mut self, clause: Vec<Literal>)

Add a clause (disjunction of literals).

pub fn solve(&self) -> Option<Vec<bool>>

Check satisfiability using the DPLL algorithm.

Returns Some(assignment) where assignment\[i\] is the truth value for variable i, or None if unsatisfiable.

pub fn check_assignment(&self, assignment: &[bool]) -> bool

Check whether the given assignment satisfies all clauses.

pub fn clause_count(&self) -> usize

Return the number of clauses.

Trait Implementations

impl Clone for SatisfiabilityChecker

fn clone(&self) -> SatisfiabilityChecker

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SatisfiabilityChecker

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

Formats the value using the given formatter.