Struct TruthTableChecker 

pub struct TruthTableChecker {
    pub num_vars: usize,
}

A simple truth table checker for propositional formulas over a fixed number of variables.

Checks if a formula is a tautology, satisfiable, or contradictory by exhaustive enumeration of truth assignments.

Fields

num_vars: usize

Number of propositional variables.

Implementations

impl TruthTableChecker

pub fn new(n: usize) -> Self

Create a checker for n variables.

pub fn all_assignments(&self) -> Vec<Vec<bool>>

Enumerate all truth assignments.

pub fn is_tautology(&self, formula: &NnfFormula) -> bool

Check if a formula (given as evaluator) is a tautology.

pub fn is_satisfiable(&self, formula: &NnfFormula) -> bool

Check if a formula is satisfiable.

pub fn is_contradiction(&self, formula: &NnfFormula) -> bool

Check if a formula is a contradiction.

pub fn find_satisfying_assignment( &self, formula: &NnfFormula, ) -> Option<Vec<bool>>

Find a satisfying assignment, if one exists.

pub fn count_satisfying(&self, formula: &NnfFormula) -> usize

Count the number of satisfying assignments.