关键词:  自动推理, DPLL算法, 可满足性

Abstract:

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.

Key words: automated reasoning, DPLL algorithm, satisfiability