Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Strong ETH and Resolution via Games and the Multiplicity of Strategies
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2017 (English)In: Algorithmica, ISSN 0178-4617, E-ISSN 1432-0541, Vol. 79, no 1, p. 29-41Article in journal (Refereed) Published
Abstract [en]

We consider a proof system intermediate between regular Resolution, in which no variable can be resolved more than once along any refutation path, and general Resolution. We call -regular Resolution such system, in which at most a fraction of the variables can be resolved more than once along each refutation path (however, the re-resolved variables along different paths do not need to be the same). We show that when for not too large, -regular Resolution is consistent with the Strong Exponential Time Hypothesis (SETH). More precisely, for large n and k, we show that there are unsatisfiable k-CNF formulas which require -regular Resolution refutations of size , where n is the number of variables and and is the number of variables that can be resolved multiple times.

Place, publisher, year, edition, pages
Springer, 2017. Vol. 79, no 1, p. 29-41
Keywords [en]
Satisfiability, Resolution, Strong ETH
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-211585DOI: 10.1007/s00453-016-0228-6ISI: 000405908000003Scopus ID: 2-s2.0-84991780959OAI: oai:DiVA.org:kth-211585DiVA, id: diva2:1133399
Funder
EU, FP7, Seventh Framework Programme, 279611
Note

QC 20170815

Available from: 2017-08-15 Created: 2017-08-15 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Bonacina, Ilario
By organisation
Theoretical Computer Science, TCS
In the same journal
Algorithmica
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 31 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf