zbMATH — the first resource for mathematics

A little blocked literal goes a long way. (English) Zbl 06807232
Gaspers, Serge (ed.) et al., Theory and applications of satisfiability testing – SAT 2017. 20th international conference, Melbourne, VIC, Australia, August 28 – September 1, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-66262-6/pbk; 978-3-319-66263-3/ebook). Lecture Notes in Computer Science 10491, 281-297 (2017).
Summary: 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 \(\mathsf {QRAT}\), a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that \(\mathsf {QRAT}\) polynomially simulates long-distance resolution. Two simple rules of \(\mathsf {QRAT}\) 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 \(\mathsf {QRAT}\) proofs. In a case study, we compare long-distance-resolution proofs of the well-known Kleine B√ľning formulas with corresponding \(\mathsf {QRAT}\) proofs.
For the entire collection see [Zbl 1368.68008].
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
DepQBF; DRAT-trim
Full Text: DOI