A Partition Rule for SAT Solvers: The Multiple Partition Rule (MPR)
- 10.2991/iske.2007.225How to use a DOI?
- satisfiability, SAT, Np-Complete, Algorithms, MPR
We propose a new partition rule for DPLL-based SAT Solvers. Most of the complete SAT solver 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.
- © 2007, the Authors. Published by Atlantis Press.
- Open Access
- This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).
Cite this article
TY - CONF AU - Juan Segura-Salazar AU - Juan Frausto-Solís PY - 2007/10 DA - 2007/10 TI - A Partition Rule for SAT Solvers: The Multiple Partition Rule (MPR) BT - Proceedings of the 2007 International Conference on Intelligent Systems and Knowledge Engineering (ISKE 2007) PB - Atlantis Press SP - 1325 EP - 1330 SN - 1951-6851 UR - https://doi.org/10.2991/iske.2007.225 DO - 10.2991/iske.2007.225 ID - Segura-Salazar2007/10 ER -