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 SATs 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.
Propositional satisfiability problem SAT Np-Complete Algorithms.
Juan Segura-Salazar Juan Frausto-Solís
Genomic Science Center, UNAM, P.O. Box 565-A, Av. Universidad s/n, C.P. 62210, Cuernavaca Morelos, M ITESM, Cuernavaca Campus, A.P. 99-C, Paseo de la Reforma 182-A, C.P. 62589, Cuernavaca Morelos, Méxi
国际会议
The 2007 International Conference on Intelligent Systems and Knowledge Engineering(第二届智能系统与知识工程国际会议)
成都
英文
226-231
2007-10-15（万方平台首次上网日期，不代表论文的发表时间）