# 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].
##### MSC:
 68Q25 Analysis of algorithms and problem complexity 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
##### Software:
DepQBF; DRAT-trim
Full Text: