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, and combinatorial design. Beyond answering satisfiability, they also produce unsatisfiability proofs, which are valuable for certification and analysis.