Integrating advanced reasoning into a SAT solver

In this paper, we present a SAT solver based on the combination of DPLL (Davis Putnam Logemann and Loveland) algorithm and Failed Literal Detection (FLD), one of the advanced reasoning techniques. We propose a Dynamic Filtering method that consists of two restriction rules for FLD: internal and external filtering. The method reduces the number of tested literals in FLD and its computational time while maintaining the ability to find most of the failed literals in each decision level. Unlike the pre-defined criteria, literals are removed dynamically in our approach. In this way, our FLD can adapt itself to different real-life benchmarks. Many useless tests are therefore avoided and as a consequence it makes FLD fast. Some other static restrictions are also added to further improve the efficiency of FLD. Experiments show that our optimized FLD is much more efficient than other advanced reasoning techniques.