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


Youjun Xu, Journal of Information Processing Systems Vol. 13, No. 5, pp. 1149-1157, Oct. 2017  

10.3745/JIPS.02.0071
Keywords: Extension Rule, IER, MOAMD Strategy, Satisfiability Problem, Splitting Rule
Fulltext:

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.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from November 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.




Cite this article
[APA Style]
Xu, Y. (2017). An Algorithm Solving SAT Problem Based on Splitting Rule and Extension Rule. Journal of Information Processing Systems, 13(5), 1149-1157. DOI: 10.3745/JIPS.02.0071.

[IEEE Style]
Y. 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. 2017. 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.