Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond1 | Zendy

Olga Tveretina | Zendy; Carsten Sinz | Zendy; Hans Zantema | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond1

Author(s) -

Olga Tveretina,

Carsten Sinz,

Hans Zantema

Publication year - 2010

Publication title -

journal on satisfiability boolean modeling and computation

Language(s) - English

Resource type - Journals

eISSN - 1875-5011

pISSN - 1574-0617

DOI - 10.3233/sat190074

Subject(s) - pigeonhole principle , binary decision diagram , computation , exponential function , resolution (logic) , mathematics , binary number , conjunctive normal form , discrete mathematics , order (exchange) , combinatorics , algorithm , computer science , arithmetic , mathematical analysis , artificial intelligence , finance , economics

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.14 n ). We also present a family of CNFs that show an exponential blow-up for all OBDD refutations compared to unrestricted resolution refutations.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research