An Algorithm Solving SAT Problem Based on Splitting Rule and Extension Rule

Youjun Xu
Volume: 13, No: 5, Page: 1149 ~ 1157, Year: 2017
10.3745/JIPS.02.0071
Keywords: Extension Rule, IER, MOAMD Strategy, Satisfiability Problem, Splitting Rule
Full Text:

Abstract
The satisfiability problem is always a core problem in artificial intelligence (AI). And how to improve the efficiency of algorithms solving the satisfiability problem is widely concerned. Algorithm IER (Improved Extension Rule) is based on extension rule. The number of atoms and the number of clauses affect the efficiency of the algorithm IER. DPLL rules are helpful to reduce these numbers. Then a complete algorithm CIER based on splitting rule and extension rule is proposed in this paper in order to improve the efficiency. At first, the algorithm CIER (Complete Improved Extension Rule) reduces the scale of a clause set with DPLL rules. Then, the clause set is split into a group of small clause sets. In the end, the satisfiability of the clause set is got from these small clause sets’. A strategy MOAMD (maximum occurrences and maximum difference) for the algorithm CIER is given. With this strategy, a better arrangement of atoms could be got. This arrangement could make the number of small clause sets fewer and the scale of these sets smaller. So, the algorithm CIER will be more efficient.

Article Statistics
Multiple requests among the same broswer session are counted as one view (or download).
If you mouse over a chart, a box will show the data point's value.


Cite this article
IEEE Style
Youjun Xu, "An Algorithm Solving SAT Problem Based on Splitting Rule and Extension Rule," Journal of Information Processing Systems, vol. 13, no. 5, pp. 1149~1157, 2017. DOI: 10.3745/JIPS.02.0071.

ACM Style
Youjun Xu, "An Algorithm Solving SAT Problem Based on Splitting Rule and Extension Rule," Journal of Information Processing Systems, 13, 5, (2017), 1149~1157. DOI: 10.3745/JIPS.02.0071.