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
Reordering rule makes OBDD proof systems stronger
KTH, School of Electrical Engineering and Computer Science (EECS), Theoretical Computer Science, TCS.
2018 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2018, p. 161-1624Conference paper, Published paper (Refereed)
Abstract [en]

Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(∧, weakening), simulates CP∗ (Cutting Planes with unary coefficients). We show that OBDD(∧, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD(∧, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD (∧, weakening, reordering) is strictly stronger than OBDD(∧, weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD(∧) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolve an open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results, we completely analyze which of the systems among CP∗, OBDD(∧), OBDD(∧, reordering), OBDD(∧, weakening) and OBDD (∧, weakening, reordering) polynomially simulate each other. For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.

Place, publisher, year, edition, pages
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2018. p. 161-1624
Keywords [en]
Lifting theorems, OBDD, Proof complexity, The Clique-Coloring principle, Tseitin formulas
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:kth:diva-238217DOI: 10.4230/LIPIcs.CCC.2018.16Scopus ID: 2-s2.0-85048982223ISBN: 9783959770699 (print)OAI: oai:DiVA.org:kth-238217DiVA, id: diva2:1264169
Conference
33rd Computational Complexity Conference, CCC 2018, San Diego, United States, 22 June 2018 through 24 June 2018
Note

QC 20181119

Available from: 2018-11-19 Created: 2018-11-19 Last updated: 2018-11-19Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Sokolov, Dmitry
By organisation
Theoretical Computer Science, TCS
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 248 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