The final publication is available via <a href="https://doi.org/10.1007/978-3-319-40970-2_31" target="_blank">https://doi.org/10.1007/978-3-319-40970-2_31</a>.
-
dc.description.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.
en
dc.description.sponsorship
Austrian Science Funds (FWF)
-
dc.language
English
-
dc.language.iso
en
-
dc.publisher
Cham
-
dc.relation.ispartofseries
SAT: International Conference on Theory and Applications of Satisfiability Testing
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
QBF
en
dc.subject
Dependency Schemes
en
dc.subject
Long-distance
en
dc.subject
Q-resolution
en
dc.title
Long Distance Q-Resolution with Dependency Schemes
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.relation.publication
Lecture Notes in Computer Science ; Creignou, Nadia; Le Berre, Daniel
-
dc.relation.grantno
P27721
-
dc.relation.grantno
W1255-N23
-
dc.rights.holder
Springer International Publishing Switzerland 2016
-
dc.type.category
Full-Paper Contribution
-
tuw.container.volume
Theory and Applications of Satisfiability Testing – SAT 2016
-
tuw.version
am
-
tuw.publication.orgunit
E192 - Institut für Computergraphik und Algorithmen