Skip to content
STIMSMITH

Branch-and-Bound

Concept WIKI v1 · 6/9/2026

Branch-and-bound is a search technique that uses a backtracking search tree to turn a satisfaction problem into an optimization problem by combining recursive subdivision (branching) with pruning via computed bounds. It is a foundational algorithmic pattern used in constraint programming, MaxSAT solving, and neural network verification.

Overview

Branch-and-bound is a search technique that operates over the backtracking search tree of a constraint-based solver. It is described as "an efficient technique to search for optimality using the search tree," with the search tree itself providing the mechanism to "turn a satisfaction problem into an optimization problem" [1].

How it Relates to the Search Tree

In a constraint solver, the engine coordinates propagators and a guessing method (search with backtracking). The solver runs each propagator until a fixed-point is reached (a round of propagation). If the fixed-point is not a solution, the solver resorts to guessing: picking a variable and constraining its domain. Guesses are kept as a tree (the search tree), and the solver backtracks from incorrect guesses. The variable selection heuristic and value selection heuristic together decide the shape of the search tree [1].

Branch-and-bound is the technique that exploits this search-tree structure to look for an optimal solution rather than just any feasible one [1].

Use in MaxSAT Solving

Branch-and-bound is one of the state-of-the-art algorithmic patterns for MaxSAT, the optimization variant of SAT. The dominant branch-and-bound MaxSAT solver is MaxCDCL, which has been extended with proof-logging support to certify look-ahead methods and clausal encodings of pseudo-Boolean constraints based on Multi-Valued Decision Diagrams (MDDs). Proof logging in this setting was shown to be feasible with limited overhead, although proof checking remains a challenge [arxiv:2511.10273].

Use in Neural Network Verification

Branch-and-bound is also used inside modern neural network verifiers. The BICCOS method ("Branch-and-bound Inferred Cuts with COnstraint Strengthening") exploits the structure of neural network verification to generate scalable cutting planes. It leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and introduces cuts that preclude these relationships in other subproblems. BICCOS additionally assigns influence scores to neurons in each path to allow cut strengthening, and uses a multi-tree search technique to identify more cuts. The approach is part of the α,β-CROWN verifier, the VNN-COMP 2024 winner [arxiv:2501.00200].

Use in Code Generation for Custom Architectures

Branch-and-bound has also been applied in code generation for custom architectures, where constraint programming is used to model the placement, scheduling, and resource-binding sub-problems and branch-and-bound is used to search the resulting search tree for optimal or near-optimal solutions [2].

LINKED ENTITIES

1 links
Code Generation for Custom Architectures using Constraint Programming USES

CITATIONS

4 sources
4 citations
[1] The search tree of a constraint solver can be used to turn a satisfaction problem into an optimization problem, and branch-and-bound is an efficient technique to search for optimality using that search tree. Arslan, Mehmet Ali (PhD thesis)
[2] In a constraint solver, guesses are kept as a search tree; variable selection and value selection heuristics decide the shape of the tree, and the solver backtracks from incorrect guesses. Arslan, Mehmet Ali (PhD thesis)
[3] MaxCDCL is the dominant branch-and-bound MaxSAT solver, and proof logging has been added to certify look-ahead methods and MDD-based clausal encodings of pseudo-Boolean constraints, with feasible overhead but proof checking still a challenge. Certified Branch-and-Bound MaxSAT Solving (Extended Version)
[4] BICCOS leverages logical relationships of neurons within verified subproblems in the branch-and-bound search tree, introduces cuts that preclude these relationships in other subproblems, assigns influence scores to neurons per path for cut strengthening, and uses multi-tree search; it is part of the α,β-CROWN verifier (VNN-COMP 2024 winner). Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes