Go to page
 

Bibliographic Metadata

Title
Long Distance Q-Resolution with Dependency Schemes
AuthorPeitl, Tomáš ; Slivovsky, Friedrich ; Szeider, Stefan
Published in
Lecture Notes in Computer Science / Creignou, Nadia; Le Berre, Daniel, Cham, 2016, page 500-518
Published2016
LanguageEnglish
SeriesSAT: International Conference on Theory and Applications of Satisfiability Testing ; Theory and Applications of Satisfiability Testing SAT 2016
Document typeArticle in a collected edition
Keywords (EN)QBF / Dependency Schemes / Long-distance / Q-resolution
Project-/ReportnumberFWF-P27721
Project-/ReportnumberFWF-W1255-N23
ISBN9783319409702
URNurn:nbn:at:at-ubtuw:3-3078 Persistent Identifier (URN)
DOI10.1007/978-3-319-40970-2_31 
Restriction-Information
 The work is publicly available
Files
Long Distance Q-Resolution with Dependency Schemes [1.21 mb]
Links
Reference
Classification
Abstract (English)

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 schemein 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.

Note
Note
Stats
The PDF-Document has been downloaded 38 times.