Struct DpllSolver 

pub struct DpllSolver { /* private fields */ }

DPLL-based propositional SAT solver. Variables are 1..=n. Clauses are lists of literals (positive = var, negative = -var).

Implementations

impl DpllSolver

pub fn new(n_vars: usize) -> Self

Create a new DPLL solver with n_vars variables.

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

Add a clause (disjunction of literals).

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

Solve. Returns Some(assignment) if SAT (assignment[i] = value of variable i+1).