A Partition Rule for SAT Solvers: The Multiple Partition Rule (MPR)

摘要

We propose a new partition rule for DPLL-based SAT Solvers. Most of the complete SAT solvers usually are based on Davis, Logemann and Loveland (DPLL) rules. One most DPLL rule actually used in the modern algorithms is the Classical Partition Rule (CPR), that divides the problem into sub-problems (resolvents) and thereby it finds a solution through a decision tree. In this paper a new partition rule named Multiple Partition Rule (MPR) is presented. MPR generates a new decision tree according to clauses instead CPR which generates a decision tree according to variables. MPR can be used for developing new SAT's algorithms and to improve existence ones that use CPR. Experimental results comparing MPR versus CPR show that using MPR makes more efficient solutions than CPR.