Abstract
In this paper, we explore data mining techniques for preprocessing Satisfiability problem -SAT- instances, reducing the complexity of the later and allowing an easier resolution.
Our study started with the exploration of the variables distribution on clauses, where we defined two kinds of distribution. The first distribution represents a space where variables are divided into dense regions and sparse or empty regions. The second distribution defines a space where the variables are distributed randomly filling almost the entire space.
This exploration led us to think about two different and appropriate data mining techniques for each of the two defined distribution. The Density based clustering, for the first distribution, where the high density regions are considered as clusters, and sparse regions as noise. And the Grid clustering, for the second distribution, where the space is considered as a grid and each case represent a cluster.
The presented work is a modelling of the density based clustering for SAT, which tend to reduce the problem’s complexity by clustering the problems instance in sub problems that can be solved separately.
Experiments were conducted on some well know benchmarks. The results show the impact of the use of the data mining preprocessing, and especially, the use of the appropriate technique according to the kind of data distribution.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: The Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1999). LNCS, Springer (1999)
Cook, S.: The complexity of theorem-proving procedures. In: Proceedings of 3rd Annual ACM Symposium on the Theory of Computing, New York, pp. 151–198 (1971)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394–397 (1962)
Drias, H., Douib, A., Hirèche, C.: Swarm intelligence with clustering for solving SAT. In: Yin, H., Tang, K., Gao, Y., Klawonn, F., Lee, M., Weise, T., Li, B., Yao, X. (eds.) IDEAL 2013. LNCS, vol. 8206, pp. 585–593. Springer, Heidelberg (2013)
Drias, H., Hireche, C., Douib, A.: Datamining techniques and swarm intelligence for problem solving: application to SAT. In: 2013 World Congress on Nature and Biologically Inspired Computing (NaBIC), pp. 200–206. IEEE (2013). ISBN 978-1-4799-1414-2
Drias, H., Sadeg, S., Yahi, S.: Cooperatives bees swarm for solving the maximum weighted satisfiability problem. In: Proceedings of IWANN 2005. LNCS, vol. 3512, pp. 318–325. Springer Verlag, Barcelona, June 2005
Ester, M., Kriegel, H.P., Sander, J., Xu, X.: A density-based algorithm for discovering clusters in large spatial databases with noise. In: Proceedings of the 2nd International Conference on Knowledge Discovery and Data mining, pp. 226–231 (1996)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. A Series of Books in the Mathematical Sciences. W.H. Freeman and Co, San Francisco (1979). pp. x+338. ISBN 0-7167-1045-5. MR 519066
Glover, F., Kochenberger, G.A.: Handbook of Metaheuristics. Springer, Heidelberg. https://doi.org/10.1007/b101874. ISBN: 978-1-4020-7263-5
Han, J. et al.: Data Mining, Concepts and Techniques: The Morgan Kaufmann Series in Data Management Systems. 3rd edn (2011)
Le, T., Kulikowski, C., Muchnik, I.: Coring method for clustering a graph. In: 19th International Conference on Pattern Recognition. ICPR 2008, Pattern Recognition, USA (2008)
Seeley, T.D., Camazine, S., Sneyd, J.: Collective decision-making in honey bees: how colonies choose among nectar sources. Behav. Ecol. Sociobiol. 28, 277–290 (1991). 232
Artificially generated random. https://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=benchmarks
Random SAT. https://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=benchmarks
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Hireche, C., Drias, H. (2018). Density Based Clustering for Satisfiability Solving. In: Rocha, Á., Adeli, H., Reis, L., Costanzo, S. (eds) Trends and Advances in Information Systems and Technologies. WorldCIST'18 2018. Advances in Intelligent Systems and Computing, vol 746. Springer, Cham. https://doi.org/10.1007/978-3-319-77712-2_85
Download citation
DOI: https://doi.org/10.1007/978-3-319-77712-2_85
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-77711-5
Online ISBN: 978-3-319-77712-2
eBook Packages: EngineeringEngineering (R0)