How to discover short, shorter, and the shortest proofs of unsatisfiability: A branch-and-bound approach for resolution proof length minimization
Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, and 2 more authors
J. Artif. Intell. Res., Aug 2026
Background: Modern SAT solvers are indispensable reasoning tools that are widely applied in verification, planning, and combinatorial design. Beyond answering satisfiability, they also produce unsatisfiability proofs, which are valuable for certification and analysis. Since there are no guarantees that their length is close to optimal, however, those proofs are insufficient to make claims about the gap between the solver proofs and the shortest possible proof. Understanding this gap is important for analyzing solver behavior, as it can be seen as a proxy for evaluating the room for improvement of the solver for the input formula in question. Objectives: We study the problem of finding the shortest resolution proofs for unsatisfiable formulas. Our goal is to understand how far solver-generated proofs deviate from the optimum, and to develop algorithms that can discover proofs substantially shorter than the solver-produced proofs. Methods: We propose a novel branch-and-bound algorithm for resolution proof length minimization. To facilitate it, we introduce a layer list representation that eliminates all symmetries from clause permutations, thereby improving upon an earlier SAT-encoding approach to proof length minimization. Further, we accelerate the search by integrating pruning techniques based on proof length lower bounds and clause subsumption. Results: Our algorithm consistently reduces solver proof lengths by 25–50% for synthetic instances and by 15—50% for formulas from the SAT Competition editions from 2002 to 2025, as well as halves the proof lengths for half of the available formulas from planning problems. As an exact method, it solves twice as many minimally unsatisfiable instances as the state-of-the-art approach and is faster by orders of magnitude on the overlapping instances. Conclusions: These results show that solver-generated proofs can often be substantially shortened—not by removing redundant claims, but by an entirely different chain of derivations—and that resolution proof length minimization is more tractable in practice than earlier approaches suggested. Our work highlights proof length minimization as a useful perspective for analyzing solver behavior and opens avenues for applying similar techniques to stronger proof systems.