<div class="csl-bib-body">
<div class="csl-entry">Peitl, T., Slivovsky, F., & Szeider, S. (2016). Long Distance Q-Resolution with Dependency Schemes. In N. Creignou & D. Le Berre (Eds.), <i>Theory and Applications of Satisfiability Testing – SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings</i> (pp. 500–518). Cham. https://doi.org/10.1007/978-3-319-40970-2_31</div>
</div>
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.description.sponsorship
Austrian Science Funds (FWF)
-
dc.language
English
-
dc.language.iso
en
-
dc.publisher
Cham
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
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.isbn
9783319409702
-
dc.relation.doi
10.1007/978-3-319-40970-2
-
dc.relation.issn
0302-9743
-
dc.description.startpage
500
-
dc.description.endpage
518
-
dc.relation.grantno
P27721
-
dc.relation.grantno
W1255-N23
-
dc.rights.holder
Springer International Publishing Switzerland 2016
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Theory and Applications of Satisfiability Testing – SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
-
tuw.container.volume
9710
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.version
am
-
tuw.publication.orgunit
E192-01 - Forschungsbereich Algorithms and Complexity
-
tuw.publisher.doi
10.1007/978-3-319-40970-2_31
-
dc.identifier.libraryid
AC11362647
-
dc.description.numberOfPages
19
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:3-3078
-
tuw.author.orcid
0000-0001-7799-1568
-
tuw.author.orcid
0000-0001-8994-1656
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
tuw.event.name
SAT: International Conference on Theory and Applications of Satisfiability Testing 2016
-
tuw.event.startdate
05-07-2016
-
tuw.event.enddate
08-07-2016
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Bordeaux
-
tuw.event.country
FR
-
tuw.event.presenter
Peitl, Tomáš
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
open
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity
