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
Total space in resolution is at least width squared
KTH, School of Computer Science and Communication (CSC).
2016 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2016Conference paper (Refereed)
Abstract [en]

Given an unsatisfiable k-CNF formula φ we consider two complexity measures in Resolution: width and total space. The width is the minimal W such that there exists a Resolution refutation of φ with clauses of at most W literals. The total space is the minimal size T of a memory used to write down a Resolution refutation of φ, where the size of the memory is measured as the total number of literals it can contain. We prove that T = Ω((W - k)2). 1998 ACM Subject Classification F.2.2 Nonnumerical Algorithms and Problems - Complexity of proof procedures.

Place, publisher, year, edition, pages
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2016.
Keyword [en]
Resolution, Total space, Width, Automata theory, Optical resolving power, Trees (mathematics), Complexity measures, Complexity of proof procedures, K-CNF formulas, Nonnumerical algorithms and problems, Resolution refutation, Subject classification, Computational complexity
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-207493DOI: 10.4230/LIPIcs.ICALP.2016.56ScopusID: 2-s2.0-85012894715ISBN: 9783959770132 OAI: oai:DiVA.org:kth-207493DiVA: diva2:1106449
Conference
43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, 12 July 2016 through 15 July 2016
Note

Conference code: 123446; Export Date: 22 May 2017; Conference Paper; Correspondence Address: Bonacina, I.; KTH Royal Institute of Technology, School of Computer Science and CommunicationSweden; email: ilario@kth.se; Funding details: 279611, ERC, European Research Council; Funding text: The author was was partially funded by the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement no. 279611. QC 20170607

Available from: 2017-06-07 Created: 2017-06-07 Last updated: 2017-06-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Bonacina, I.
By organisation
School of Computer Science and Communication (CSC)
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 7 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