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 Lecture Notes in Computer Science (LNCS), Vol. 11460, Springer, Seite(n) 204-210, 2019
Original Titel:
Clausal Proofs of Mutilated Chessboards
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 11th Intl. Symp. NASA Formal Methods (NFM'19)
Original Kurzfassung:
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.
Forschungs-