Struct BinaryImplicationGraph 

pub struct BinaryImplicationGraph { /* private fields */ }

Binary Implication Graph optimizer

Implementations

impl BinaryImplicationGraph

pub fn new(num_vars: usize) -> Self

Create a new BIG optimizer

pub fn build(&mut self, clauses: &ClauseDatabase)

Build the implication graph from clause database

pub fn transitive_reduction(&mut self) -> Vec<(Lit, Lit)>

Perform transitive reduction to remove redundant implications

An edge a => c is redundant if there exists a path a => b => c

pub fn find_sccs(&mut self) -> Vec<Vec<Lit>>

Detect strongly connected components using Tarjan’s algorithm

Literals in the same SCC are equivalent (mutual implication)

pub fn optimize(&mut self, clauses: &mut ClauseDatabase)

Apply BIG optimizations to clause database

Removes redundant binary clauses found through transitive reduction

pub fn get_implications(&self, lit: Lit) -> Vec<Lit>

Get all implications for a literal

pub fn implies(&self, a: Lit, b: Lit) -> bool

Check if literal a implies literal b

pub fn stats(&self) -> &BigStats

Get statistics

pub fn reset_stats(&mut self)

Reset statistics

Trait Implementations

impl Debug for BinaryImplicationGraph

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.