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