Resolution and binary decision diagrams cannot simulate each other polynomially

DOI10.1016/S0166-218X(02)00403-1zbMath1029.68129OpenAlexW3022749232MaRDI QIDQ1408378

Hans Zantema, Jan Friso Groote

Publication date: 15 September 2003

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0166-218x(02)00403-1

zbMATH Keywords

propositional logicbinary decision diagrams

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Classical propositional logic (03B05)

Related Items

Decomposition representations of logical equations in problems of inversion of discrete functions, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Binary decision diagrams for first-order predicate logic., ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES, Extended resolution simulates binary decision diagrams, Resolution cannot polynomially simulate compressed-BFS, A direct construction of polynomial-size OBDD proof of pigeon hole problem, Generating extended resolution proofs with a BDD-based SAT solver, Unnamed Item, Unnamed Item, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• A rewriting approach to binary decision diagrams
• Davis-Putnam resolution versus unrestricted resolution
• Short proofs are narrow—resolution made simple
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Graph-Based Algorithms for Boolean Function Manipulation
• Hard examples for resolution
• GRASP: a search algorithm for propositional satisfiability
• The Complexity of Propositional Proofs
• Ordered Binary Decision Diagrams and the Davis-Putnam procedure
• A machine program for theorem-proving
• The complexity of theorem-proving procedures