Towards the shortest DRAT proof of the Pigeonhole Principle

Autor:	Grosof, Isaac, Zhang, Naifeng, Heule, Marijn J. H.
Rok vydání:	2022
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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$. Comment: 13 pages. To appear in Pragmatics of SAT 2022
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2207.11284 Zobrazit plný text záznamu View this record from Arxiv