Struct SATInstance 

pub struct SATInstance {
    pub num_vars: usize,
    pub clauses: Vec<Vec<i32>>,
}

SAT instance: a propositional formula in conjunctive normal form.

Fields

num_vars: usize

Number of variables.

clauses: Vec<Vec<i32>>

Clauses as disjunctions of literals (positive = var index, negative = -(var index+1)).

Implementations

impl SATInstance

pub fn new(num_vars: usize) -> Self

Create a new empty SAT instance with given number of variables.

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

Add a clause to the SAT instance.

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

Naive SAT solver by exhaustive enumeration.

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

Evaluate all clauses under a given assignment.