Benjamin Kiesl, Marijn Heule, Martina Seidl,
"A Little Blocked Literal Goes a Long Way"
, in Serge Gaspers and Toby Walsh: Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, Serie Lecture Notes in Computer Science (LNCS), Vol. 10491, Springer, Seite(n) 281-297, 2017
Original Titel:
A Little Blocked Literal Goes a Long Way
Sprache des Titels:
Englisch
Original Buchtitel:
Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings
Original Kurzfassung:
Q-resolution is a generalization of propositional resolution that provides the theoretical foundation for search-based solvers of quantified Boolean formulas (QBFs). Recently, it has been shown that an extension of Q-resolution, called long-distance resolution, is remarkably powerful both in theory and in practice. However, it was unknown how long-distance resolution is related to ????????, a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that ???????? polynomially simulates long-distance resolution. Two simple rules of ???????? are crucial for our simulation?blocked-literal addition and blocked-literal elimination. Based on the simulation, we implemented a tool that transforms long-distance-resolution proofs into ???????? proofs. In a case study, we compare long-distance-resolution proofs of the well-known Kleine Büning formulas with corresponding ???????? proofs.
Forschungs-