Module cdcl_branching 

CDCL-Style (Conflict-Driven Clause Learning) MIP Branching

This module adapts CDCL techniques from SAT solving to MIP branch-and-bound. When a sub-problem is found infeasible, the algorithm extracts a “nogood” clause (a conjunction of branching decisions that caused infeasibility) and stores it to prune future subproblems that replay the same partial assignment.

Algorithm Overview

1. Branching: select the fractional variable with the highest VSIDS activity score.
2. Conflict analysis: when a node is infeasible, record a learned clause NOT(d_1) ∨ NOT(d_2) ∨ … ∨ NOT(d_k) for each branching decision d_i on the path.
3. Propagation: before expanding a node, check all learned clauses; prune if any clause is violated.
4. Activity decay: periodically decay all activity scores to prioritise recent conflicts (VSIDS heuristic).

Integration

The CdclBranchingState is designed to plug into MilpBranchAndBound via the BranchingStrategy::Cdcl variant (see BranchingStrategy). The host solver calls:

• select_branching_var to pick which variable to branch on.
• record_conflict when LP infeasibility is detected.
• apply_clauses before expanding each child node.
• decay_activities after each batch of conflicts.

References

• Marques-Silva & Sakallah (1996). “GRASP—A new search algorithm for satisfiability.” ICCAD.
• Achterberg, T. (2007). “Conflict analysis in mixed integer programming.” Discrete Optimization, 4(1), 4–20.

Structs

BranchingDecision

A single branching decision: set variable var_index to value value.

CdclBranchingState

Mutable state for CDCL-style MIP branching.

CdclConfig

Configuration for the CDCL branching state.

LearnedClause

A learned nogood clause: a disjunction of negated literals.

Enums

BranchingStrategy

Enumeration of branching strategies for use with MilpBranchAndBound.