Revisiting Decision Diagrams for SAT

Tom van Dijk, Rüdiger Ehlers, Armin Biere

Research output: Working paperPreprintAcademic

5 Downloads (Pure)

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.
Original languageEnglish
Publication statusPublished - 9 May 2018
Externally publishedYes

Keywords

  • cs.LO

Fingerprint

Dive into the research topics of 'Revisiting Decision Diagrams for SAT'. Together they form a unique fingerprint.

Cite this