Struct CdclBranchingState 

pub struct CdclBranchingState<F = f64> {
    pub n_vars: usize,
    pub decisions: Vec<BranchingDecision>,
    pub learned_clauses: Vec<LearnedClause>,
    pub activity: Vec<F>,
    pub config: CdclConfig,
}

Mutable state for CDCL-style MIP branching.

Maintains a decision trail, a database of learned clauses, and VSIDS activity scores for heuristic variable selection.

Fields

n_vars: usize

Number of (binary/integer) variables in the problem.

decisions: Vec<BranchingDecision>

Current decision trail (ordered stack).

learned_clauses: Vec<LearnedClause>

Accumulated learned clauses (nogoods).

activity: Vec<F>

VSIDS activity scores per variable.

config: CdclConfig

Solver configuration.

Implementations

impl<F> CdclBranchingState<F>

where F: Float + FromPrimitive + Debug + Clone + AddAssign + MulAssign,

pub fn new(n_vars: usize, config: CdclConfig) -> OptimizeResult<Self>

Create a new CDCL branching state for a problem with n_vars variables.

pub fn select_branching_var(&self, lp_solution: &[F]) -> Option<usize>

Select the variable to branch on.

Among all variables that are fractional in the LP relaxation (i.e., 0 < lp_solution[i] < 1), return the index with the highest activity score. If no fractional variable exists, return None.

Arguments

• lp_solution – current LP relaxation solution (length n_vars).

pub fn record_conflict(&mut self, infeasible_decisions: &[BranchingDecision])

Record a conflict: given the set of branching decisions that led to infeasibility, extract a learned clause and update VSIDS activities.

Algorithm

1. Build clause {NOT d | d ∈ infeasible_decisions} as the conjunction of negated literals.
2. Bump activity for all variables in the clause.
3. Apply clause minimisation (remove literals subsumed by existing shorter clauses).
4. Evict oldest clauses if the database exceeds max_clauses.

At most max_learned_per_conflict clauses are added per call.

pub fn apply_clauses(&self, current_decisions: &[BranchingDecision]) -> bool

Check whether any learned clause is violated by the current decisions.

A clause is violated (fires) when every literal (i, v) in the clause is matched by some decision d with d.var_index == i and d.value == v. Firing indicates that the current node is provably infeasible and should be pruned.

Returns true if at least one clause fires (prune this node).

pub fn decay_activities(&mut self)

Decay all variable activity scores by multiplying by config.decay.

This implements the VSIDS (Variable State Independent Decaying Sum) heuristic, which prioritises variables that appeared in recent conflicts.

pub fn push_decision(&mut self, decision: BranchingDecision)

Push a new decision onto the decision trail.

pub fn pop_decision(&mut self) -> Option<BranchingDecision>

Pop the most recent decision from the trail (backtrack one level).

pub fn n_learned_clauses(&self) -> usize

Return the number of learned clauses currently in the database.

pub fn prune_inactive_clauses(&mut self)

Remove all learned clauses with activity below the configured threshold.

Trait Implementations

impl<F: Clone> Clone for CdclBranchingState<F>

fn clone(&self) -> CdclBranchingState<F>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<F: Debug> Debug for CdclBranchingState<F>

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

Formats the value using the given formatter.