[Back]

B. Kiesl, M. Heule, M. Seidl:
"A Little Blocked Literal Goes a Long Way";
Talk: 20th International Conference on Theory and Applications of Satisfiability Testing - SAT 2017, Melbourne, Australien; 2017-08-28 - 2017-09-01; in: "Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing", S. Gaspers, T. Walsh (ed.); Lecture Notes in Computer Science (LNCS) / Springer, 10491 (2017), ISBN: 978-3-319-66262-6; 281 - 297.

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 QRAT, a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that QRAT polynomially simulates long-distance resolution. Two simple rules of 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 QRAT proofs. In a case study, we compare long-distance-resolution proofs of the well-known Kleine Büning formulas with corresponding QRAT proofs.

quantified boolean formulas, qbf, qrat, proof complexity

http://dx.doi.org/10.1007/978-3-319-66263-3_18

http://publik.tuwien.ac.at/files/publik_266840.pdf