ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES
From MaRDI portal
Publication:5148102
DOI10.1017/jsl.2019.53zbMath1497.68218OpenAlexW3035897643MaRDI QIDQ5148102
Dmitry Itsykson, Alexander Knop, Andrei Romashchenko, Dmitry Sokolov
Publication date: 29 January 2021
Published in: The Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2017/6991/
Linear codes (general theory) (94B05) Complexity of proofs (03F20) Computational aspects of satisfiability (68R07) Communication complexity, information complexity (68Q11)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the complexity of cutting-plane proofs
- Symbolic techniques in satisfiability solving
- A direct construction of polynomial-size OBDD proof of pigeon hole problem
- Ramanujan graphs
- Resolution and binary decision diagrams cannot simulate each other polynomially
- On multi-partition communication complexity
- Explicit construction of linear sized tolerant networks. (Reprint)
- Expander graphs and their applications
- List decoding from erasures: bounds and code constructions
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for cutting planes proofs with small coefficients
- Branching Programs and Binary Decision Diagrams
- On expander codes
- On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables
- Communication Complexity
- Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams
- On the complexity of constructing optimal ordered binary decision diagrams
- An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
- Principles and Practice of Constraint Programming – CP 2004
