论文标题
朝着最短的鸽子原理证明
Towards the shortest DRAT proof of the Pigeonhole Principle
论文作者
论文摘要
在理论上和实践中，对自动推理进行了大量研究。大多数求解器具有指数运行时和证明长度，而一些专业技术实现了多项式运行时和证明长度。几十年前，库克手动构建了$ O（n^4）$扩展的分辨率证明，其中$ n $表示鸽子的数量。存在自动化技术仅超过库克在大型$ n $的类似证明系统中的证明。我们以现代SAT解决的标准证明格式Drat构建了PHP的最短证明。使用辅助变量并递归将原始程序分解为较小的尺寸，我们手动获得具有长度$ O（n^3）$和领先系数$ 5/2 $的证明。
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$.
