An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams.

*(English)*Zbl 1141.03028The main result of the paper is an exponential lower bound on the size of proofs in a propositional proof system operating with ordered binary decision diagrams (OBDD), introduced by A. Atserias, P. Kolaitis and M. Vardi [“Constraint propagation as proof system”, Lect. Notes Comput. Sci. 3258, 77–91 (2004)]. A variant of feasible interpolation holds for OBDD refutations as a corollary to the author’s feasible interpolation theorem for semantic derivations [J. Symb. Log. 62, No. 2, 457–486 (1997; Zbl 0891.03029)], which implies a lower bound for a variant of clique/color tautologies with respect to OBDD refutations using a specific ordering of the variables. The author then applies a substitution, which has the effect of introducing a permutation of input variables, and obtains an exponential lower bound on arbitrary OBDD refutations.

Reviewer: Emil Jeřábek (Praha)

##### MSC:

03F20 | Complexity of proofs |

##### Keywords:

propositional proof system; lower bound; ordered binary decision diagrams; feasible interpolation; communication complexity; proof complexity; constraint propagation**OpenURL**

##### References:

[1] | Branching programs and binary decision diagrams – theory and applications (2000) · Zbl 0956.68068 |

[2] | Lower bounds to the size of constant-depth propositional proofs 59 pp 73– (1994) · Zbl 0798.03056 |

[3] | Izvestiya of the R.A.N. 59 pp 201– (1995) |

[4] | Logic in computer science pp 220– (1994) |

[5] | Constraint processing (2003) |

[6] | The relative efficiency of propositional proof systems 44 pp 36– (1979) · Zbl 0408.03044 |

[7] | ACM Computing Surveys 2493 pp 293– (1992) |

[8] | IEEE Transactions on Computing 35 pp 677– (1986) |

[9] | Lower bounds for cutting planes proofs with small coefficients pp 708– (1997) |

[10] | 10th Int. Conf. on Principles and Practice of Constraint Programing 3258 pp 77– (2004) |

[11] | DOI: 10.1007/BF02579196 · Zbl 0631.68041 |

[12] | Handbook of proof theory pp 547– (1998) |

[13] | Lower bounds for resolution and cutting plane proofs and monotone computations pp 981– (1997) |

[14] | Communication complexity (1996) |

[15] | Logic and computational complexity (Proc. of the meeting held in Indianapolis, October 1994) 140 pp 82– (1998) |

[16] | DOI: 10.4064/fm170-1-8 · Zbl 0987.03051 |

[17] | Discretely ordered modules as a first-order extension of the cutting planes proof system 63 pp 1582– (1998) |

[18] | Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic 62 pp 457– (1997) · Zbl 0891.03029 |

[19] | Bounded arithmetic, propositional logic, and complexity theory 60 (1995) |

[20] | The complexity of Boolean functions (1987) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.