Struct BackboneDetector 

pub struct BackboneDetector { /* private fields */ }

Backbone detector

Implementations

impl BackboneDetector

pub fn new() -> Self

Create a new backbone detector with default algorithm

pub fn with_algorithm(algorithm: BackboneAlgorithm) -> Self

Create with specific algorithm

pub fn is_backbone(&self, lit: Lit) -> bool

Check if a literal is in the backbone

pub fn add_backbone(&mut self, lit: Lit)

Add a literal to the backbone

pub fn remove_backbone(&mut self, lit: Lit)

Remove a literal from the backbone

pub fn detect_iterative<F>( &mut self, candidates: &[Lit], is_sat_with_assumption: F, )

where F: FnMut(Lit) -> bool,

Detect backbone using iterative algorithm

For each literal l, check if the formula is UNSAT under assumption ~l. If UNSAT, then l must be in the backbone.

pub fn detect_binary_search<F>( &mut self, candidates: &[Lit], is_sat_with_assumptions: F, )

where F: Fn(&[Lit]) -> bool + Clone,

Detect backbone using binary search

Recursively partition the candidate set and test groups. More efficient when the backbone is large.

pub fn compute_rotatable(&self, all_lits: &[Lit]) -> Vec<Lit>

Compute rotatable literals (non-backbone)

A literal is rotatable if it can be both true and false in different satisfying assignments.

pub fn backbone(&self) -> Vec<Lit>

Get all backbone literals

pub fn size(&self) -> usize

Get backbone size

pub fn is_empty(&self) -> bool

Check if backbone is empty

pub fn stats(&self) -> &BackboneStats

Get statistics

pub fn clear(&mut self)

Reset the detector

pub fn algorithm(&self) -> BackboneAlgorithm

Get the algorithm being used

pub fn set_algorithm(&mut self, algorithm: BackboneAlgorithm)

Set the algorithm to use

Trait Implementations

impl Debug for BackboneDetector

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

Formats the value using the given formatter.

impl Default for BackboneDetector

fn default() -> Self

Returns the “default value” for a type.