Talks and Poster Presentations (with Proceedings-Entry):
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.
English abstract:
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.
Keywords:
quantified boolean formulas, qbf, qrat, proof complexity
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-66263-3_18
Electronic version of the publication:
http://publik.tuwien.ac.at/files/publik_266840.pdf
Created from the Publication Database of the Vienna University of Technology.