On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables

Autor: Dmitry Itsykson, Alexander Knop, Andrei Romashchenko, Dmitry Sokolov
Přispěvatelé: St. Petersburg Department of V.A. Steklov Mathematical Institute (PDMI RAS), Steklov Mathematical Institute [Moscow] (SMI), Russian Academy of Sciences [Moscow] (RAS)-Russian Academy of Sciences [Moscow] (RAS), Systèmes complexes, automates et pavages (ESCAPE), Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), ANR-15-CE40-0016,RaCAF,Dépasser les frontières de l'aléatoire et du calculable(2015), Steklov Mathematical Institute (SMI), Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)
Jazyk: angličtina
Rok vydání: 2017
Předmět:
[INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC]
TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES
Logic
Computer science
error-correcting codes
Existential quantification
02 engineering and technology
0102 computer and information sciences
[INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM]
Computer Science::Artificial Intelligence
Computer Science::Computational Complexity
System of linear equations
Mathematical proof
01 natural sciences
Computer Science::Logic in Computer Science
Quantifier elimination
ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION
0202 electrical engineering
electronic engineering
information engineering
communication complexity
0101 mathematics
Time complexity
expanders
000 Computer science
knowledge
general works
Proof complexity
Pigeonhole principle
010102 general mathematics
[MATH.MATH-IT]Mathematics [math]/Information Theory [math.IT]
020206 networking & telecommunications
OBDD
Philosophy
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
Tseitin formulas
Computer Science
Boolean satisfiability problem
Algorithm
Hardware_LOGICDESIGN
Zdroj: 34th Symposium on Theoretical Aspects of Computer Science
STACS: Symposium on Theoretical Aspects of Computer Science
STACS: Symposium on Theoretical Aspects of Computer Science, Mar 2017, Hannover, Germany. pp.43:1-43:14, ⟨10.4230/LIPIcs.STACS.2017.43⟩
The Journal of Symbolic Logic
The Journal of Symbolic Logic, Association for Symbolic Logic, In press, pp.1-41. ⟨10.1017/jsl.2019.53⟩
The Journal of Symbolic Logic, Association for Symbolic Logic, 2020, 85 (2), pp.632-670. ⟨10.1017/jsl.2019.53⟩
ISSN: 0022-4812
1943-5886
DOI: 10.4230/lipics.stacs.2017.43
Popis: In 2004 Atserias, Kolaitis, and Vardi proposed $\text {OBDD}$ -based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of an identically false $\text {OBDD}$ from $\text {OBDD}$ s representing clauses of the initial formula. All $\text {OBDD}$ s in such proofs have the same order of variables. We initiate the study of $\text {OBDD}$ based proof systems that additionally contain a rule that allows changing the order in $\text {OBDD}$ s. At first we consider a proof system $\text {OBDD}(\land , \text{reordering})$ that uses the conjunction (join) rule and the rule that allows changing the order. We exponentially separate this proof system from $\text {OBDD}(\land )$ proof system that uses only the conjunction rule. We prove exponential lower bounds on the size of $\text {OBDD}(\land , \text{reordering})$ refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for $\text {OBDD}(\land )$ proofs and the second one extends the result of Tveretina et al. from $\text {OBDD}(\land )$ to $\text {OBDD}(\land , \text{reordering})$ .In 2001 Aguirre and Vardi proposed an approach to the propositional satisfiability problem based on $\text {OBDD}$ s and symbolic quantifier elimination (we denote algorithms based on this approach as $\text {OBDD}(\land , \exists )$ algorithms). We augment these algorithms with the operation of reordering of variables and call the new scheme $\text {OBDD}(\land , \exists , \text{reordering})$ algorithms. We notice that there exists an $\text {OBDD}(\land , \exists )$ algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time (a standard example of a hard system of linear equations over $\mathbb {F}_2$ ), but we show that there are formulas representing systems of linear equations over $\mathbb {F}_2$ that are hard for $\text {OBDD}(\land , \exists , \text{reordering})$ algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over $\mathbb {F}_2$ that correspond to checksum matrices of error correcting codes.
Databáze: OpenAIRE
Externí odkaz: