An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
2008 ◽
Vol 73
(1)
◽
pp. 227-237
◽
Keyword(s):
AbstractWe prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular format of proofs or ordering of variables, the hard formulas are in CNF. We utilize (somewhat indirectly) feasible interpolation.We define a proof system combining resolution and the OBDD proof system.
2015 ◽
Vol 59
(3)
◽
pp. 532-559
◽
1993 ◽
Vol 03
(01)
◽
pp. 3-12
◽
2000 ◽
Vol 103
(1-3)
◽
pp. 237-258
◽
2010 ◽
Vol 7
(1)
◽
pp. 35-58
◽
1999 ◽
Vol 09
(03n04)
◽
pp. 181-198
◽
2006 ◽
Vol 98
(1)
◽
pp. 6-10
◽