Long Distance Q-Resolution with Dependency Schemes (bibtex)

by Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider

Abstract:

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.

Reference:

Long Distance Q-Resolution with Dependency SchemesTomáš Peitl, Friedrich Slivovsky, Stefan SzeiderTheory and Applications of Satisfiability Testing – SAT 2016 (Nadia Creignou, Daniel Le Berre, eds.), pages 500–518, 2016, Springer International Publishing.

Bibtex Entry:

@InProceedings{PeitlSlivovskySzeider16, author="Peitl, Tom{\'a}{\v{s}} and Slivovsky, Friedrich and Szeider, Stefan", editor="Creignou, Nadia and Le Berre, Daniel", title="Long Distance Q-Resolution with Dependency Schemes", booktitle="Theory and Applications of Satisfiability Testing -- {SAT} 2016", year="2016", publisher="Springer International Publishing", address="Cham", pages="500--518", abstract="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.", isbn="978-3-319-40970-2", doi="10.1007/978-3-319-40970-2_31", url="http://repositum.tuwien.ac.at/obvutwoa/download/pdf/2034178?originalFilename=true" }

Powered by bibtexbrowser