Resolution and binary decision diagrams cannot simulate each other polynomially
type: Item
instance of: scholarly article
title: Resolution and binary decision diagrams cannot simulate each other polynomially
zbMATH Open document ID: 1029.68129
DOI: 10.1016/S0166-218X(02)00403-1
author: Jan Friso Groote
author: Hans Zantema
published in: Discrete Applied Mathematics
publication date: 2003-09-15T00:00:00Z
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 03B05
zbMATH DE Number: 1981506
zbMATH Keywords: propositional logic
zbMATH Keywords: binary decision diagrams
MaRDI profile type: Publication
cites work: Short proofs are narrow -- resolution made simple
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
cites work: The complexity of theorem-proving procedures
cites work: Q4133141
cites work: A machine program for theorem-proving
cites work: Davis-Putnam resolution versus unrestricted resolution
cites work: Q3043797
cites work: The intractability of resolution
cites work: GRASP: a search algorithm for propositional satisfiability
cites work: Q4388806
cites work: Q4152212
cites work: Q5593816
cites work: Ordered Binary Decision Diagrams and the Davis-Putnam procedure
cites work: Hard examples for resolution
cites work: The Complexity of Propositional Proofs
cites work: A rewriting approach to binary decision diagrams
full work available at URL: s0166-218x(02)00403-1
OpenAlex ID: W3022749232
description: scientific article; zbMATH DE number 1981506