Zur Seitenansicht
 

Titelaufnahme

Titel
Long Distance Q-Resolution with Dependency Schemes
VerfasserPeitl, Tomáš ; Slivovsky, Friedrich ; Szeider, Stefan
Erschienen in
Lecture Notes in Computer Science / Creignou, Nadia; Le Berre, Daniel, Cham, 2016, S. 500-518
Erschienen2016
SpracheEnglisch
SerieSAT: International Conference on Theory and Applications of Satisfiability Testing ; Theory and Applications of Satisfiability Testing SAT 2016
DokumenttypAufsatz in einem Sammelwerk
Schlagwörter (EN)QBF / Dependency Schemes / Long-distance / Q-resolution
Projekt-/ReportnummerFWF-P27721
Projekt-/ReportnummerFWF-W1255-N23
ISBN978-3-319-40970-2
URNurn:nbn:at:at-ubtuw:3-3078 Persistent Identifier (URN)
DOI10.1007/978-3-319-40970-2_31 
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Long Distance Q-Resolution with Dependency Schemes [1.21 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

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.

Notiz
Notiz