Full Program »

# Density Based Clustering for Satisﬁability Solving

In this paper, we explore data mining techniques for preprocessing Satisﬁability 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 deﬁned two kinds of distribution. The ﬁrst distribution represents a space where variables are divided into dense regions and sparse or empty regions. The second distribution deﬁnes a space where the variables are distributed randomly ﬁlling almost the entire space. This exploration led us to think about two diﬀerent and appropriate data mining techniques for each of the two deﬁned distribution. The Density based clustering, for the ﬁrst 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.