Struct TwoSatSolver 

pub struct TwoSatSolver { /* private fields */ }

Evaluate a 2-CNF formula (given as list of clauses over bool variables). Returns true if satisfiable (2-SAT, solved via Kosaraju SCC).

Implementations

impl TwoSatSolver

pub fn new(n: usize) -> Self

Create a new 2-SAT solver for n variables.

pub fn add_clause(&mut self, a: usize, b: usize)

Add clause (a OR b). a and b are literals: 2var for positive, 2var+1 for negative.

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

Solve. Returns Some(assignment) if satisfiable, None otherwise.