Revisiting Decision Diagrams for SAT

TL;DR

This paper reevaluates decision diagram techniques for SAT solving, exploring different heuristics and leveraging parallel BDD features to improve performance on complex instances.

Contribution

It introduces new heuristics for variable elimination and utilizes parallel BDD capabilities, enhancing the effectiveness of decision diagram-based SAT solving.

Findings

Decision diagrams can effectively solve hard SAT instances.

Heuristics significantly impact variable elimination efficiency.

Parallel BDD features improve computational performance.

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.