Marijn Heule, Benjamin Kiesl, Armin Biere,
"Clausal Proofs of Mutilated Chessboards"
, in Intl. Symp. NASA Formal Methods (NFM'19): Proc. 11th Intl. Symp. NASA Formal Methods (NFM'19), Serie LNCS, Vol. 11460, Springer, Seite(n) 204-210, 2019
Clausal Proofs of Mutilated Chessboards
Sprache des Titels:
Proc. 11th Intl. Symp. NASA Formal Methods (NFM'19)
Mutilated chessboard problems have been called a ?tough nut to crack? for automated reasoning. They are, for instance, hard for resolution, resulting in exponential runtime of current SAT solvers. Although there exists a well-known short argument for solving mutilated chessboard problems, this argument is based on an abstraction that is challenging to discover by automated-reasoning techniques. In this paper, we present another short argument that is much easier to compute and that can be expressed within the recent (clausal) PR proof system for propositional logic. We construct short clausal proofs of mutilated chessboard problems using this new argument and validate them using a formally-veri?ed proof checker.