SAT solver based on advanced forward reasoning

This paper proposes a new Propositional Satisfiability Problem (SAT) solver which combined the Failed Literal Detection(FLD), one of the advanced forward reasoning technologies and Davis Putnam Logemann and Loveland(DPLL). This SAT solver utilizes double testing of FLD, First, apply Symmetric Extended Unit Propagation(SEUP) to find the failed literal deeply and conjecture more connotative relations among them, then apply the DYN filtration algorithm which based on the FLD to the results of previous step. The algorithm can search more failed literal on each decision-making layer and the experimental results confirms that. The SAT solver not only can improve the efficiency of FLD but also can solve the difficult satisfiability problems independently without further reasoning.