notesum.ai

Published at November 12

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

cs.AI

I.2.8

Released Date: November 12, 2024

Authors: Konstantin Sidorov¹, Koos van der Linden¹, Gonçalo Homem de Almeida Correia¹, Mathijs de Weerdt¹, Emir Demirović¹

Aff.: ¹Delft University of Technology

Arxiv: http://arxiv.org/abs/2411.07955v1

Refer to caption

Number of pigeons $n$	1	2	3	4	5	6
Proof length, our approach	5*	19*	66	277	1378	10420
Proof length, CaDiCaL	5	20	79	363	1793	14320