Revisiting Decision Diagrams for SAT
Logic in Computer Science
2018-05-10 v1
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.
Keywords
Cite
@article{arxiv.1805.03496,
title = {Revisiting Decision Diagrams for SAT},
author = {Tom van Dijk and Rüdiger Ehlers and Armin Biere},
journal= {arXiv preprint arXiv:1805.03496},
year = {2018}
}