Struct ResolutionProverSmall 

pub struct ResolutionProverSmall { /* private fields */ }

Simple resolution-based propositional prover. Works on clauses over integer literals (positive = var, negative = negated var). Attempts to derive the empty clause (refutation).

Implementations

impl ResolutionProverSmall

pub fn new() -> Self

Create a new prover.

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

Add a clause.

pub fn refute(&self, max_steps: usize) -> bool

Attempt to find a resolution refutation (saturation, bounded by max_steps). Returns true if the empty clause is derived.

Trait Implementations

impl Default for ResolutionProverSmall

fn default() -> Self

Returns the “default value” for a type.