scientific article; zbMATH DE number 7250156
From MaRDI portal
Publication:5121904
DOI10.4230/LIPIcs.CCC.2018.16zbMath1441.03042MaRDI QIDQ5121904
Dmitry Itsykson, Alexander Knop, Dmitry Sokolov, Samuel R. Buss
Publication date: 22 September 2020
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (4)
ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES ⋮ Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs ⋮ On tseitin formulas, read-once branching programs and treewidth ⋮ Proof complexity of symbolic QBF reasoning
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A direct construction of polynomial-size OBDD proof of pigeon hole problem
- Symbolic model checking: \(10^{20}\) states and beyond
- Resolution and binary decision diagrams cannot simulate each other polynomially
- Dag-like communication and its applications
- Hard examples for resolution
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Short proofs are narrow—resolution made simple
- On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables
- Ordered Binary Decision Diagrams and the Davis-Putnam procedure
- On the complexity of constructing optimal ordered binary decision diagrams
- Communication lower bounds via critical block sensitivity
- An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
- The complexity of resolution refinements
- Theory and Applications of Satisfiability Testing
- Principles and Practice of Constraint Programming – CP 2004
This page was built for publication:
