Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
On OBDD-based algorithms and proof systems that dynamically change order of variables. / Itsykson, Dmitry; Knop, Alexander; Romashchenko, Andrey; Sokolov, Dmitry.
34th Symposium on Theoretical Aspects of Computer Science, STACS 2017. ed. / Brigitte Vallee; Heribert Vollmer. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2017. 43 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 66).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - On OBDD-based algorithms and proof systems that dynamically change order of variables
AU - Itsykson, Dmitry
AU - Knop, Alexander
AU - Romashchenko, Andrey
AU - Sokolov, Dmitry
PY - 2017/3/1
Y1 - 2017/3/1
N2 - In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of 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 to change the order in OBDDs. At first we consider a proof system OBDD(∧, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separate this proof system from OBDD(∧)-proof system that uses only the conjunction rule. We prove two 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 2004 Pan 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 notice that there exists an OBDD(∧,∃)-algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over F2 that are hard for OBDD(∧, ∃,reordering)-algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F2 that correspond to some checksum matrices of error correcting codes.
AB - In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of 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 to change the order in OBDDs. At first we consider a proof system OBDD(∧, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separate this proof system from OBDD(∧)-proof system that uses only the conjunction rule. We prove two 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 2004 Pan 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 notice that there exists an OBDD(∧,∃)-algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time. In contrast, we show that there exist formulas representing systems of linear equations over F2 that are hard for OBDD(∧, ∃,reordering)-algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over F2 that correspond to some checksum matrices of error correcting codes.
KW - Error-correcting codes
KW - Expanders
KW - OBDD
KW - Proof complexity
KW - Tseitin formulas
UR - http://www.scopus.com/inward/record.url?scp=85016185155&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.STACS.2017.43
DO - 10.4230/LIPIcs.STACS.2017.43
M3 - Conference contribution
AN - SCOPUS:85016185155
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017
A2 - Vallee, Brigitte
A2 - Vollmer, Heribert
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017
Y2 - 8 March 2017 through 11 March 2017
ER -
ID: 49785466