Search

In 2004 Atserias, Kolaitis, and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of an identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based proof systems that additionally contain a rule that allows changing the order in OBDDs. At first we consider a proof system OBDD(\∧, reordering) that uses the conjunction (join) rule and the rule that allows changing the order. We exponentially separate this proof system from OBDD(∧) proof system that uses only the conjunction rule. We prove exponential lower bounds on the size of OBDD(∧, reordering) refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(∧) proofs and the second one extends the result of Tveretina et al. from OBDD(∧) to OBDD(∧, reordering). In 2001 Aguirre and Vardi proposed an approach to the propositional satisfiability problem based on OBDDs and symbolic quantifier elimination (we denote algorithms based on this approach as OBDD(∧, ∃) algorithms). We augment these algorithms with the operation of reordering of variables and call the new scheme OBDD(∧, ∃, reordering) algorithms. We notice that there exists an OBDD(∧, \exists) algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time (a standard example of a hard system of linear equations over F2), but we show that there are formulas representing systems of linear equations over F2 that are hard for OBDD(∧, \exists , reordering) algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F2 that correspond to checksum matrices of error correcting codes. [ABSTRACT FROM AUTHOR]

The relativized weak pigeonhole principle states that if at least 2n out of n2 pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle requires size $2^{\left( {{\rm{log\ }}n} \right)^{3/2 - \varepsilon } } $ for every ε﹥0 and every sufficiently large n. By reducing it to the standard weak pigeonhole principle with 2n pigeons and n holes, we also show that this lower bound is essentially tight in that there exist DNF-refutations of size $2^{\left( {{\rm{log\ }}n} \right)^{O\left( 1 \right)} } $ even in R(log). For the lower bound proof we need to discuss the existence of unbalanced low-degree bipartite expanders satisfying a certain robustness condition. [ABSTRACT FROM PUBLISHER]

We 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. [ABSTRACT FROM AUTHOR]

We give an exponential lower bound on number of proof-lines in the proof system K of modal logic, i.e., we give an example of K-tautologies ψ1, ψ2.... s.t. every K-proof of ψi must have a number of proof-lines exponential in terms of the size of ψi. The result extends, for the same sequence of K-tautologies, to the systems K4. Gödel-Löb's logic, S and S4. We also determine some speed-up relations between different systems of modal logic on formulas of modal-depth one. [ABSTRACT FROM AUTHOR]