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 that use these systems to generate proofs. We study a combination of two proof systems supported by the solver DepQBF: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system—which we call long-distance Q(D)-resolution—is sound for the reflexive resolution-path dependency scheme. In fact, we prove that it admits strategy extraction in polynomial time. This comes as an application of a general result, by which we identify a whole class of dependency schemes for which long-distance Q(D)-resolution admits polynomial-time strategy extraction. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q(D)-resolution with the standard dependency scheme. We further show that search-based QBF solvers using a dependency scheme D and learning with long-distance Q-resolution generate long-distance Q(D)-resolution proofs. The above soundness results thus translate to partial soundness results for such solvers: they declare an input QBF to be false only if it is indeed false. Finally, we report on experiments with a configuration of DepQBF that uses the standard dependency scheme and learning based on long-distance Q-resolution.

Reference:

Long-Distance Q-Resolution with Dependency SchemesTomáš Peitl, Friedrich Slivovsky, Stefan SzeiderJournal of Automated Reasoning, Jun 2018.

Bibtex Entry:

@Article{PeitlSlivovskySzeider18a, author="Peitl, Tom{\'a}{\v{s}} and Slivovsky, Friedrich and Szeider, Stefan", title="Long-Distance Q-Resolution with Dependency Schemes", journal="Journal of Automated Reasoning", year="2018", month="Jun", day="09", 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 that use these systems to generate proofs. We study a combination of two proof systems supported by the solver DepQBF: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system---which we call long-distance Q(D)-resolution---is sound for the reflexive resolution-path dependency scheme. In fact, we prove that it admits strategy extraction in polynomial time. This comes as an application of a general result, by which we identify a whole class of dependency schemes for which long-distance Q(D)-resolution admits polynomial-time strategy extraction. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q(D)-resolution with the standard dependency scheme. We further show that search-based QBF solvers using a dependency scheme D and learning with long-distance Q-resolution generate long-distance Q(D)-resolution proofs. The above soundness results thus translate to partial soundness results for such solvers: they declare an input QBF to be false only if it is indeed false. Finally, we report on experiments with a configuration of DepQBF that uses the standard dependency scheme and learning based on long-distance Q-resolution.", issn="1573-0670", doi="10.1007/s10817-018-9467-3", url="https://doi.org/10.1007/s10817-018-9467-3" }

Powered by bibtexbrowser