How to Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization

Background: Modern SAT solvers are indispensable reasoning tools that are widely applied in verification, planning, andcombinatorial design. Beyond answering satisfiability, they also produce unsatisfiability proofs, which are valuable forcertification and analysis. Since there are no guarantees that their length is close to optimal, however, those proofs areinsufficient to make claims about the gap between the solver proofs and the shortest possible proof. Understanding this gap isimportant for analyzing solver behavior, as it can be seen as a proxy for evaluating the room for improvement of the solverfor the input formula in question.

Objectives: We study the problem of finding the shortest resolution proofs for unsatisfiable formulas. Our goal is tounderstand how far solver-generated proofs deviate from the optimum, and to develop algorithms that can discover proofssubstantially 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 alayer listrepresentation that eliminates all symmetries from clause permutations, thereby improving uponan earlier SAT-encoding approach to proof length minimization. Further, we accelerate the search by integrating pruningtechniques 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% forformulas from the SAT Competition editions from 2002 to 2025, as well as halves the proof lengths for half of the availableformulas from planning problems. As an exact method, it solves twice as many minimally unsatisfiable instances as thestate-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 removingredundant claims, but by an entirely different chain of derivations—and that resolution proof length minimization is moretractable in practice than earlier approaches suggested. Our work highlights proof length minimization as a useful perspectivefor analyzing solver behavior and opens avenues for applying similar techniques to stronger proof systems.

Recommended citation: Sidorov, K., Van der Linden, K., Correia, G. H. A., De Weerdt, M. & Demirović, E. (2026) "How to Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization" Journal of Artificial Intelligence Research 86, Article 54, 39 pages.
Download Paper