Every mixed-integer programme (MIP — an optimisation problem where some variables must take integer values) is solved by branch-and-bound: the solver recursively fixes the values of integer variables, creating a tree of subproblems. At many nodes in that tree, the fixed values produce a contradiction — the constraints cannot all be satisfied simultaneously. The subproblem is infeasible.
Without conflict analysis, each infeasibility is a one-time discovery. The solver records the dead branch, backtracks, and continues. But the same combination of variable assignments that caused the infeasibility may reappear at many different nodes in the tree, approached from different ancestors. The solver will rediscover the same contradiction repeatedly, wasting computation on dead regions it has already proved are impossible.
The hard problem: How do you make infeasibility proofs reusable across the entire search tree, not just the branch where they were found?
Conflict analysis extracts the reason a subproblem is infeasible — the minimal set of variable bounds and constraint violations that made it impossible — and encodes that reason as a new constraint added permanently to the model. This constraint, called a conflict clause or conflict cut, rules out all assignments that reproduce the same infeasibility, wherever they appear in the remaining search tree.
The process runs as a loop inside the branch-and-bound search:
- Detect infeasibility. A node’s LP relaxation (the continuous version of the subproblem, which relaxes integer constraints) returns infeasible, or propagation of branching constraints leads to a logical contradiction.
- Extract the reason. The solver traces back through the sequence of variable fixings and constraint tightenings that produced the contradiction, identifying the minimal “reason set” — the smallest collection of bounds and constraints whose conjunction implies infeasibility.
- Encode as a constraint. The reason set is converted into a linear inequality (a conflict cut) or a logical clause (a conflict clause, a disjunction of variable bounds that must be satisfied to avoid the infeasibility). Both forms are valid for MIP.
- Add to the model. The conflict constraint is appended to the global model, not just to the current branch. Every node in the remaining tree inherits it. The solver never enters the infeasible region again.
Modern solvers implement two flavours: clause-based conflict analysis (borrowed from SAT solving — a technique for satisfiability problems over binary variables — and generalised to MIP) and cut-based conflict analysis (which produces a linear inequality from the infeasibility proof, giving a strictly tighter bound than a clause). SCIP 10 introduced cut-based conflict analysis alongside the existing clause-based approach.
Let x be the vector of integer decision variables (the things the solver is choosing). A branching path is a sequence of bounds of the form xᵢ ≤ uᵢ or xᵢ ≥ lᵢ that the solver has fixed along a path from the root to the current node.
When propagation (the process of deducing further bounds from constraints, given the current fixings) detects an infeasibility, it identifies a conflict set C: the minimal subset of the current bounds whose conjunction implies infeasibility. That is, no assignment satisfying all bounds in C simultaneously can satisfy all the model’s constraints.
The conflict cut derived from C is a linear inequality that is violated by every assignment in C — meaning it cuts off all variable assignments that reproduce this infeasibility — but satisfied by every feasible solution to the original problem (so no valid solution is lost).
In the clause-based version, the conflict clause is the disjunction: at least one of the bounds in C must be relaxed (i.e., violated). In the cut-based version, a linear combination of the constraints in the infeasibility proof yields a linear inequality tight enough to exclude the infeasible region.
In plain English: the infeasibility proof is a certificate that says “whenever variable xᵢ ≥ a AND x ≤ b AND …, the problem has no solution.” The conflict cut encodes this certificate as a constraint that permanently forbids those combinations across the full tree.
Setup. A logistics company is solving an integer programme (a discrete optimisation problem with binary yes/no decision variables) for overnight truck routing. The model decides which drivers are assigned to which routes. Two binary variables: x₁ = 1 means driver A is assigned to route 1; x₂ = 1 means driver B is assigned to route 2. Both routes require a mandatory stop at a rest facility that can accommodate only one truck at a time.
Without conflict analysis. The solver branches: at node N₁, it sets x₁ = 1. At node N₂ (child of N₁), it sets x₂ = 1. Propagation discovers the rest-facility conflict: both drivers cannot use the same facility simultaneously. Infeasibility. The solver backtracks to N₁ and tries x₂ = 0. Later, at a completely different part of the tree — with different ancestors — the solver again arrives at a node where x₁ = 1 and x₂ = 1. It rediscovers the same infeasibility. This rediscovery can happen dozens or hundreds of times on a large instance.
With conflict analysis. When the infeasibility at N₂ is detected, the solver extracts the reason: the constraint x₁ + x₂ ≤ 1 (at most one of these two routes can be active simultaneously) is derived as a conflict cut. This cut is added globally to the model. Every node in the remaining tree inherits it. The solver never again explores any assignment with x₁ = 1 and x₂ = 1. One infeasibility proof becomes a permanent barrier.
The symbols, for the record. The conflict set is C = {x₁ ≥ 1, x₂ ≥ 1}. The conflict cut derived is x₁ + x₂ ≤ 1. This inequality is satisfied by all feasible solutions (the facility constraint was always implicitly required) but is now explicit and globally applied.
Practitioners see conflicts: 47 in a solver log and assume the model has 47 constraint violations to fix. This is wrong. The model is still a valid formulation. That number reports how many conflict clauses (reusable constraints derived from infeasibility proofs encountered during branch-and-bound) the solver generated during the search. A high conflict count usually signals the solver is working near a tight feasibility boundary — it can indicate a well-structured problem where the solver is learning efficiently from dead branches, not a modelling error.
Think of the conflict count as a measure of how much infeasibility structure the solver has exploited, not a count of errors in your model.
Infeasibility debugging tells a practitioner why their complete model has no feasible solution at all — the model itself is overconstrained. Conflict analysis is a completely separate mechanism that operates inside a globally feasible model, during the search for an integer-feasible point (a solution that satisfies integrality constraints as well as the linear constraints). It analyses local infeasibilities created by branching decisions, not global infeasibility of the model.
If your model is globally infeasible (no feasible solution exists regardless of variable values), conflict analysis cannot help. You need to examine the constraint set directly using infeasibility isolation tools (minimum infeasible subsystem, or MIS, analysis). Conflict analysis only fires when the solver is searching for a feasible integer solution inside a feasible continuous relaxation.
Clause-based conflict analysis (borrowed from SAT solvers — tools for determining whether a logical formula over binary variables is satisfiable) produces a disjunction: at least one of the bounds in the conflict set must be relaxed. Cut-based conflict analysis (introduced in SCIP 10) produces a linear inequality derived from a linear combination of the constraints in the infeasibility proof. The linear inequality is generally tighter — it excludes more of the infeasible region — but is more expensive to derive. For instances dominated by logical conflicts (bin packing, combinatorial scheduling), clause-based is often sufficient. For instances where the infeasibility arises from tight continuous bounds (capacity planning, network design), cut-based conflict analysis typically provides a stronger pruning effect.
The first question to ask when evaluating any published MIP implementation: is conflict analysis enabled, and what does the solver log show for conflict clause count and tree size reduction?
The Achterberg Principle: every infeasibility proof is a free constraint. A solver that does not record and reuse infeasibility proofs is discarding the most valuable information the search generates — proof that certain regions of the tree are permanently dead.