Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver
The work
| Authors | Randal E. Bryant; Marijn J. H. Heule |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2021 |
| Citekey | bryant2021dual |
Where it appeared
| Published in | Automated Deduction (CADE 2021) |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Artificial Intelligence |
| Volume | 12699 |
| Pages | 433--449 |
Access
| Landing page | https://www.cs.cmu.edu/~bryant/pubdir/cade21.pdf |
|---|
Related
| Distinct from | andrici2019verifying |
|---|---|
| Distinct from | bryant1986graphbased |
| Distinct from | davis2013verified |
| Distinct from | jacobi2005automatic |
| Distinct from | nukala2024translating |
| Distinct from | oleary2013relational |
| Distinct from | slobodova2011flexible |
From bibtex.
Abstract
Existing proof-generating quantified Boolean formula (QBF) solvers must construct a different type of proof depending on whether the formula is false (refutation) or true (satisfaction). We show that a QBF solver based on ordered binary decision diagrams (BDDs) can emit a single dual proof as it operates, supporting either outcome. This form consists of a sequence of equivalence-preserving clause addition and deletion steps in an extended resolution framework. For a false formula, the proof terminates with the empty clause, indicating conflict. For a true one, it terminates with all clauses deleted, indicating tautology. Both the length of the proof and the time required to check it are proportional to the total number of BDD operations performed. We evaluate our solver using a scalable benchmark based on a two-player tiling game.
A copy is held
pdf, 285.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 23:53 UTC |
| Approved by | a person 2026-09-17 17:06 UTC |
Filed under
Cite it as
@inproceedings{bryant2021dual,
title = {Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver},
author = {Randal E. Bryant and Marijn J. H. Heule},
year = {2021},
booktitle = {Automated Deduction (CADE 2021)},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
volume = {12699},
pages = {433--449},
}
This record lives at https://refs.drheap.org/bryant2021dual/ and will keep doing so.