On Obdd-Based Algorithms And Proof Systems That Dynamically Change The Order Of Variables

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(boolean AND, reordering) that uses the conjunction (join) rule and the rule that allows changing the order. We exponentially separate this proof system from OBDD(boolean AND) proof system that uses only the conjunction rule. We prove exponential lower bounds on the size of OBDD (boolean AND, reordering) refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(boolean AND) proofs and the second one extends the result of Tveretina et al. from OBDD(boolean AND) to OBDD(boolean AND, 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(boolean AND, 3) algorithms). We augment these algorithms with the operation of reordering of variables and call the new scheme OBDD(boolean AND, 3, reordering) algorithms. We notice that there exists an OBDD(boolean AND, there exists) algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time (a standard example of a hard system of linear equations over F-2), but we show that there are formulas representing systems of linear equations over F-2 that are hard for OBDD(boolean AND, there exists, reordering) algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F-2 that correspond to checksum matrices of error correcting codes.