To Meet The Simplification Of The Problem Of Algorithm Research-cnf

Boolean Satisfiability Problem (SAT) is a problem of solving boolean expression to find out if it can be satisfied. Boolean expression can always be translated into Conjunctive Normal Form (CNF). This paper introduces the author's work on SAT algorithms and also a strategy to simplify the CNF to improve the performance of SAT solving.SAT is used in many modern applications, for example in the field of Electronic Design Automation (EDA), the formal verification that checks the equivalence of logic circuits often uses the SAT solver as engine. Due to the high complexity and high repetitiveness of cirsuits, this paper tries to use the Boolean expression implication and reduction formula to simplify the CNF to improve the performance of SAT solver. The program is written in C++ with Standard Template Library (STL). It converts the original CNF to a simplified CNF, and use Zchaff to solve the new CNF so as to improve the solver's performance. The experiment shows that the program successfully reduces the sizes of CNFs and and time of simplifying plus the time Zchaff solves the new CNF is smaller than the time that Zchaff uses to solve the original CNF.