Using Decision Diagrams of Special Kind for Compactification of Conflict Data Bases Generated by CDCL SAT Solvers

摘要

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.