Struct ResolutionGraph 

pub struct ResolutionGraph { /* private fields */ }

Resolution Graph for analyzing proof structure

Implementations

impl ResolutionGraph

pub fn new() -> Self

Create a new resolution graph

pub fn add_clause(&mut self, clause: Vec<Lit>, decision_level: usize) -> usize

Add a clause node to the graph

pub fn add_decision(&mut self, literal: Lit, decision_level: usize) -> usize

Add a decision node to the graph

pub fn add_resolution( &mut self, parent1_id: usize, parent2_id: usize, resolved_var: Var, result_clause: Vec<Lit>, decision_level: usize, ) -> usize

Record a resolution between two clauses

pub fn compute_depth(&self, node_id: usize) -> usize

Compute graph depth starting from a given node

pub fn analyze(&mut self)

Analyze the graph and update statistics

pub fn get_frequent_vars(&self, k: usize) -> Vec<(Var, usize)>

Get the top-k most frequently resolved variables

pub fn clause_quality(&self, node_id: usize) -> f64

Compute clause quality based on resolution graph structure

Lower scores indicate better quality clauses:

• Shorter resolution paths are better (fewer resolution steps)
• Clauses involving frequently-resolved variables are more important
• Clauses at lower decision levels are more general

pub fn find_redundant_resolutions(&self) -> Vec<usize>

Find redundant resolutions in the graph

Returns node IDs of resolutions that could be eliminated

pub fn stats(&self) -> &GraphStats

Get statistics about the graph

pub fn clear(&mut self)

Clear the graph

pub fn num_nodes(&self) -> usize

Get the number of nodes in the graph

pub fn get_node(&self, node_id: usize) -> Option<&ResolutionNode>

Get a node by ID

Trait Implementations

impl Debug for ResolutionGraph

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

Formats the value using the given formatter.

impl Default for ResolutionGraph

fn default() -> Self

Returns the “default value” for a type.