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

DOI

10.2991/iske.2007.225How to use a DOI?

Keywords

satisfiability, SAT, Np-Complete, Algorithms, MPR

Abstract

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.

Copyright

© 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/).

Download article (PDF)

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  -