Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
B. Kiesl, M. Heule, M. Seidl:
"A Little Blocked Literal Goes a Long Way";
Vortrag: 20th International Conference on Theory and Applications of Satisfiability Testing - SAT 2017,
Melbourne, Australien;
28.08.2017
- 01.09.2017; in: "Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing",
S. Gaspers, T. Walsh (Hrg.);
Lecture Notes in Computer Science (LNCS) / Springer,
10491
(2017),
ISBN: 978-3-319-66262-6;
S. 281
- 297.
Kurzfassung englisch:
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.
Schlagworte:
quantified boolean formulas, qbf, qrat, proof complexity
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-66263-3_18
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_266840.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.