A comprehensive study and analysis on SAT-solvers: advances, usages and achievements

摘要

Boolean satisfiability (SAT) has been studied for the last twenty years. Advances have been made allowing SAT solvers to be used in many applications including formal verification of digital designs. However, performance and capacity of SAT solvers are still limited. From the practical side, many of the existing applications based on SAT solvers use them as blackboxes in which the problem is translated into a monolithic conjunctive normal form instance and then throw it to the SAT solver with no interaction between the application and the SAT solver. This paper presents a comprehensive study and analysis of the latest developments in SAT-solver and new approaches that used in branching heuristics, Boolean constraint propagation and conflict analysis techniques during the last two decade. In addition, the paper provides the most effective techniques in using SAT solvers as verification techniques, mainly model checkers, to enhance the SAT solver performance, efficiency and productivity. Moreover, the paper presents the remarkable accomplishments and the main challenges facing SAT-solver techniques and contrasts between different techniques according to their efficiency, algorithms, usage and feasibility.