RECORD
Resolution Simulates Ordered Binary Decision Diagrams for Formulas in Conjunctive Normal Form
Logic in Computer Science · Submitted 9 Jan 2017
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim Contrary to popular belief, we argue that resolution simulates OBDDs polynomially if we limit both to CNFs and thus answer negatively the open question of Groote and Zantema whether there exist unsatisfiable CNFs having polynomial OBDD refutations and requiring exponentially long resolution refutations.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
A classical question of propositional logic is one of the shortest proof of a tautology. A related fundamental problem is to determine the relative efficiency of standard proof systems, where the relative complexity is measured using the notion of polynomial simulation. Presently, the state-of-the-art satisfiability algorithms are based on resolution in combination with search. An Ordered Binary Decision Diagram (OBDD) is a data structure that is used to represent Boolean functions. Groote and Zantema have proved that there is exponential separation between resolution and a proof system based on limited OBDD derivations. However, formal comparison of these methods is not straightforward because OBDDs work on arbitrary formulas, whereas resolution can only be applied to formulas in Conjunctive Normal Form (CNFs). Contrary to popular belief, we argue that resolution simulates OBDDs polynomially if we limit both to CNFs and thus answer negatively the open question of Groote and Zantema whether there exist unsatisfiable CNFs having polynomial OBDD refutations and requiring exponentially long resolution refutations.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | A classical question of propositional logic is one of the shortest proof of a tautology. | background 1.00 | 0.03 | 0.01 | asserted 0.97 |
| s1 | A related fundamental problem is to determine the relative efficiency of standard proof systems, where the relative complexity is measured using the notion of polynomial simulation. | background 1.00 | 0.04 | 0.02 | asserted 0.99 |
| s2 | Presently, the state-of-the-art satisfiability algorithms are based on resolution in combination with search. | background 1.00 | 0.04 | 0.02 | asserted 1.00 |
| s3 | An Ordered Binary Decision Diagram (OBDD) is a data structure that is used to represent Boolean functions. | background 1.00 | 0.04 | 0.02 | asserted 1.00 |
| s4 | Groote and Zantema have proved that there is exponential separation between resolution and a proof system based on limited OBDD derivations. | background 0.98 | 0.02 | 0.03 | asserted 1.00 |
| s5 | However, formal comparison of these methods is not straightforward because OBDDs work on arbitrary formulas, whereas resolution can only be applied to formulas in Conjunctive Normal Form (CNFs). | gap 0.70 | 0.05 | 0.03 | asserted 0.99 |
| s6 | Contrary to popular belief, we argue that resolution simulates OBDDs polynomially if we limit both to CNFs and thus answer negatively the open question of Groote and Zantema whether there exist unsatisfiable CNFs having polynomial OBDD refutations and requiring exponentially long resolution refutations. | result 0.85 | 0.79 | 0.96 | asserted 0.88 |
What was examined, and what was not
- arXiv listing abstract v3
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
A classical question of propositional logic is one of the shortest proof of a tautology. A related fundamental problem is to determine the relative efficiency of standard proof systems, where the relative complexity is measured using the notion of polynomial simulation. Presently, the state-of-the-art satisfiability algorithms are based on resolution in combination with search. An Ordered Binary Decision Diagram (OBDD) is a data structure that is used to represent Boolean functions. Groote and Zantema have proved that there is exponential separation between resolution and a proof system based on limited OBDD derivations. However, formal comparison of these methods is not straightforward because OBDDs work on arbitrary formulas, whereas resolution can only be applied to formulas in Conjunctive Normal Form (CNFs). Contrary to popular belief, we argue that resolution simulates OBDDs polynomially if we limit both to CNFs and thus answer negatively the open question of Groote and Zantema whether there exist unsatisfiable CNFs having polynomial OBDD refutations and requiring exponentially long resolution refutations.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.