You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond1

Article type: Research Article

Authors: Tveretina, Olgaa | Sinz, Carstena | Zantema, Hansb

Affiliations: [a] Institute for Theoretical Computer Science, Karlsruhe Institute of Technology (KIT), Germany. E-mails: olga.tveretina@kit.edu, carsten.sinz@kit.edu | [b] Department of Computer Science, TU Eindhoven Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands. E-mail: h.zantema@tue.nl

Note: [1] This work was supported in part by the “Concept for the Future” of Karlsruhe Institute of Technology within the framework of the German Excellence Initiative.

Keywords: ordered binary decision diagrams, resolution, pigeonhole formulas, lower bounds

DOI: 10.3233/SAT190074

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 1, pp. 35-58, 2010

Received 1 October 2009
|
Revision received 1 March 2010
|
Published: 1 March 2010
Get PDF open access

Abstract

Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has exponential size, and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that an arbitrary OBDD refutation of the pigeonhole formula has exponential size: we prove that for any order of computation at least one intermediate OBDD in the proof has size Ω(1.14n). We also present a family of CNFs that show an exponential blow-up for all OBDD refutations compared to unrestricted resolution refutations.

Show more