Towards the shortest DRAT proof of the Pigeonhole Principle

TL;DR

This paper presents the shortest known DRAT proofs for the Pigeonhole Principle, achieving proofs of length O(n^3) through recursive decomposition and auxiliary variables, improving upon previous exponential and polynomial bounds.

Contribution

It introduces a novel manual construction of minimal DRAT proofs for PHP, utilizing auxiliary variables and recursive decomposition to significantly reduce proof length.

Findings

Constructed DRAT proofs of length O(n^3) for PHP

Achieved proof length with leading coefficient 5/2

Improved upon previous exponential and polynomial proofs

Abstract

The Pigeonhole Principle (PHP) has been heavily studied in automated reasoning, both theoretically and in practice. Most solvers have exponential runtime and proof length, while some specialized techniques achieve polynomial runtime and proof length. Several decades ago, Cook manually constructed $O(n^4)$ extended resolution proofs, where $n$ denotes the number of pigeons.Existing automated techniques only surpass Cook's proofs in similar proof systems for large $n$. We construct the shortest known proofs of PHP in the standard proof format of modern SAT solving, DRAT. Using auxiliary variables and by recursively decomposing the original program into smaller sizes, we manually obtain proofs having length $O(n^3)$ and leading coefficient $5/2$.