Show simple item record

Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond

dc.contributor.authorTveretina, Olga
dc.contributor.authorSinz, Carsten
dc.contributor.authorZantema, Hans
dc.date.accessioned2013-01-15T16:59:06Z
dc.date.available2013-01-15T16:59:06Z
dc.date.issued2010
dc.identifier.citationTveretina , O , Sinz , C & Zantema , H 2010 , ' Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond ' , Journal on Satisfiability, Boolean Modeling and Computation , vol. 7 , no. 1 , pp. 35-58 .
dc.identifier.urihttp://hdl.handle.net/2299/9664
dc.description.abstractGroote 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.en
dc.format.extent561727
dc.language.isoeng
dc.relation.ispartofJournal on Satisfiability, Boolean Modeling and Computation
dc.subjectordered binary decision diagrams, resolution, pigeonhole formulas, lower bounds
dc.titleOrdered Binary Decision Diagrams, Pigeonhole Formulas and Beyonden
dc.contributor.institutionSchool of Physics, Engineering & Computer Science
dc.contributor.institutionBiocomputation Research Group
dc.contributor.institutionDepartment of Computer Science
dc.description.statusPeer reviewed
rioxxterms.typeJournal Article/Review
herts.preservation.rarelyaccessedtrue


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record