Struct HyperBinaryResolver 

pub struct HyperBinaryResolver { /* private fields */ }

Hyper-binary resolution manager

Performs probing and hyper-binary resolution to discover new binary clauses. This can strengthen the clause database and reduce search space.

Implementations

impl HyperBinaryResolver

pub fn new() -> Self

Create a new hyper-binary resolver

pub fn resize(&mut self, num_vars: usize)

Resize for new number of variables

pub fn add_binary_clause(&mut self, a: Lit, b: Lit)

Add a binary clause to the implication graph

For binary clause (a v b), this means:

• ~a => b (when a is false, b must be true)
• ~b => a (when b is false, a must be true)

pub fn probe(&mut self, probe_lit: Lit) -> Vec<HbrResult>

Probe a literal to discover implied literals

Assumes the literal is true and propagates to find all implications. Returns discovered binary clauses, units, or conflicts.

pub fn double_probe(&mut self, lit: Lit) -> Vec<HbrResult>

Perform double lookahead probing

Probes both polarities of a literal to discover implications. Can detect:

• Failed literals (both polarities lead to conflict)
• Forced assignments (one polarity always conflicts)
• Common implications (both polarities imply same literals)

pub fn stats(&self) -> &HyperBinaryStats

Get statistics

pub fn clear(&mut self)

Clear all implications

pub fn reset_stats(&mut self)

Reset statistics

Trait Implementations

impl Debug for HyperBinaryResolver

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

Formats the value using the given formatter.

impl Default for HyperBinaryResolver

fn default() -> Self

Returns the “default value” for a type.