Authors:
- Tom van Dijk
- Rüdiger Ehlers
- Armin Biere
Published in: CoRR
Abstract:
Symbolic variants of clause distribution using decision diagrams to eliminate variables in SAT were shown to perform well on hard combinatorial instances. In this paper we revisit both existing ZDD and BDD variants of this approach. We further investigate different heuristics for selecting the next variable to eliminate. Our implementation makes further use of parallel features of the open source BDD library Sylvan.
BibTeX entry:
@article{DijkEB18,
arxiv = {1805.03496},
author = {Tom van Dijk and Rüdiger Ehlers and Armin Biere},
journal = {CoRR},
title = {Revisiting Decision Diagrams for {SAT}},
volume = {abs/1805.03496},
year = {2018}
}