Transforming The DPLL To (1,1)-resolution And Its Complexity Analysis

The satisfiability problem (SAT problem) of propositional formulas refers to satisfiability problem of boolean formulas, a major problem in theoretical computer science, which can be widely used in such fields as symbolic logic, artificial intelligence, constraint satisfaction problem, design and detection of VLSI integrate circuit, and theories of computer science. SAT problem is the first NP-complete problem and the nucleus of the category of NP-complete problems. A CNF formula is the conjunction of finite clauses. (r,s) — CNF formulas mean all the CNF formulas that contain r variables and every variable occurs at most s times, (r, s) — SAT is the propositional satisfiability problem instances in (r,s) — CNF. A SAT algorithm can determine whether any given CNF formula is satisfiable in limited time. DPLL algorithm and resolution refutation are two key methods resolving SAT problems. Olga Tveretina and Hans Zantema have analyzed in details the transformation from DPLL algorithm to resolution, improving that if in the DPLL procedure s unit resolution steps are executed and r recursive calls are done, a resolution refutation exists of length at most s — r, being essentially better than s. As we know, for any formula in MU(1), there is a corresponding (1, 1)-resolution refutation. Research of minimal unsatisfiable formulas is the focus problems that have emerged in recent years, on which Germany scholars such as H. Kleine Buening , O. Kullmann etc. have done much work . Some structures and properties of minimal unsatisfiable formulas will promote research of algorithm of solving SAT.Through studying tree resolution proofs of minimal unsatisfiable formulas and splitting of minimal unsatisfiable formulas, we constructs minimal unsatisfiable instances in (r, s) — SAT and presents some minimal unsatisfiable NP-complete instances in (r, s) — SAT in this paper.Furthermore, on the basis of construction method of minimal unsatisfiable formulas, a concrete transformative method from resolution proof to (1, 1)-resolution proof is found, and accordingly getting a transformation from DPLL algorithm to (1, 1)-resolution proof.