Using Decision Diagrams of Special Kind for Compactification of Conflict Data Bases Generated by CDCL SAT Solvers
Viktor V. Kondratiev, Ilya V. Otpuschennikov, Alexander Alexeevich Semenov · 2020
In the paper we propose new algorithms for constructing compact representations of databases of conflict clauses accumulated by state-of-the-art CDCL SAT solvers. These algorithms use the Decision Diagrams of a special kind (the so-called Disjunctive Diagrams). We consider several families of hard SAT instances and use them to compare the implementations of the proposed algorithms and the well-known CUDD package that uses Zero-Suppressed Binary Decision Diagrams (ZBDD) for solving similar problems. The computational experiments clearly show that our algorithm that uses Disjunctive Diagrams has better effectiveness compared to CUDD.