Boolean satisfiability (SAT) is one of the most important problems of theoretical computer
science with many practical applications in which Boolean Satisfiability (SAT) solvers are
used in the background as high-performance reasoning engines. These applications include
automated planning and scheduling, formal verification, and automated theorem proving. In
the last decades, the performance of state-of-the-art SAT solvers has increased dramatically,
thanks to the invention of advanced heuristics, preprocessing and inprocessing techniques,
and data structures that allow efficient implementation of search space pruning. The in-
creasing popularity of SAT in verification and synthesis encourages the search for additional
speed-ups. This paper presents a new approach to support a Conflict Driven Clause Learning
(CDCL) SAT solver with Binary Decision Diagram (BDD) techniques. While SAT and BDD
techniques are often presented as mutually exclusive alternatives, this work points out that
both can be improved by running in parallel and exchanging information. In this thesis, a
BDD library is implemented in Rust, designed to support the latest version of the Glucose
SAT solver. The proposed methods are based on efficient communication between the two
architectures. Several benchmarks from the SAT competitions are run both on Glucose alone
and Glucose with the contribution of the BDDs, and the results are compared. Eventually,
the experiments show that the performance of Glucose is improved when running in parallel
with the BDD solver.
