Solution to Set of SAT Problems

In practical applications,we always need to resolve a series SAT(Satisfiability Problem) problems which only differ in a few clauses between corresponding CNF(Conjunctive Normal Form) formulas.However,most of current SAT solving algorithms are designed for single SAT problem.An algorithm is proposed which is based on DPLL and can solve a set of SAT problems at a time.Tests on random problems demonstrated that: nDPLL algorithm reflects high efficiency on some CNF formulas;the efficiency of nDPLL is proportional to the size of CNF formulas,close factor and the ratio between the number of clauses and variables.