<div class="csl-bib-body">
<div class="csl-entry">Beyersdorff, O., Blinkhorn, J., Mahajan, M., Peitl, T., & Sood, G. (2023). Hard QBFs for merge resolution. <i>ACM Transactions on Computation Theory</i>. https://doi.org/10.1145/3638263</div>
</div>
-
dc.identifier.issn
1942-3454
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/193563
-
dc.description.abstract
We prove the first genuine QBF proof size lower bounds for the proof system Merge Resolution (MRes [7]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [7], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems.
Here we show the first genuine QBF exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems ∀Exp + Res and IR.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.publisher
Association for Computing Machinery
-
dc.relation.ispartof
ACM Transactions on Computation Theory
-
dc.subject
QBF
en
dc.subject
resolution
en
dc.subject
strategy
en
dc.title
Hard QBFs for merge resolution
en
dc.type
Article
en
dc.type
Artikel
de
dc.contributor.affiliation
Friedrich-Schiller-Universität Jena, Germany
-
dc.contributor.affiliation
Friedrich-Schiller-Universität Jena, Germany
-
dc.contributor.affiliation
Homi Bhabha National Institute, India
-
dc.contributor.affiliation
Homi Bhabha National Institute, India
-
dc.relation.grantno
J4361
-
dc.type.category
Original Research Article
-
tuw.journal.peerreviewed
true
-
tuw.peerreviewed
true
-
wb.publication.intCoWork
International Co-publication
-
tuw.project.title
Von QBF zu DQBF: Theorie zusammen mit Praxis
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
dcterms.isPartOf.title
ACM Transactions on Computation Theory
-
tuw.publication.orgunit
E192-01 - Forschungsbereich Algorithms and Complexity
-
tuw.publisher.doi
10.1145/3638263
-
dc.date.onlinefirst
2023-12-22
-
dc.identifier.eissn
1942-3462
-
dc.description.numberOfPages
23
-
tuw.author.orcid
0000-0001-7799-1568
-
dc.description.sponsorshipexternal
John Templeton Foundation
-
dc.description.sponsorshipexternal
DFG
-
dc.relation.grantnoexternal
60842
-
dc.relation.grantnoexternal
BE 4209/3-1
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.openairecristype
http://purl.org/coar/resource_type/c_2df8fbb1
-
item.cerifentitytype
Publications
-
item.grantfulltext
restricted
-
item.fulltext
no Fulltext
-
item.languageiso639-1
en
-
item.openairetype
research article
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.grantno
J4361
-
crisitem.author.dept
Friedrich-Schiller-Universität Jena, Germany
-
crisitem.author.dept
Friedrich-Schiller-Universität Jena, Germany
-
crisitem.author.dept
Homi Bhabha National Institute, India
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity