Resolution and binary decision diagrams cannot simulate each other polynomially

DOI10.1016/S0166-218X(02)00403-1MaRDI QIDQ1408378zbMATH OpenOpenAlexFDO

Authors Jan Friso Groote, Hans Zantema

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

binary decision diagramspropositional logic

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2084326
• Extended resolution simulates binary decision diagrams
• Extended Resolution Proofs for Conjoining BDDs
• Binary decision diagrams for first-order predicate logic.
• Ordered binary decision diagrams and the Davis-Putnam procedure

Cites work

• A machine program for theorem-proving
• A rewriting approach to binary decision diagrams
• Davis-Putnam resolution versus unrestricted resolution
• Graph-Based Algorithms for Boolean Function Manipulation
• GRASP: a search algorithm for propositional satisfiability
• Hard examples for resolution
• scientific article; zbMATH DE number 2084326 (Why is no real title available?)
• scientific article; zbMATH DE number 3557241 (Why is no real title available?)
• scientific article; zbMATH DE number 3583767 (Why is no real title available?)
• scientific article; zbMATH DE number 1150567 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Ordered binary decision diagrams and the Davis-Putnam procedure
• Short proofs are narrow -- resolution made simple
• The Complexity of Propositional Proofs
• The complexity of theorem-proving procedures
• The intractability of resolution

Cited in

(14)

• Binary decision diagrams for first-order predicate logic.
• Resolution cannot polynomially simulate compressed-BFS
• Generating extended resolution proofs with a BDD-based SAT solver
• Extended resolution simulates binary decision diagrams
• scientific article; zbMATH DE number 2084326 (Why is no real title available?)
• Extended Resolution Proofs for Conjoining BDDs
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• Decomposition representations of logical equations in problems of inversion of discrete functions
• scientific article; zbMATH DE number 7250156 (Why is no real title available?)
• scientific article; zbMATH DE number 7300350 (Why is no real title available?)
• scientific article; zbMATH DE number 7300363 (Why is no real title available?)
• ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• A direct construction of polynomial-size OBDD proof of pigeon hole problem

This page was built for publication: Resolution and binary decision diagrams cannot simulate each other polynomially

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1408378)