On obdd-based algorithms and proof systems that dynamically change the order of variables

Standard

On obdd-based algorithms and proof systems that dynamically change the order of variables. / Itsykson, Dmitry; Knop, Alexander; Romashchenko, Andrei; Sokolov, Dmitry.

In: Journal of Symbolic Logic, Vol. 85, No. 2, 06.2020, p. 632-670.

Research output: Contribution to journal › Article › peer-review

BibTeX

@article{b33b69146a0149d4ac66754ea22928cc,

title = "On obdd-based algorithms and proof systems that dynamically change the order of variables",

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

keywords = "communication complexity, error correcting codes, OBDD, proof complexity, satisfiability algorithms",

author = "Dmitry Itsykson and Alexander Knop and Andrei Romashchenko and Dmitry Sokolov",

note = "Funding Information: Acknowledgments. The authors are grateful to Sam Buss for fruitful discussions and to the anonymous reviewers for useful comments. The research presented in Sections 3, 4, and 5 was supported by Russian Science Foundation (project 16-11-10123). The work of the third author on the research presented in Section 6 was partially supported by RFBR grant 19-01-00563. Dmitry Itsykson is a Young Russian Mathematics award winner and would like to thank sponsors and jury of the contest. Publisher Copyright: {\textcopyright} 2020 Cambridge University Press. All rights reserved. Copyright: Copyright 2021 Elsevier B.V., All rights reserved.",

year = "2020",

month = jun,

doi = "10.1017/jsl.2019.53",

language = "English",

volume = "85",

pages = "632--670",

journal = "Journal of Symbolic Logic",

issn = "0022-4812",

publisher = "Cambridge University Press",

number = "2",

}

RIS

TY - JOUR

T1 - On obdd-based algorithms and proof systems that dynamically change the order of variables

AU - Itsykson, Dmitry

AU - Knop, Alexander

AU - Romashchenko, Andrei

AU - Sokolov, Dmitry

N1 - Funding Information: Acknowledgments. The authors are grateful to Sam Buss for fruitful discussions and to the anonymous reviewers for useful comments. The research presented in Sections 3, 4, and 5 was supported by Russian Science Foundation (project 16-11-10123). The work of the third author on the research presented in Section 6 was partially supported by RFBR grant 19-01-00563. Dmitry Itsykson is a Young Russian Mathematics award winner and would like to thank sponsors and jury of the contest. Publisher Copyright: © 2020 Cambridge University Press. All rights reserved. Copyright: Copyright 2021 Elsevier B.V., All rights reserved.

PY - 2020/6

Y1 - 2020/6

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

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

KW - communication complexity

KW - error correcting codes

KW - OBDD

KW - proof complexity

KW - satisfiability algorithms

UR - http://www.scopus.com/inward/record.url?scp=85100132552&partnerID=8YFLogxK

U2 - 10.1017/jsl.2019.53

DO - 10.1017/jsl.2019.53

M3 - Article

AN - SCOPUS:85100132552

VL - 85

SP - 632

EP - 670

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

SN - 0022-4812

IS - 2

ER -

ID: 75310429