Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
T. Peitl, F. Slivovsky, S. Szeider:
"Long Distance Q-Resolution with Dependency Schemes";
Vortrag: Theory and Application of Satisfiability Testing -- SAT,
Bordeaux, France;
05.07.2016
- 08.07.2016; in: "Proceedings of SAT 2016: Theory and Applications of Satisfiability Testing - SAT 2016",
(2016),
ISBN: 978-3-319-40969-6;
S. 500
- 518.
Kurzfassung englisch:
Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers, which use these systems to generate proofs. In this paper, we define a new proof system that combines two such proof systems: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system is sound for the reflexive resolution-path dependency scheme-in fact, we prove that it admits strategy extraction in polynomial time. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q-resolution with universal reduction according to the standard dependency scheme. We report on experiments with a configuration of DepQBF that generates proofs in this system.
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_254744.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.