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"
}