**Definition 2.** Let a and b be two objects described by two propositional formulas $\phi_1$ and $\phi_2$ respectively. Similarity between a and b is defined as:

$$s(a, b) = \frac{f(\phi_1 \land \phi_2)}{f(\phi_1 \land \phi_2) + \alpha f(\phi_1 \land \neg \phi_2) + \beta f(\phi_2 \land \neg \phi_1)} \quad \alpha, \beta \ge 0$$

In our context, as no distinction is made between the measure of $\phi_1 \land \neg \phi_2$ and $\phi_2 \land \neg \phi_1$, we derive the following similarity measure.

**Definition 3.** Let a and b be two objects described by two propositional formulas $\phi_1$ and $\phi_2$ respectively. Similarity between a and b is defined as:

$$s(a, b) = \frac{f(\phi_1 \land \phi_2)}{f(\phi_1 \land \phi_2) + \gamma f(\phi_1 \oplus \phi_2)}, \quad \gamma \ge 0$$

From Definition 2 (resp. Definition 3), instantiating $\alpha = \beta = 1$ (resp. $\gamma = 1$), we derive a logic-based variant of the well known Jaccard similarity coefficient (resp. distance) [13]:

**Definition 4.** Let a and b be two objects described by two propositional formulas $\phi_1$ and $\phi_2$ respectively. Similarity and distance between a and b or between $\phi_1$ and $\phi_2$ are defined respectively as:

$$s_J(a, b) = s_J(\phi_1, \phi_2) = \frac{f(\phi_1 \land \phi_2)}{f(\phi_1 \lor \phi_2)} \quad \text{and} \quad d_J(a, b) = 1 - s_J(a, b) = d_J(\phi_1, \phi_2)$$

As mentioned previously, considering the model based representation of propositional formulas, we define the function $f$ as:

$$f: \left| \begin{array}{l} F_P \rightarrow N \\ \phi \mapsto |M(\phi)| \end{array} \right. $$

Clearly, the function $f$ satisfies the additive property. Indeed, we have $M(\phi_1 \lor \phi_2) = M(\phi_1) \cup M(\phi_2)$. Computing $f$ involves solving a #P-Complete model counting problem as discussed in Section 1.1.

Let us now define the representative of a cluster of propositional formulas.

**Definition 5.** Let $C_i$ be a cluster involving $n_i$ formulas $\{\phi_{1i}, \phi_{2i}, \dots, \phi_{ni}\}$. We define the cluster representative (also called centroid) $\mathcal{O}_{C_i}$ of the cluster $C_i$ as:

$$\mathcal{O}_{C_i} = \phi_{1i} \land \phi_{2i} \land \dots \land \phi_{ni}$$

It is important to note that in our proposed extension, the goal is to group formulas into consistent clusters. Consequently, the formula representing a given cluster must be consistent.

We use the classical k-means objective function introduced in Definition 6

**Definition 6.** Let $\mathcal{P}(k, \Phi)$ be the problem of clustering a set of propositional formulas $\Phi = \{\phi_1, \dots, \phi_n\}$ to $k(\le n)$ clusters $C = \{C_1, \dots, C_k\}$. The objective function is defined using Absolute-Error Criterion (AEC):

$$C^* = \arg \min_C \sum_{i=1}^{k} \sum_{\phi \in C_i} d_J(\phi, \mathcal{O}_{C_i}) \quad (1)$$
Our clustering algorithm of a set of propositional formulas can now be de-
rived from the classical k-means algorithm using the new components (distance,
centroid and objective function) defined above.

## 3.2 Hierarchical Agglomerative Algorithm for propositional formulas Clustering

Hierarchical algorithms can behave better than the k-means. The base idea of
hierarchical agglomerative algorithms is to build a dendrogram such that at each
level the two closest clusters are merged. By applying a hierarchical algorithm,
we will ensure that if there are two objects that are closest to each other, they
will necessarily be in the same cluster. In this adaptation, the similarity be-
tween two clusters is identical to the similarity between their representatives.
Similarly to Definition 5, the conjunction of all formulas in a cluster represents
its centroid. To merge clusters, we combine the two clusters with the smallest
centroid distance. Using this adaptation, we can apply a standard hierarchical
agglomerative algorithm on data represented as boolean formulas as illustrated
in figure 2. Note that this algorithm needs at least $O(n^2)$ calls to a \# SAT oracle.

<figure><img src="image_40.png" /><figcaption>Fig. 2. Agglomerative Clustering on the Car Dealer Example</figcaption></figure>

# 4 Divisive Algorithm for Model Based Representation

As mentioned previously, when we consider the problem of clustering a set of formulas $\Phi = \{\phi_1, \phi_2, \dots, \phi_n\}$ without common model, i.e., $\Phi \vdash \perp$, agglomerative algorithm and k-means can fail to find a clustering with the desired number of clusters. In the sequel, we propose a top-down hierarchical (or divisive) algorithm for clustering a set of propositional formulas. Our proposed adaptation makes use of the well-known minimum hitting sets problem, that we recall.

**Definition 7.** *H is a hitting set of a set of sets Ω if ∀S ∈ Ω, H ∩ S ≠ ∅. A hitting set H is irreducible if there is no other hitting set H' s.t H' ⊂ H. H is called minimum hitting set if there is no hitting set H' such that |H'| < |H|.*
**Example 1.** Let $\Phi = \{\phi_1, \phi_2, \phi_3\}$ be a set of propositional formulas such that $\mathcal{M}(\phi_1) = \{m_1, m_2, m_3\}$, $\mathcal{M}(\phi_2) = \{m_1, m_4\}$ and $\mathcal{M}(\phi_3) = \{m_3, m_5\}$. The set $H = \{m_1, m_3\}$ is a minimum and irreducible hitting set of the models of $\Phi$.

In our adaptation, we choose the worst cluster to divide according to the following quality measure.

**Definition 8.** Let $C_i = \{\phi_{1_i}, \dots, \phi_{n_i}\}$ be a cluster of $n_i$ propositional formulas. We define the quality of $C_i$ as:

$$Q(C_i) = \frac{|\mathcal{M}(\phi_{1_i} \wedge \dots \wedge \phi_{n_i})|}{|\mathcal{M}(\phi_{1_i} \vee \dots \vee \phi_{n_i})|}$$

The quality of a cluster is obtained by extending the similarity measure between two formulas to a set of formulas. Indeed, a cluster is qualified to be of poor quality, when its formulas admits a great number of models while sharing a small number of models. Consequently, the worst cluster is obtained as follows:

$$C_i^* = \underset{C_i \in \mathcal{C}}{\operatorname{argmin}} Q(C_i)$$

**Definition 9.** Let $\Phi$ be a set of propositional formulas and $\mathcal{I}$ a Boolean interpretation. We define the subset of formulas of $\Phi$ sharing the model $\mathcal{I}$ as $S(\mathcal{I}, \Phi) = \{\phi \in \Phi \mid \mathcal{I} \models \phi\}$

To build consistent clusters, Algorithm 1 starts by computing a minimum hitting set $H$ of the set of sets of models of the formulas in $\Phi$ (line 1). The main idea behind our algorithm is to use the models of the computed minimum hitting set to divide a cluster into several consistent clusters. Each cluster is obtained by selecting for each model $m$ of the minimum hitting set, the set of formulas admitting $m$ as a model. In this way, the formulas in the obtained clusters share at least one model. If the size of the minimum hitting set $H$ is greater than $k$, then no clustering is possible, and the algorithm returns an empty set (line 3), otherwise a consistent clustering can be obtained. In this last case, the algorithm starts by a clustering $C$ where all the formulas in $\Phi$ are grouped into a single cluster (line 6). We start an iterative top-down divisive process (lines 7-20), until generating $k$ clusters. At each iteration, we choose a cluster to divide (line 8) which is one of those with the worst quality (see Definition 8). Then, we build $\Omega$ the set of sets of models of the formulas involved in the selected cluster, while removing the set of common models $M$ (lines 9-10). A minimum hitting set $H$ of $\Omega$ is then computed (line 11). It is important to note that by removing the common models $M$ from the models of each formula of the selected cluster, we avoid the trivial minimum hitting sets of size 1. Now, we use the hitting set $H$ to divide the chosen cluster $C_i^*$ into $|H|$ clusters (line 12). Indeed, for each model $m$ in $H$, we associate a cluster $\Psi_m$ made of formulas of $C_i^*$ sharing the model $m$. In this way, we maintain the consistency property on each new cluster $\Psi_m$. Now, we substitute in $C$ the cluster of poor quality $C_i^*$ with the new set of clusters (line 18). However, this is only done when the size of the new
<caption>**Algorithm 1:** Model-Based Divisive Algorithm for Clustering Boolean Formulas</caption>

**Input:** A set of formulas $\Phi = \{\phi_1, \dots, \phi_n\}$ and an integer $k \ge 1$
**Output:** A set of clusters $C = \{C_1, \dots, C_k\}$
1 $H \leftarrow \text{minHittingSet}(\{\mathcal{M}(\phi_1), \dots, \mathcal{M}(\phi_n)\})$;
2 **if** $|H| > k$ **then**
3 $\quad \text{return } \emptyset$;
4 **end**
5 **else**
6 $\quad C \leftarrow \{\Phi\}$;
7 $\quad \text{while } (|C| != k) \text{ do}$
8 $\quad \quad C_i^* = \{\phi_{i_1} \dots \phi_{i_{n_i}}\} \leftarrow \arg\min_{C_i \in C, |C_i| > 1} Q(C_i)$,
9 $\quad \quad \quad \triangleright n_i = |C_i^*|$;
10 $\quad \quad M = \mathcal{M}(\phi_{i_1}) \cap \dots \cap \mathcal{M}(\phi_{i_{n_i}})$;
11 $\quad \quad \Omega = \{\mathcal{M}(\phi_{i_1}) \setminus M, \dots, \mathcal{M}(\phi_{i_{n_i}}) \setminus M\}$;
12 $\quad \forall m \in H, \Psi_m \leftarrow S(m, C_i^*)$;
13 $\quad \text{if } (|C| + |H| - 1 > k) \text{ then}$
14 $\quad \quad \Psi \leftarrow \text{merge}(\{\Psi_{m_1}, \dots, \Psi_{m_{|C|+|H|-1-k}}\})$;
15 $\quad \quad C \leftarrow (C \setminus C_i^*) \cup \{\Psi\} \cup \{\Psi_{m_{|C|+|H|-k}}, \dots, \Psi_{m_{|H|}}\}$
16 $\quad \quad \quad \text{end}$
17 $\quad \quad \text{else}$
18 $\quad \quad C \leftarrow (C \setminus C_i^*) \cup \{\Psi_{m_1}, \dots, \Psi_{m_{|H|}}\}$
19 $\quad \quad \quad \text{end}$
20 $\quad \text{end}$
21 $\quad \text{end}$
22 $\quad C \leftarrow \text{eliminateOverlap}(C)$;
23 $\quad \text{return } C$

clustering does not exceed *k* (line 13); otherwise to obtain exactly *k* clusters, we merge (function merge) the first $|C| + |H| - (k + 1)$ of these new clusters (line 14) before applying substitution (line 15). Note that in the divisive step (line 12), a formula can belong to several new clusters. The reason comes from the fact that a given formula can share several models of the minimum hitting set. Consequently, a last step is then performed to produce non overlapping clusters (line 20 - function eliminateOverlap). To do this, for each formula occurring in several clusters, we keep it in the cluster with the best quality, while removing it in the remaining clusters. Obviously, depending on applications, overlapping clusters might be more suitable. In this case, one only need to skip the call to the overlap elimination function.

Algorithm 1, involves $O(n)$ calls to model enumeration problem (line 1), $O(k)$ calls to \# SAT oracle (line 8) and $O(k)$ calls to minimum hitting set problem (line 1 and 11).

Let us now gives some interesting properties of our propositional formulas based divisive algorithm. The first one states the correctness of our algorithm.

**Proposition 1.** If $\mathcal{P}(k, \Phi)$ is consistent, then Algorithm 1 produces a clustering.

The proof trivially follows from the previous detailed explanation on how the algorithm operates.
The second property allows us to establish that two equivalent formulas might be located in the same cluster when overlaps between clusters are allowed.

**Proposition 2.** Let $\mathcal{P}(k, \Phi)$ be a clustering problem with overlaps, $C$ a clustering of $\mathcal{P}(k, \Phi)$ and $\phi_1, \phi_2 \in \Phi$. If $\phi_1 \equiv \phi_2$ then $\forall C_i \in C, \phi_1 \in C_i \text{ iff } \phi_2 \in C_i$.

The last property generalizes the previous property to the case of two formulas where one is a logical consequence of the other.

**Proposition 3.** Let $\mathcal{P}(k, \Phi)$ be a clustering problem with overlaps, $C$ a clustering of $\mathcal{P}(k, \Phi)$ and $\phi_1, \phi_2 \in \Phi$. If $\phi_1 \vdash \phi_2$ then $\forall C_i \in C, \text{ if } \phi_1 \in C_i \text{ then } \phi_2 \in C_i$.

# 5 SAT encoding for a Bounded Consistent Clustering

As discussed in the previous section, when the propositional formulas are not represented by their models, our proposed model based divisive algorithm requires $O(n)$ calls to model enumeration oracle, to compute the set of models of each formula. Such set of models might be of exponential size in the worst case. In addition to these limitations, one also need to compute a minimum hitting set of a set of sets of models ($O(k)$ calls). In this section, we present an alternative approach that significantly reduces the overall complexity of our Algorithm. To this end, we introduce a SAT-based encoding that allows to find a bounded consistent clustering of a given set of propositional formulas.

Let $\Phi = \{\phi_1, \dots, \phi_n\}$ be a set of propositional formulas and $k$ a positive integer. To define our encoding, we associate to each propositional variable $p$ appearing in $\Phi$ a set of $k$ fresh propositional variables, denoted $p^1, \dots, p^k$. Then, for every formula $\phi_i \in \Phi$ and $j \in \{1, \dots, k\}$, we use $\phi_i^j$ to denote the formula obtained from $\phi_i$ by replacing each propositional variable $p$ with the fresh variable $p^j$. The formula $\phi_i^j$ is used to model the fact that $\phi_i$ is in the $j^{th}$ cluster.

The following formula expresses that each formula in $\Phi$ has to be true in at least one consistent cluster:

$$ \bigwedge_{i=1}^{n} \left( \bigvee_{j=1}^{k} \phi_i^j \right) \qquad (2) $$

One can easily see that (2) is satisfiable if and only if $\Phi$ can be partitioned in $k$ consistent clusters. It is worth noting that in a model of (2) a formula can belong to more than one cluster. To obtain a bounded consistent clustering from a model $m$, we only have to consider for each formula $\phi_i \in \Phi$ a single positive integer $j$ in the set $\{1 \le j \le k \mid m(\phi_i^j) = 1\}$. This problem can be avoided by reformulation. To this end, we associate to each formula $\phi_i$ in $\Phi$ a set of $k$ fresh propositional variables, denoted $q_{\phi_i}^1, \dots, q_{\phi_i}^k$. The variable $q_{\phi_i}^j$ is used to represent the fact that $\phi_i$ is in the $j^{th}$ cluster by using the following formula:

$$ \bigwedge_{i=1}^{n} \left( \bigwedge_{j=1}^{k} q_{\phi_i}^{j} \Leftrightarrow \phi_i^{j} \right) \qquad (3) $$
Then, to express that each formula in $\Phi$ belongs to exactly one consistent cluster, we use the following formula:

$$ \bigwedge_{i=1}^{n} \left( \sum_{j=1}^{k} q_{\phi_i}^{j} = 1 \right) \qquad (4) $$

Our second SAT encoding of the bounded consistent clustering problem $\mathcal{P}(k, \Phi)$ is defined by the formula $\mathcal{P}_{SAT}(k, \Phi) = (3) \wedge (4)$. From a model $m$ of $\mathcal{P}_{SAT}(k, \Phi)$, a clustering can be easily extracted. Indeed, if $m(q_{\phi_i}^j) = true$ then $\phi_i \in C_j$ otherwise $\phi_i \notin C_j$.

**Definition 10.** Let $\Phi = \{\phi_1, \dots, \phi_n\}$. $C$ is called a minimum consistent clustering of $\Phi$ if there is no consistent clustering $C'$ of $\Phi$ such that $|C'| < |C|$.

As we can observe, clustering propositional formulas can be done using Algorithm 1 by replacing the computation of the minimum hitting set with the computation of the minimum consistent clustering (Definition 10) using $\mathcal{P}_{SAT}(k, \Phi)$. Similarly to Algorithm 1, Properties 1, 2 and 3 holds.

# 6 Experimentation

In this section, we carried out an experimental evaluation of the performance of our divisive and agglomerative algorithms for the clustering of a set of propositional formulas. Our goal is to assess the feasibility and effectiveness of our proposed framework.

We performed our experiments on a machine with Intel Core2 Quad CPU of 2.66GHz and 8G of RAM. Our first aim is to compare the performance of our divisive and agglomerative algorithms. To this end, We consider two datasets splice, and german-credit<fnref n="1" />. We consider each data set as a set of transactions, where each transaction is a formula (a set of models). Consequently, an item is assimilated to a model.

Figure 3 shows the performances of agglomerative (Algorithm ??) and divisive (Algorithm 1) methods on the problem of clustering transaction databases. First, our divisive algorithm outperforms the agglomerative algorithm on splice and german-credit. Nevertheless, as illustrated in section 3.2, the agglomerative algorithm is unable to find a clustering all the time. This is the case on splice data, where such approach can not provide clustering answer when the number of desired clusters is less than 84.

To further investigate the expressiveness and the ability of our approach to scale, we enlarge our experiments of the previous problem by studying the clustering of a set of formulas resulting from a random-generated poll with 100 to 1000 participants where each participant is invited to report its preferences. The questions of the poll are organized in four levels. At the first level, the participant is invited to select its 3 preferred options among 5. According to the

<footnote n="1">¹ https://dtai.cs.kuleuven.be/CP4IM/</footnote>
<figure><img src="image_41.png" /><figcaption>Fig. 3. Model approach: Agglomerative vs Divisive</figcaption></figure>

preferences of the participant, she/he is invited to select other preferences from the second level and so on until the last level (level 4). For illustration, assume that in the first level we consider a set *S* of courses (e.g. Artificial Intelligence, Data Mining, Databases, Networks and Web Programming). A student selects three courses from *S* (level 1). Then, for each selected course, she/he chooses chapters (level 2), and so on. The preferences of each participant are encoded as a propositional formula (the resulting formulas have between 567 and 1813 models). Agglomerative approach is not considered since it can not guaranty to find a clustering solution if it exists.

<figure><img src="image_42.png" /><figcaption>Fig. 4. Time vs #Clusters vs #Participants</figcaption></figure>

The time needed to obtain a clustering, Figure 4, does not exceed 100 seconds for all values of *k*. This shows that our approach scale well. Finally, we study the evolution of the time needed to find a clustering when the number of clusters is fixed to 20 and the number of participants is varied from 100 to 1000 (Figure 4). Here again the time needed is reasonable, i.e., less than 100 seconds.

# 7 Conclusion et perspectives

In this work we introduced the concept of consistent clustering propositional formulas. We show how well-known k-means, agglomerative and divisive algorithms
can be adapted to this new framework. We then, propose two new solutions. The first one called model based, assume that the set of models of each formula are given. We then show how the hitting set notion is used to efficiently give a consistent clustering. In the second part, we propose an encoding into SAT of the divisive algorithm that make a linear number of calls to a #SAT oracle to count the set of models during the clustering steps. As a future work, we plan to explore other similarity measure, to define intuitive distance between propositional formulas. Improving our divisive algorithm by exploiting efficiently the overlaps deserves further investigation.

## References

1. C. C. Aggarwal and C. K. Reddy. *Data clustering: algorithms and applications*. CRC Press, 2013.

2. P. Berkhin. A survey of clustering data mining techniques. In J. Kogan, C. K. Nicholas, and M. Teboulle, editors, *Grouping Multidimensional Data - Recent Advances in Clustering*, pages 25-71. Springer, 2006.

3. L. Billard and E. Diday. *Symbolic Data Analysis: Conceptual Statistics and Data Mining*. John Wiley & Sons, May 2012.

4. H. H. Bock. *Analysis of Symbolic Data: Exploratory Methods for Extracting Statistical Information from Complex Data*. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2000.

5. S. Chakraborty, K. Meel, and M. Vardi. A scalable approximate model counter. In *CP'2013*, pages 200-216, 2013.

6. F. d. A. de Carvalho, M. Csernel, and Y. Lechevallier. Clustering constrained symbolic data. *Pattern Recognition Letters*, 30(11):1037-1045, 2009.

7. R. M. de Souza and F. d. A. De Carvalho. Clustering of interval data based on city-block distances. *Pattern Recognition Letters*, 25(3):353-365, 2004.

8. E. Diday and F. Esposito. An introduction to symbolic data analysis and the SODAS software. *Intell. Data Anal.*, 7(6):583-601, 2003.

9. C. P. Gomes, J. Hoffmann, A. Sabharwal, and B. Selman. From sampling to model counting. In *IJCAI'1997*, pages 2293-2299, 2007.

10. K. C. Gowda and E. Diday. *New Approaches in Classification and Data Analysis*, chapter Symbolic Clustering Algorithms using Similarity and Dissimilarity Measures, pages 414-422. Springer Berlin Heidelberg, Berlin, Heidelberg, 1994.

11. L. Hotz, A. Felfernig, M. Stumptner, A. Ryabokon, C. Bagley, and K. Wolter. Chapter 6 - configuration knowledge representation and reasoning. In *Knowledge-Based Configuration*, pages 41-72. Morgan Kaufmann, 2014.

12. S. Jabbour, J. Lonlac, L. Sais, and Y. Salhi. Extending modern SAT solvers for models enumeration. In *IEEE-IRI'2014*, pages 803-810, 2014.

13. P. Jaccard. The distribution of the flora of the alpine zon. *New Phytologist*, 11:37-50, 1912.

14. R. S. Michalski. Knowledge acquisition through conceptual clustering: A theoretical framework and an algorithm for partitioning data into conjunctive concepts. *Journal of Policy Analysis and Information Systems*, 4(3):219-244, 1980.

15. A. Tversky. Features of similarity. *Psychological Review*, 84(4):327-352, 1977.

16. A. Tversky. *Preference, Belief, and Similarity*. The MIT Press, November 2003.
# A SAT-based Framework for Overlapping Community Detection in Networks

**Abstract.** In this paper, we propose a new approach to the classic problem of detecting overlapping community in large complex networks. We first introduce a parametrized notion of communities, called *k-linked community*, allowing us to characterize node/edge centered k-linked community with bounded diameter. Next, we show how the problem of centered k-linked community detection can be expressed as a partial Max-SAT optimization problem. Last, we propose a post-processing strategy to limit the overlaps between communities. An extensive experimental evaluation on real-world networks shows that our approach outperforms several popular algorithms for community detection. Interestingly, when the diameter upper bound is set to four, our proposed approach outperforms the existing ones.

## 1 Introduction

Many complex interactions can be represented by networks, which are set of nodes connected by edges. Such connections might represent different type of relations between individuals or entities. Nodes in networks can be organized into *communities*, which often correspond to groups of nodes that share common properties, roles or functionnalities, such as functionally related proteins, social communities, or topically related webpages.

One of the most important tasks when studying networks is that of identifying communities. Indeed, detecting and analyzing communities is of great interest in several concrete applications, including clustering web clients who have similar interests, identifying clusters of customers in the network of customers-products purchase relationships of online retailers (e.g. Amazon), etc. However, designing an efficient algorithm for discovering communities in complex networks remains highly non-trivial for many reasons. For example, the most popular algorithm based on non-negative matrix factorisation [12] and spectral clustering methods [17] depend on a set of parameters such as the number of expected communities. Other approaches based on the edge betweenness [8] involve the computation of the shortest paths between pairs of nodes. So, the major motivation of this paper is to develop an algorithm which does not require any knowledge about the number of expected communities or the original division of the communities and discover the community structure in a reasonable amount of time.

To this end, we first introduce a parametrized notion of communities, called *k-linked community*, allowing us to characterize node/edge centered *k*-linked community with bounded diameter. We then show how to use off-the-shelf satisfiability solvers for community discovering using an appropriate encoding of the
centered *k*-linked community detection task as a partial maximum satisfiability
(Partial Max-SAT) optimisation problem. Our proposed framework allows us to
benefit from the recent advances in propositional satisfiability and its optimisa-
tion variants. Finally, we propose a post-processing strategy to limit the overlaps
between communities. Our proposed framework, follows the recent data mining
research trend exploiting two powerful declarative models, namely constraint
programming and propositional satisfiability. Indeed, several data mining tasks
including pattern mining [10] and clustering [7] have been modeled and solved
using these two well-known declarative and flexible models.

2 Formal Preliminaries

## 2.1 Propositional Logic and SAT Problem

Let $\mathcal{L}$ be a propositional language defined inductively from a finite set $\mathcal{P}\mathcal{S}$ of propositional symbols, the boolean constants $\top$ (*true* or 1) and $\bot$ (*false* or 0) and the standard logical connectives $\{\neg, \wedge, \vee, \rightarrow, \leftrightarrow\}$ in the usual way. We use the letters $x, y, z$, etc. to range over the elements of $\mathcal{P}\mathcal{S}$. Formulas of $\mathcal{L}$ are denoted by $A, B, C$, etc. A *literal* is a propositional variable ($x$) of $\mathcal{P}\mathcal{S}$ or the negation of a variable ($\neg x$). The two literals $x$ and $\neg x$ are called complementary. A *clause* is a (finite) disjunction of literals, i.e., $a_1 \vee \dots \vee a_n$. For every propositional formula $\mathcal{A}$ from $\mathcal{L}, \mathcal{P}(\mathcal{A})$ denotes the symbols of $\mathcal{P}\mathcal{S}$ occurring in $\mathcal{A}$.

A Boolean interpretation $\mathcal{I}$ of a formula $\mathcal{A}$ is a truth assignement of $\mathcal{P}\mathcal{S}$, that is, a total function from $\mathcal{P}(\mathcal{A})$ to $\{0, 1\}$. A model of a formula $\mathcal{A}$ is a Boolean interpretation $\mathcal{I}$ that satisfies $\mathcal{A}$, i.e. $\mathcal{I}(\mathcal{A}) = 1$. A formula $\mathcal{A}$ is satisfiable if there exists a model of $\mathcal{A}$. We denote by $\mathcal{M}(\mathcal{A})$ is the set of all models of $\mathcal{A}$.

As usual, every finite set of formulas is considered as the conjunctive formula
whose conjuncts are the elements of the set. A formula in *conjunctive normal form* (CNF) is a (finite) conjunction of clauses. The SAT problem consists in deciding whether a given CNF formula admits a model or not. This well-known NP-Complete problem has seen spectacular progress these recent years.

SAT has seen many successful applications in various fields such as elec-
tronic design automation, debugging of hardware designs, artificial intelligence,
and data mining. Several SAT extensions have been proposed to deal with op-
timisation problems. For example, the Max-SAT Problem seeks the maximum
number of clauses that can be satisfied. In this paper, we consider one of these
optimisation variants referred to as Partial Max-SAT problem. Partial Max-SAT
sits between SAT and Max-SAT problems. While SAT requires all clauses to be
satisfied, Partial Max-SAT relaxes this requirement by considering two kind of
clauses, hard and soft. Partial MaxSAT is the problem of finding an optimal
assignment to the variables that satisfies all the hard clauses, while satisfying
the maximum number of soft clauses.

## 2.2 Overlapping Community Detection

In this subsection, we discuss the classic problem of detecting overlapping com-
munity structure in networks.
A network is an undirected graph $\mathcal{N} = (V, E)$ where $V$ is a set of nodes and $E \subseteq V \times V$ is a set of edges. We denote by $n$ (respectively $m$) the number of nodes (respectively edges) in $\mathcal{N}$. The degree of a node $u \in V$, denoted $d_u$, is the number of edges connected to it. The length of the shortest path between two nodes $u, v \in V$ is called the distance between the nodes, noted $dist(u, v)$. Given an edge $e = (u, v) \in E$ and a node $w \in V$, the distance between $e$ and $w$ is defined as $dist(e, w) = \min\{dist(u, w), dist(v, w)\}$. In graph theory, a community is described as a set of nodes densely connected internally. In real-world networks, nodes are organized into densely linked sets of nodes that are commonly referred to as network communities, clusters or modules. Notice that communities in networks often overlap as nodes can belong to multiple communities at once. Network overlapping community detection problem consists in dividing a network of interest into (overlapping) communities for intelligent analysis. It has recently attracted significant attention in diverse application domains. Identifying the community structure is crucial for understanding structural properties of the real-world networks. Various methods have been proposed to identify the community structure of complex networks (see [6, 15] for an overview).

## Quality Metrics:

Several measures have been proposed for quantifying the quality of communities in networks (see [13] for a comparative study of quality measures). In this paper, we adopt two well-known metrics to assess the performance of our method:

**Modularity.** The most widely used metric for measuring the quality of network's partition into communities (without a ground-truth) is Newman's modularity function [19]. The idea of modularity-based community detection is to try to assign each node of the given network to a community such that it maximizes the modularity value of the whole network. Modularity quantifies the community strength by comparing the fraction of edges within the community with such fraction when random connections between the nodes are made. Networks with high modularity have dense connections between the nodes within communities but sparse connections between nodes in different communities. The modularity function has several variants, but these variants share the same principle. Without the loss of generality, we use the following equation of modularity, an extension of Newman's modularity function designed to support overlapping communities proposed in [20]. For the given community partition of a network $\mathcal{N} = (V, E)$ with $m$ edges, an extended modularity $EQ$ is given by:

$$EQ = \frac{1}{2m} \sum_{C \in \mathcal{C}_N} \sum_{u,v \in C} \frac{1}{O_u O_v} \left[ A_{uv} - \frac{d_u d_v}{2m} \right] \quad (1)$$

with $C_N$ the set of communities in $\mathcal{N}$; $O_u$ the number of communities to which the node $u$ belongs and $A_{uv}$ is the element of the adjacency matrix representing the network.
**F1 score.** Let $\mathcal{N} = (V, E)$ be a network, and $\hat{C}$ (respectively $C^*$) the set of (respectively ground truth) communities associated to $\mathcal{N}$. The average F1 score measure aims to quantify the level of correspondence between $C^*$ and $\hat{C}$. More precisely, we need to determine which $C_i \in C^*$ corresponds to which $\hat{C}_i \in \hat{C}$. The F1 score is defined as the average of F1 score of the best matching ground-truth community to each detected community, and the F1 score of the best matching detected community to each ground-truth community [25]. More formally, this function is defined as follows:

$$ \frac{1}{2} \left( \frac{1}{|C^*|} \sum_{C_i \in C^*} F_1(C_i, \hat{C}_{g(i)}) + \frac{1}{|\hat{C}|} \sum_{\hat{C}_i \in \hat{C}} F_1(C_{g'(i)}, \hat{C}_i) \right) \quad (2) $$

where the best matching $g$ and $g'$ is defined as follows: $g(i) = \arg\max_j F_1(C_i, \hat{C}_j)$, $g'(i) = \arg\max_j F_1(C_j, \hat{C}_i)$, and $F_1(C_i, \hat{C}_j)$ is the harmonic mean of Precision and Recall.

## 3 A SAT-based Framework for Community Detection

Fundamentally, communities allow us to discover groups of interacting objects and the relations between them. A community (also referred to as a cluster) is a set of cohesive nodes that have more connections inside the set than outside. In this section, we propose to use off-the-shelf satisfiability solvers for community detection using an appropriate encoding of the community detection task as a SAT optimization problem. Proximity between nodes have been expressed as direct edges expressing formally a direct relation. Individuals can be grouped into the same cluster even if they are not linked directly. Relationships between individuals can be expressed via some proximity conditions. For instance, individuals having much common friends could be considered as very closed to each other. Consequently, the definition of individuals proximity is clearly a fundamental issue, as it have a great impact on the outcome. Next, we establish the main definitions which will be used to formulate our problem.

**Definition 1 (k-linked community).** A community is k-linked if the nodes are pairwise k-linked, i.e., the distance between each two nodes is less or equal than k.

According to Definition 1, a k-linked community has a diameter less or equal than k. Now, to allow for the use of SAT problem in discovering overlapping communities, we need to focus on the following kinds of k-linked communities called k-linked centered communities: those having a centroid node or centroid edge that possesses a distance at most $\frac{k}{2}$ from each other node of the community.

**Definition 2 (Node/Edge Centered k-linked Community).** Let $\mathcal{N} = (V, E)$ be a network and $k > 1$ a positive integer. A community $C \subseteq V$ is node
(resp. edge) centered k-linked community of $\mathcal{N}$ iff there exists $c \in C$ (resp. $e = (u, v) \in E$ with $u, v \in C$) s.t. $\forall w \in C$, $\text{dist}(c, w) \le \frac{k}{2}$ (resp. $\text{dist}(e, w) \le \frac{k}{2}$).

Obviously, a node centered k-linked community is an edge centered k-linked community, while the converse is not true. Note also that a k-linked community is not necessarily a centered k-linked community. A counter-example consists of the network $\mathcal{N} = (V, E)$ where $V = \{x_1, \dots, x_8\}$ and $E = \{(x_1, x_2), (x_2, x_3), (x_3, x_4), (x_5, x_6), (x_6, x_7), (x_7, x_8), (x_1, x_5), (x_4, x_8)\}$. Then, $C = V$ is a 4-linked community, while there is neither a node $x_i \in V$ nor edge $e \in E$ with distance at most 2 from all the remaining nodes of $C$.

**Lemma 1.** Let $\mathcal{N} = (V, E)$ be a network, $C \subseteq V$ a community and $k > 1$ a positive integer. If $C$ is a centered k-linked community, then $C$ is also a k-linked community.

Now, based on the notion of centered k-linked community, community detection is defined as an optimization problem, solving partial Max-SAT. To do so, our starting point is to find a set of centroids $S$ in the given network. The next step is to form the communities around the centroids based on a predefined parameter $k$ which represents the diameter of the communities. Clearly, we distinguish the following two cases: k-linked node (resp. edge) centered communities corresponding to an even (resp. odd) value of $k$.

Next, we propose two appropriate reformulations as an optimization problem for the community detection problem corresponding to node and edge centered k-linked communities, respectively. To achieve this, propositional variables are used for representing the network. Indeed, we associate each node $u$ (resp. edge $e$) with a propositional variable denoted $x_u$ (resp. $y_e$) where $x_u, y_e \in \{0, 1\}$. The key idea is that the variables assigned to 1 represent the centroids nodes (resp. edges), i.e., $S_v = \{u \in V | \mathcal{I}(x_u) = 1\}$ (resp. $S_e = \{e \in E | \mathcal{I}(y_e) = 1\}$). We now describe our SAT-based encodings using such propositional variables.

**Node Centered k-linked Community:** Our encoding consists of a set of constraints. The first propositional formula expresses the fact that if a node $u$ is a centroid ($\mathcal{I}(x_u) = 1$), then the nodes with a distance at most $\frac{k}{2}$ from $u$ are placed to the same community that possesses $u$ as a centroid.

$$ \bigwedge_{u \in V} (x_u \rightarrow \bigwedge_{v \in V | \text{dist}(u, v) \le \frac{k}{2}} \neg x_v) \qquad (3) $$

Let us remark that constraint (3) can be expressed by a set of binary clauses:

$$ \bigwedge_{u \in V} \bigwedge_{v \in V | \text{dist}(u, v) \le \frac{k}{2}} (\neg x_u \lor \neg x_v) $$

After finding the centroids, we still have to determine whether a node $u$ belongs to community $C$ or not depending on the value of $k$. To achieve this, we use the following formula that affects nodes of the network to communities
where they belong to, i.e., nodes that have a distance at most of $\frac{k}{2}$ from the centroid.

$$ \bigwedge_{u \in V} \bigvee_{v \in V | dist(u,v) \le \frac{k}{2}} x_v \qquad (4) $$

**Proposition 1.** If the constraints (3) ∧ (4) are satisfied, then for all $u \notin S_v$ there exists $v \in S_v$ s.t. $dist(u, v) \le \frac{k}{2}$.

Proposition 1 ensures that if (3) ∧ (4) admits a model $\mathcal{I}$, then the nodes corresponding to the variables assigned to 1 ($\{u \in V | \mathcal{I}(x_u) = 1\}$) are the centroids and the network can be partitioned into $|S|$ communities. The communities can then be constructed by finding the nodes with a distance at most $\frac{k}{2}$ from each centroid.

Obviously, the formula (3) ∧ (4) may admits many candidate solutions (i.e. models). However, choosing an arbitrary model do not always guarantee a best partition of the network into communities. To alleviate this problem, we will consider an objective function to optimize over the space of solutions. Then, the node centered k-linked community detection problem can be formulated as the following optimisation problem:

$$ \min/\max \sum_{u \in V} x_u \quad \text{subject to (3) ∧ (4)} \qquad (5) $$

**Edge Centered k-linked Community:** Now, to derive the formulation of edge centered k-linked community detection problem, we use similar reasoning as for node centered k-linked community, except that we consider centroid edges instead of centroid nodes. To do so, a community is built around an edge $e = (u, v)$ by considering nodes with a distance at most $\frac{k}{2}$ from the edge $e$. This is equivalent to partition the set of edges into modules and from that modules we can deduce the set of communities of nodes.

In the same way as for centroid nodes, the following formula expresses the fact that if an edge $e = (u, v)$ is a centroid edge ($\mathcal{I}(y_e) = 1$), then the nodes with a distance at most $\frac{k}{2}$ from $u$ or $v$ are assigned to 0.

$$ \bigwedge_{e=(u,v) \in E} (y_e \rightarrow \bigwedge_{e' \in E | dist(e',u) \le \frac{k}{2} | dist(e',v) \le \frac{k}{2}} \neg y_{e'}) \qquad (6) $$

Let us now introduce the following formula that affects nodes of the network to their associated communities, i.e. nodes that have a distance of $\frac{k}{2}$ from the centroid edge $e$.

$$ \bigwedge_{e=(u,v) \in E} \bigvee_{e' \in E | dist(e',u) \le \frac{k}{2} | dist(e',v) \le \frac{k}{2}} y_{e'} \qquad (7) $$

After fixing the centroids edges, the constraint 7 allows to identify whether a node $u$ belongs to a community $C$ or not from the value of $k$.
Similarly, to improve the quality of the detected communities, our edge centered k-linked community detection problem is formulated as the following optimization problem:

$$ \min/\max \sum_{e \in E} y_e \quad \text{subject to (6) } \wedge \text{ (7)} \qquad (8) $$

We will use the notation $CDSAT_{min/max}^k$ to denote the optimization problems (5) and (8).

**Example 1.** Let us consider the undirected network $\mathcal{N} = (V, E)$ depicted in Figure 1. Setting $k = 4$ can lead to the following solution of $CDSAT_{max}^4$: $\mathcal{I} = \{\neg x_1, \neg x_2, \neg x_3, \neg x_4, \neg x_5, x_6, \neg x_7, x_8, \neg x_9, \neg x_{10}, \neg x_{11}\}$. So for that solution, $\mathcal{N}$ can be partitioned into the two communities $C_1 = \{x_1, \dots, x_6, x_7, x_{11}\}$ and $C_2 = \{x_1, x_2, x_5, x_6, x_7, \dots, x_{11}\}$. In contrast, $CDSAT_{min}^4$ leads to one community with centroid $x_1$ and containing all the nodes of $\mathcal{N}$.

<figure><img src="image_43.png" /><figcaption>Fig. 1. A simple undirected network</figcaption></figure>

**Overlapping Enhancement:** As said before, once the node/edge centroids are found, the communities are formed around them based on a predefined parameter $k$. As a result, some nodes can belong to multiple communities as illustrated in Example 1. However, such overlapping can be huge and not significant enough w.r.t. real communities. To overcome this drawback and to allow for an accurate partition of the network, we propose a simple but effective overlaps reduction technique in order to correctly identify dense community overlaps. Starting from a set of communities, each overlapping node will be assigned to its closest community according to its distance from the centroids of these communities.

**Example 2.** Let us consider again the network $\mathcal{N} = (V, E)$ of Figure 1. By enhancing the overlapping, the two communities are reduced to $C_1 = \{x_1, \dots, x_6\}$ and $C_2 = \{x_1, x_7, \dots, x_{11}\}$.

Algorithm 1 describes the general feature of our SAT-based node centered k-linked community detection procedure <fnref n="1" />. The algorithm takes as input the

<footnote n="1">¹ Algorithm 1 can be slightly modified to deal with edge centered k-linked community detection problem.</footnote>
network and even integer *k* and returns a set of overlapping communities. It proceeds as follows: First, we generate the corresponding optimization problem that can be represented as a Partial MaxSAT problem (line 1). Then, a state-of-the-art Weighted Partial MaxSAT solver WPM3 is used to get an optimal solution (i.e. model) *I*. Next, the centroids are determined from the obtained model (lines 4-7). Using such centroids, the next step is to build communities by finding the nodes with a distance at most $\frac{k}{2}$ from each centroid. Finally, the cleaning step is called to improve the quality of detected communities (lines 11-13).

<caption>**Algorithm 1:** CDSAT<sup>*k*</sup><sub>min/max</sub></caption>

**Input:** A network $\mathcal{N} = (V, E)$ and an integer $k > 1$
**Output:** A set of overlapping communities
1 &Phi; = encodeToOpt(k, G);
2 I = solve(&Phi;);
3 S &lt;= &emptyset;;
4 for $u_x \in I$ do
5 &nbsp;&nbsp;&nbsp;&nbsp;if $\mathcal{I}(u_x) == 1$ then
6 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$C_u \leftarrow \{u\}$;
7 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$S \leftarrow S \cup C_u$;
8 &nbsp;&nbsp;&nbsp;&nbsp;end
9 end
10 for $v_x \in I$ do
11 &nbsp;&nbsp;&nbsp;&nbsp;for $C_u \in S$ do
12 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $\text{dist}(u, v) \le \frac{k}{2}$ then $C_u \leftarrow C_u \cup \{v\}$;
13 &nbsp;&nbsp;&nbsp;&nbsp;end
14 end
15 for $C_u, C_v \in S \times S$ do
16 &nbsp;&nbsp;&nbsp;&nbsp;for $w \in V$ do
17 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $\text{dist}(w, u) < \text{dist}(w, v)$ then $C_v \leftarrow C_v \setminus \{w\}$;
18 &nbsp;&nbsp;&nbsp;&nbsp;end
19 end
20 return S

# 4 Performance Evaluation

## 4.1 Experiment Settings

In this section, we present an experimental evaluation of our proposed approach. It was conducted on fourteen networks that cover a variety of application areas and are briefly described in Table 1 (columns 1 and 2). Some of these networks have ground-truth communities as presented in column 2 of Table 2. We have also chosen three large networks (Facebook, DBLP, and Amazon taken from SNAP [14]) to show the scalability of our model.

We evaluate the performance of our approaches by comparing them with the following most prominent state-of-the-art overlapping community detection algorithms: (i) *Community-Affiliation Graph Model (AGM)* [24], (ii) *Clique Percolation Method (CPM)* [1], (iii) *Cluster Affiliation Model for Big Networks (BIGCLAM)* [25], and (iv) *Communities from Edge Structure and Node Attributes (CESNA)* [26]. For the CPM algorithm, we use the cliques of size equal to 3. For BIGCLAM
method, user can specify the number of communities to detect, or let the program determine the number of communities in the network from the topology of the network. We opt for the second case where the number of communities is not fixed in advance.

The proposed system, referred to as CDSAT<sub>min/max</sub><sup>k</sup>, was written in Python. Given an input network as a set of edges, our algorithm starts by generating the corresponding optimization problem represented as a Partial MaxSAT problem. To solve this problem, we consider the state-of-the-art Weighted Partial MaxSAT solver WPM3 (best solver at the last MaxSAT competition <sup>2</sup>) [2]. For our experimental study, all algorithms have been run on a PC with an Intel Core 2 Duo (2 GHz) processor and 2 GB memory. We imposed one hour time limit for all the methods. Last, we use the symbol (-) in Tables 1 and 2 to indicate that the method is not able to scale on the considered network under the time limit.

## 4.2 Choosing the Best Value of the Diameter

Our CDSAT<sub>min/max</sub><sup>k</sup> algorithm takes as input a network and a positive integer *k* and returns a set of overlapping communities. In order to determine the best diameter *k*, we run our CDSAT<sub>min/max</sub><sup>k</sup> algorithms on the fourteen considered networks, while varying *k* from 3 to 6. The Figure 2 summarises the relationship between the average modularity and *k*. In both algorithms CDSAT<sub>min</sub><sup>k</sup> and CDSAT<sub>max</sub><sup>k</sup>, we see that the best average modularity is achieved for the diameter *k* = 4. As Figure 2 reveals, the best average modularity is obtained by CDSAT<sub>min</sub><sup>4</sup> and CDSAT<sub>max</sub><sup>4</sup> with a value of 0.421 and 0.432 respectively. As we can observe, the average modularity obtained by both algorithms decreases beyond *k* = 4. Overall, for both algorithms the best average modularity is obtained for *k* = 4. There performances are relatively close. This can be explained by the fact that real-world social networks possess small (average or effective) diameter (e.g. [5]). This can be related to the property of the small-world phenomenon observed by several authors on real graphs (e.g. [21]).

## 4.3 Comparison with Baseline Algorithms

**Experiments with modularity metric.** Table 1 reports the performance comparison between our CDSAT<sub>min/max</sub><sup>4</sup> approaches and the considered methods. Experiments show that our methods outperform every baseline, in most cases, by an interesting margin as shown by the average modularity reported in the last line of Table 1. We observe that across all datasets and modularity metric, CDSAT<sub>min</sub><sup>4</sup> yields the best performance in 8 out of 14 networks. We also note that CDSAT<sub>min</sub><sup>4</sup> shows a high margin in performance gain against the baselines in two large networks DBLP and Amazon, and in a collaborations network such as Coauthorship. In terms of average performance, CDSAT<sub>min</sub><sup>4</sup> outperforms CPM by 111.55%, BIGCLAM by 26.42%, and CESNA by 40.80%. Similarly, we note

<footnote n="2"><sup>2</sup> http://maxsat.ia.udl.cat/introduction/</footnote>
<figure><img src="image_44.png" /><figcaption>Fig. 2. Average modularity for CDSAT<sup>k</sup><sub>min/max</sub></figcaption></figure>

that CDSAT<sup>4</sup><sub>max</sub> outperforms all the other methods in 7 out of 14 datasets. In terms of average performance, CDSAT<sup>4</sup><sub>max</sub> outperforms CPM by 117.08%, BIGCLAM by 29.72%, and CESNA by 44.48%. We also observe that CDSAT<sup>4</sup><sub>max</sub> gives an important improvement against the baselines in two large networks Facebook, DBLP, and also in a collaborations network like Coauthorship. On the Lemis, Power grid, Pilgrim, and Jazz datasets, our methods remain relatively competitive with the best baseline. A possible explanation for this phenomenon is that the WPM3 solver don't return the optimal solution for these datasets. Overall, our methods outperform BIGCLAM, which is the most competing algorithm, on all large real datasets.

<table><caption>Table 1. Modularity based performance on fourteen datasets</caption><thead><tr><th>Networks</th><th>nodes/edges</th><th>AGM</th><th>CPM</th><th>BIGCLAM</th><th>CESNA</th><th>CDSAT<sup>4</sup><sub>min</sub></th><th>CDSAT<sup>4</sup><sub>max</sub></th></tr></thead><tbody><tr><td>Dolphin [16]</td><td>62/159</td><td>-0.040</td><td>0.304</td><td>0.053</td><td>0.095</td><td><strong>0.438</strong></td><td>0.297</td></tr><tr><td>Karate [23]</td><td>34/78</td><td>0.200</td><td>0.230</td><td>0.195</td><td>0.180</td><td><strong>0.310</strong></td><td><strong>0.311</strong></td></tr><tr><td>Risk map [4]</td><td>42/83</td><td>0.415</td><td>0.488</td><td>0.194</td><td>0.504</td><td><strong>0.571</strong></td><td><strong>0.528</strong></td></tr><tr><td>Lemis [11]</td><td>77/254</td><td>0.162</td><td>0.205</td><td><strong>0.444</strong></td><td>0.311</td><td>0.064</td><td>0.419</td></tr><tr><td>Word adjacencies [18]</td><td>112/425</td><td>0.139</td><td>0.031</td><td>0.154</td><td>0.111</td><td><strong>0.175</strong></td><td>0.098</td></tr><tr><td>Football [8]</td><td>115/615</td><td>0.222</td><td>0.199</td><td>0.343</td><td>0.390</td><td>0.286</td><td><strong>0.404</strong></td></tr><tr><td>Facebook [14]</td><td>4039/88234</td><td>-</td><td>-</td><td>0.391</td><td>0.539</td><td>0.449</td><td><strong>0.701</strong></td></tr><tr><td>DBLP [14]</td><td>317080/1049866</td><td>-</td><td>0.293</td><td>0.216</td><td>0.202</td><td><strong>0.520</strong></td><td><strong>0.436</strong></td></tr><tr><td>Amazon [14]</td><td>334863/925872</td><td>-</td><td>0.195</td><td>0.341</td><td>0.430</td><td><strong>0.616</strong></td><td><strong>0.502</strong></td></tr><tr><td>Books [8]</td><td>105/441</td><td>0.366</td><td>0.265</td><td>0.308</td><td>0.255</td><td><strong>0.439</strong></td><td>0.345</td></tr><tr><td>Power grid [22]</td><td>4941/6594</td><td>-</td><td>0.007</td><td><strong>0.840</strong></td><td>0.586</td><td>0.679</td><td>0.547</td></tr><tr><td>Coauthorship [18]</td><td>1462/2742</td><td>0.619</td><td>0.456</td><td>0.679</td><td>0.031</td><td><strong>0.923</strong></td><td><strong>0.852</strong></td></tr><tr><td>Pilgrim [3]</td><td>34/128</td><td>0.368</td><td>0.096</td><td><strong>0.415</strong></td><td>0.321</td><td>0.312</td><td>0.407</td></tr><tr><td>Jazz [9]</td><td>196/2742</td><td><strong>0.310</strong></td><td>0.022</td><td>0.099</td><td>0.231</td><td>0.112</td><td>0.208</td></tr><tr><td>Average</td><td>N/A</td><td>N/A</td><td>0.199</td><td>0.333</td><td>0.299</td><td><strong>0.421</strong></td><td><strong>0.432</strong></td></tr></tbody></table>

**Results on ground-truth communities.** After finding communities in a given network, we can gauge the performance of each community that an algorithm has discovered and whether a ground-truth community has been successfully identified. Table 2 summarizes the evaluation results, with F1 scores of all algorithms
on each network. Interestingly, it can be seen that $CDSAT_{min}^4$ and $CDSAT_{max}^4$ produce more accurate average w.r.t. the ground-truth setting than all the other baseline algorithms. In terms of average performances, $CDSAT_{min}^4$ outperforms CPM by 16%, BIGCLAM by 22%, and CESNA by 35.05%. Moreover, notice that $CDSAT_{max}^4$ outperforms CPM by 6.49%, BIGCLAM by 12%, and CESNA by 23.98%. In the cases of Karate, Risk map and DBLP data instances, $CDSAT_{min}^4$ and $CDSAT_{max}^4$ achieves a closely gain in the F1 score compared to the best baseline (CPM in this case).

As a summary, experimental results confirm that $CDSAT_{min/max}^4$ methods achieve the overall best performance in terms of the accuracy of the detected overlapping communities.

<table><caption>**Table 2.** F1 Score based performance of methods on fourteen datasets</caption><thead><tr><th>Networks</th><th>Communities</th><th>AGM</th><th>CPM</th><th>BIGCLAM</th><th>CESNA</th><th>CDSAT<sup>4</sup><sub>min</sub></th><th>CDSAT<sup>4</sup><sub>max</sub></th></tr></thead><tbody><tr><td>Dolphin</td><td>2</td><td>0.120</td><td>0.579</td><td>0.628</td><td>0.100</td><td><strong>0.749</strong></td><td><strong>0.659</strong></td></tr><tr><td>Karate</td><td>2</td><td>0.864</td><td><strong>0.857</strong></td><td>0.629</td><td>0.663</td><td>0.847</td><td>0.851</td></tr><tr><td>Risk map</td><td>6</td><td>0.641</td><td><strong>0.884</strong></td><td>0.694</td><td>0.842</td><td>0.779</td><td>0.769</td></tr><tr><td>DBLP</td><td>13477</td><td>—</td><td><strong>0.596</strong></td><td>0.370</td><td>0.310</td><td>0.470</td><td>0.483</td></tr><tr><td>Amazon</td><td>75149</td><td>—</td><td>0.519</td><td>0.498</td><td>0.642</td><td><strong>0.695</strong></td><td>0.399</td></tr><tr><td>Books</td><td>3</td><td>0.684</td><td>0.557</td><td>0.549</td><td>0.591</td><td><strong>0.804</strong></td><td>0.652</td></tr><tr><td>Pilgrim</td><td>4</td><td>0.773</td><td>0.427</td><td>0.835</td><td>0.652</td><td>0.785</td><td><strong>0.892</strong></td></tr><tr><td>Average</td><td>N/A</td><td>N/A</td><td>0.631</td><td>0.600</td><td>0.542</td><td><strong>0.732</strong></td><td><strong>0.672</strong></td></tr></tbody></table>

**Evaluating scalability.** Finally, we evaluate the scalability of the different community detection methods by measuring the CPU time (see Table 3). From the results, it can be seen that our algorithms make few seconds to generate all communities for small networks. However, the CPM, BIGCLAM and CESNA baselines are faster than our methods for small networks (up to 200 nodes). We can observe that $CDSAT_{min}^4$ and $CDSAT_{max}^4$ are third-fastest method overall, when the network becomes larger. Interestingly, we also notice that our algorithms are the second-fastest methods, next BIGCLAM, for DBLP and Amazon.

<table><caption>**Table 3.** Comparison in terms of running Time (s)</caption><thead><tr><th>Networks</th><th>AGM</th><th>CPM</th><th>BIGCLAM</th><th>CESNA</th><th>CDSAT<sup>4</sup><sub>max</sub></th><th>CDSAT<sup>4</sup><sub>min</sub></th></tr></thead><tbody><tr><td>Dolphin</td><td>6.77</td><td>0.09</td><td>0.24</td><td>0.07</td><td>14</td><td>8</td></tr><tr><td>Karate</td><td>35</td><td>0.07</td><td>0.29</td><td>0.07</td><td>11</td><td>7.15</td></tr><tr><td>Risk map</td><td>62</td><td>0.09</td><td>2.84</td><td>0.59</td><td>38</td><td>17</td></tr><tr><td>Lemis</td><td>200</td><td>0.10</td><td>0.55</td><td>0.09</td><td>16</td><td>12</td></tr><tr><td>Word adjacencies</td><td>60.35</td><td>0.09</td><td>0.97</td><td>0.13</td><td>60.60</td><td>11</td></tr><tr><td>Football</td><td>47.71</td><td>0.08</td><td>1.78</td><td>0.13</td><td>120.20</td><td>420</td></tr><tr><td>Facebook</td><td>&gt; 1h</td><td>&gt; 1h</td><td>240.38</td><td>4.81</td><td>360.30</td><td>480.7</td></tr><tr><td>DBLP</td><td>&gt; 1h</td><td>3240</td><td>60.56</td><td>900.34</td><td>720.50</td><td>780.40</td></tr><tr><td>Amazon</td><td>&gt; 1h</td><td>&gt; 1h</td><td>60.09</td><td>1200.49</td><td>780.20</td><td>900</td></tr><tr><td>Books</td><td>19.83</td><td>0.12</td><td>2.71</td><td>0.10</td><td>14.35</td><td>60.20</td></tr><tr><td>Power grid</td><td>&gt; 1h</td><td>0.66</td><td>0.81</td><td>4.48</td><td>420.15</td><td>480.25</td></tr><tr><td>Co-authorship science</td><td>360.17</td><td>0.07</td><td>14.08</td><td>0.05</td><td>360.58</td><td>360.20</td></tr><tr><td>Pilgrim</td><td>0.61</td><td>0.09</td><td>0.35</td><td>0.07</td><td>8.2</td><td>7</td></tr><tr><td>Jazz</td><td>60.02</td><td>0.09</td><td>2.84</td><td>0.59</td><td>360.12</td><td>120</td></tr></tbody></table>
# 5 Conclusion

In this paper, we developed a novel community detection approach that accurately discovers the overlapping community structure of real-world networks. Our method is based on a partition of the network into modules having with maximum diameter *k*. We identified two kind of community structures: centroid node based community and centroid edge based community. Different encodings into Partial MaxSAT problem are provided and a policy to limit the overlapping is proposed. Experiments show that our approach outperforms the state-of-the-art methods in accurately discovering network communities.

Our work has several implications: First, our encoding can lead to big optimization problems for that the identification of an optimal solution is challenging. Decomposition and parallel algorithms would be very helpful to improve the resolution process. Second, the optimal solution is not unique which can affect the quality of clusters. Looking for particular solutions is another interesting research direction to improve the quality of detected communities.

# References

1. B. Adamcsek, G. Palla, I. J. Farkas, I. Derényi, and T. Vicsek. Cfinder: locating cliques and overlapping modules in biological networks. *Bioinformatics*, 22(8):1021–1023, 2006.

2. C. Ansótegui, F. Didier, and J. Gabàs. Exploiting the structure of unsatisfiable cores in MaxSAT. In *IJCAI*, pages 283–289, 2015.

3. Brian, B. Dickinson, W. Valyou, and Hu. A genetic algorithm for identifying overlapping communities in social networks using an optimized search space. *Social Networking*, 02No.04:1–9, 2013.

4. J. Cheng, M. Leng, L. Li, H. Zhou, and X. Chen. Active semi-supervised community detection based on must-link and cannot-link constraints. *PLoS ONE*, 9(10):1–18, 2014.

5. F. Comellas, J. Ozón, and J. G. Peters. Deterministic small-world communication networks. *Information Processing Letters*, 76(1):83 – 90, 2000.

6. S. Fortunato. Community detection in graphs. *CoRR*, abs/0906.0612, 2009.

7. S. Gilpin and I. N. Davidson. Incorporating SAT solvers into hierarchical clustering algorithms: an efficient and flexible approach. In *KDD*, pages 1136–1144, 2011.

8. M. Girvan and M. E. J. Newman. Community structure in social and biological networks. *Proc. Natl. Acad. Sci.*, 99:7821, 2002.

9. P. Gleiser and L. Danon. Community structure in jazz. *Advances in Complex Systems*, 6:565, 2003.

10. T. Guns, S. Nijssen, and L. D. Raedt. Itemset mining: A constraint programming perspective. *Artif. Intell.*, 175(12-13):1951–1983, 2011.

11. D. E. Knuth. *The Stanford GraphBase - a platform for combinatorial computing*. ACM, 1993.

12. D. D. Lee and H. S. Seung. Algorithms for non-negative matrix factorization. In T. K. Leen, T. G. Dietterich, and V. Tresp, editors, *Advances in Neural Information Processing Systems 13*, pages 556–562. MIT Press, 2001.

13. J. Leskovec, D. P. Huttenlocher, and J. M. Kleinberg. Predicting positive and negative links in online social networks. In *WWW*, pages 641–650, 2010.
14. J. Leskovec and A. Krevl. SNAP Datasets: Stanford large network dataset collection. http://snap.stanford.edu/data, June 2014.

15. J. Leskovec, K. J. Lang, and M. W. Mahoney. Empirical comparison of algorithms for network community detection. In WWW, pages 631–640, 2010.

16. D. Lusseau, K. Schneider, O. Boisseau, P. Haase, E. Slooten, and S. Dawson. The bottlenose dolphin community of Doubtful Sound features a large proportion of long-lasting associations. *Behavioral Ecology and Sociobiology*, 54(4):396–405, 2003.

17. M. E. J. Newman. Finding community structure in networks using the eigenvectors of matrices. *Phys. Rev. E*, 74, 2006.

18. M. E. J. Newman. Finding community structure in networks using the eigenvectors of matrices. *Phys. Rev. E*, 74:036104, 2006.

19. M. E. J. Newman and M. Girvan. Finding and evaluating community structure in networks. *Phys. Rev. E*, 69(2):026113, Feb. 2004.

20. H. Shen, X. Cheng, K. Cai, and M. Hu. Detect overlapping and hierarchical community structure in networks. *Physica A*, 388(8):1706–1712, 2009.

21. D. J. Watts, P. S. Dodds, and M. E. J. Newman. Collective dynamics of small-world networks. *Nature*, (393):440–442, 1998.

22. D. J. Watts and S. H. Strogatz. Collective dynamics of small-world networks. *nature*, 393(6684):440–442, 1998.

23. Z. W.W. An information flow model for conflict and fission in small groups. *Journal of Anthropological Research*, 33:452–473, 1977.

24. J. Yang and J. Leskovec. Community-affiliation graph model for overlapping network community detection. In *ICDM*, pages 1170–1175, 2012.

25. J. Yang and J. Leskovec. Overlapping community detection at scale: a nonnegative matrix factorization approach. In *WSDM*, pages 587–596, 2013.

26. J. Yang, J. J. McAuley, and J. Leskovec. Community detection in networks with node attributes. *CoRR*, abs/1401.7267, 2014.
# A Parallel SAT-based Framework for Closed Frequent Itemsets Mining

Imen Ouled Dlala ¹,³, Said Jabbour¹, Badran Raddaoui ², and Lakhdar Sais¹

¹CRIL-CNRS, Université d'Artois, F-62307 Lens Cedex, France

²SAMOVAR, Télécom SudParis, CNRS, Univ. Paris-Saclay, Evry, France

³LARODEC, University of Tunis, Tunisia

{dlala,jabbour,sais}@cril.fr,badran.raddaoui@telecom-sudparis.eu

**Abstract.** Constraint programming (CP) and propositional satisfiability (SAT) based framework for modeling and solving pattern mining tasks has gained a considerable audience in recent years. However, this nice declarative and generic framework encounters a scaling problem. The huge size of constraints networks/propositional formulas encoding large datasets is identified as the main bottleneck of most existing approaches. In this paper, we propose a parallel SAT based framework for itemset mining problem to push forward the solving efficiency. The proposed approach is based on a divide-and-conquer paradigm, where the transaction database is partitioned using item-based guiding paths. Such decomposition allows us to derive smaller and independent Boolean formulas that can be solved in parallel. The performance and scalability of the proposed algorithm are evaluated through extensive experiments on several datasets. We demonstrate that our partition-based parallel SAT approach outperforms other CP approaches even in the sequential case, while significantly reducing the performances gap with specialized approaches.

## 1 Introduction

Frequent itemset mining (abbreviated as FIM) [1,4] is a fundamental research topic in data mining (DM). It aims to discover important relationships between items in a database arising from numerous applications, ranging from marketing to scientific data analytics. Different kinds of interesting patterns and constraints have been introduced, including closeness and maximality constraints, association rules and its variants [1,3,36]. Such progress results in various scalable algorithms designed to deal with specific data mining tasks or constraints. However, such dedicated data mining systems are highly difficult to maintain when additional or combination of constraints came into play. This observation together with the increasing need in terms of user-preference led to the first and seminal paper by De Raedt et al. [28], opening a research avenue on the design of declarative approaches for itemset mining and for pattern mining in general. This new framework offers a flexible representation model that does not require any deep changes in the implementations. In other words, new constraints can be
easily integrated without developing specialized methods. These existing declar-
ative approaches for data mining clearly help pattern selection strategies such as
minimizing the redundancy or combining patterns on the basis of their usefulness
in a given context.

Encouraged by these promising results, several contributions addressed dif-
ferent data mining tasks using the well-known constraint programming (CP),
propositional satisfiability (SAT) and answer set programming (ASP) AI for-
malisms, such as frequent sequence mining [18,26,11], frequent itemset mining
[15], closed frequent itemset mining [22,30], association rules mining [5], cluster-
ing [7,6], and community detection [16,10]. A high-level language for constraint-
based mining, called MiningZinc, is introduced by Guns et al. [12]. It supports
a wide variety of different solvers, including DM algorithms and general pur-
pose solvers, and uses a significantly more high-level modeling language. This
combination of generic and specialized solvers gives MiningZinc the ability to be
both generic and efficient with respect to the performance of the state-of-the-art
algorithms on common data mining tasks.

In the first CP-based proposal for itemset mining [13], the problem is expressed through different linear and reified constraints over Boolean variables. This widely adopted model does not exploit some of the well established algorithmic skills from the state-of-the-art specialized algorithms. For the closed itemset mining task, to enhance the efficiency of such CP model, Lazaar et al. [22] proposed a new formulation using a global constraint that incorporates some of the propagation properties borrowed from specialized algorithms. This approach allows to capture the closed frequent itemset mining problem without requiring reified constraints or extra variables, leading to significantly better performances. More recently, Schaus et al. [30] introduced the CoverSize constraint for the itemset mining problem, a global constraint for counting and constraining the number of transactions covered by the itemset decision variables. The authors showed that compared to the ClosedPattern approach [22] using a global constraint for frequent closed itemset mining, both generality and efficiency can be significantly improved. A relation is established between the CoverSize constraint and the well-known table constraint, where the underlined filtering algorithm internally exploits the reversible sparse bitset data structure used for the filtering table. By expressing the size of the cover as a variable, the proposed approach opens up new modelling perspectives. Moreover, a SAT-based framework for enumerating Top-k Motifs in both transaction databases, sequences and sequences of itemsets is proposed in [20]. As a summary, this new framework offers a nice declarative and flexible representation model, while facing a real challenge in terms of scalability. Indeed, all these CP/SAT-based itemset mining approaches flag out good performance on datasets of reasonable size and high support threshold. However, the performance decreases as the database increases in size or the support threshold turns to be low. In this latter case, the size of constraints network/propositional formulas encoding the itemset mining task tends to be huge. Space complexity is clearly identified as
the main bottleneck behind the competitiveness of these new declarative and
flexible models w.r.t. specialized data mining approaches.

Some early efforts tried to speed up the specialized pattern mining algorithms
by running them in parallel [35,24,27]. Several parallel approaches use Spark or
MapReduce frameworks [33,23,38], through multi-core processors or distributed
computing platforms. For an overview of parallel FIM specialized methods, read-
ers are kindly referred to [25]. Moreover, Savasere et al. [29] addressed the problem
of generating association rules from large databases by introducing a new algo-
rithm which divides the database into a number of non-overlapping partitions.
The partitions are considered one at a time and all large itemsets for that par-
tition are generated.

In spite of the significance of the declarative framework for frequent pattern
mining, and despite of their main scalability bottleneck, no advances have been
made on parallelizing CP/SAT-based pattern mining approaches. To avoid the
generation of a single huge propositional formula encoding the whole transaction
database, in [19], the authors proposed an incremental approach allowing to par-
tition the whole problem into sub-problems of reasonable size while maintaining
incremental solving. It takes as input a transaction database and a partition of
the set of items, then it incrementally generates and sequentially solves a se-
quence of sub-problems while ensuring completeness. In this paper, we propose
a new parallel SAT based framework for Closed Frequent Itemset Mining (in
short paraSatMiner). Our proposed method is based on a divide-and-conquer
paradigm. The main idea is to decompose the input transaction database, using
item-based guiding paths, leading to sub-formulas that can be solved indepen-
dently in parallel. Our paraSatMiner approach is carefully implemented on a
multicore architecture, while maintaining workload balanced between the differ-
ent processor units. Extensive experimental comparative evaluation on several
datasets achieves significant performance improvements w.r.t. the two most re-
cent and effective CP approaches [22,30] even on the sequential case, while re-
ducing the performance gap against LCM, one of the state-of-the-art specialized
algorithms. We also show additional performance gains up to 8 cores. Contrary
to CP mining systems based on the design of specific global constraints, our ap-
proach does not integrate any technique or property from specialized algorithms.

2 Technical Background and Preliminary Definitions

## 2.1 Propositional Logic and SAT Problem

Let $\mathcal{L}$ be a propositional language defined from a finite set $\mathcal{PS}$ of propositional symbols ($p, q, r$, etc.). The set of formulas is defined inductively from $\mathcal{PS}$, the constant $\perp$ denoting false, the constant $\top$ denoting true, and using the classical logical connectives $\neg, \wedge, \vee, \rightarrow$ and the equivalence connective $\leftrightarrow$. For every two propositional formulas $\Phi$ and $\Psi$ from $\mathcal{L}$, the connective $\leftrightarrow$ is defined by $\Phi \leftrightarrow \Psi \equiv (\Phi \rightarrow \Psi) \wedge (\Psi \rightarrow \Phi)$. Moreover, we refer to the set of symbols from $\mathcal{PS}$ that occur in the formula $\Phi$ as $\mathcal{S}(\Phi)$.
A *boolean interpretation* $\mathcal{B}$ of a formula $\Phi$ is a truth assignement of $\mathcal{PS}$, that is, a total function from $\mathcal{S}(\Phi)$ to $\{0, 1\}$ (0 corresponds to false and 1 corresponds to true). For every two formulas $\Phi$ and $\Psi$ from $\mathcal{L}$, we have the following equivalences: $\mathcal{B}(\bot) = 0$, $\mathcal{B}(\top) = 1$, $\mathcal{B}(\neg\Phi) = 1 - \mathcal{B}(\Phi)$, $\mathcal{B}(\Phi \wedge \Psi) = \min(\mathcal{B}(\Phi), \mathcal{B}(\Psi))$, $\mathcal{B}(\Phi \vee \Psi) = \max(\mathcal{B}(\Phi), \mathcal{B}(\Psi))$, and $\mathcal{B}(\Phi \to \Psi) = \max(1 - \mathcal{B}(\Phi), \mathcal{B}(\Psi))$.

A *model* of a formula $\Phi$ is a boolean interpretation $\mathcal{B}$ that satisfies $\Phi$, i.e., $\mathcal{B}(\Phi) = 1$. A formula $\Phi$ is satisfiable if there exists a model of $\Phi$. We denote by $\mathcal{M}(\Phi)$ the set of all models of $\Phi$. Let $X \subseteq \mathcal{S}(\Phi)$ and $\mathcal{B} \in \mathcal{M}(\Phi)$, we define $\mathcal{B}^X = \{x \in X \mid \mathcal{B}(x) = 1\}$ and $\mathcal{M}^X(\Phi) = \{\mathcal{B}^X \mid \mathcal{B} \in \mathcal{M}(\Phi)\}$.

As usual, every finite set of formulas is considered as the conjunctive formula whose conjuncts are the elements of the set. A formula in *conjunctive normal form* (CNF) is a (finite) conjunction of clauses. A *clause* is a (finite) disjunction of literals. A *literal* is either a propositional variable $x$ of $\mathcal{PS}$ or its negation $\neg x$. Let us also mention that any propositional formula can be translated to a CNF formula equivalent w.r.t. satisfiability, using linear Tseitin's encoding [32]. The propositional satisfiability problem, called **SAT**, is the decision problem of determining the satisfiability of a CNF formula.

## 2.2 Parallel SAT Solving

Parallel SAT solving has received a lot of attention in the last years. This comes from several factors like the wide availability of cheap multicore platforms combined with the relative performance stall of sequential SAT solvers.

Many parallel SAT solvers have been previously proposed. Most of them are based on the divide-and-conquer principle. These solvers either divide the search space using for example guiding-paths [37,31] or the formula itself using decomposition techniques. The main issue behind these approaches rises in (i) getting the workload balanced between the different processing units, and (ii) selecting the most relevant guiding paths.

Portfolio-based parallel SAT solving has been recently introduced [14]. It avoids the previous problem by letting several DPLL engines compete and cooperate to be the first to solve a given instance. Each solver works on the original formula, and search spaces are not split or decomposed anymore. To be efficient, the portfolio has to use diversified search engines. This maximizes the chance of having one of them solving the problem. However, when clause sharing is added, diversification has to be restricted in order to maximize the impact of a foreign clause whose relevance is more important in a similar or related search effort. A challenging question is to maintain a good and relevant distance between the parts of the search space explored by the different search efforts which is equivalent to finding of a better diversification and intensification tradeoff.
These two parallel solving paradigms are complementary and admit their own strengths and weaknesses. As our goal is to partition the transactions database in order to generate several formulas of reasonable size, the divide-and-conquer based paradigm is clearly the most convenient for our purpose.
## 2.3 Itemset Mining Problem based on Boolean Satisfiability

Let $\Omega$ denote a universe of items (or symbols), called alphabet. A transaction database is a finite set of $n$ data records, called transactions, denoted by $\mathcal{D} = \{T_1, T_2, ..., T_n\}$. Each transaction $T_i$ ($1 \le i \le n$) is defined as a couple $(tid_i, \mathcal{I}_i)$, where $tid_i$ is the transaction identifier and $\mathcal{I}_i \subseteq \Omega$ an itemset, i.e., unordered collection of items from $\Omega$. We use $2^{\Omega}$ to denote the set of all possible itemsets over $\Omega$. Let $a \in \Omega$, we define $\mathcal{D} \downarrow_a = \{T \mid T = (tid, \mathcal{I}) \in \mathcal{D}, a \in \mathcal{I}\}$ the set of transactions containing $a$. We also define $\mathcal{D} \uparrow_a = \{(tid, \mathcal{I} \setminus \{a\}) \mid (tid, \mathcal{I}) \in \mathcal{D}\}$.

We associate to each $a \in \Omega$ a propositional variable denoted $l_a$. We note $\mathcal{P}$ such set of variables encoding the items in $\Omega$ and representing the candidate pattern. We also associate with each transaction $T_i$ ($1 \le i \le n$) a propositional variable $q_i$. We also note $\mathcal{Q}$ the set of variables associated to transactions. These variables will be used to express the following notions as propositional formulas.

**Definition 1 (Cover).** Let $\mathcal{D} = \{T_1, T_2, ..., T_n\}$ be a transaction database. The cover of an itemset $\mathcal{I} \subseteq \Omega$ in $\mathcal{D}$, denoted $\mathcal{C}(\mathcal{I}, \mathcal{D})$, corresponds to the following set of transaction identifiers: $\mathcal{C}(\mathcal{I}, \mathcal{D}) = \{tid \mid (tid, \mathcal{J}) \in \mathcal{D} \text{ and } \mathcal{I} \subseteq \mathcal{J}\}$.

For instance, if we consider the transaction database of Table 1, we have $\mathcal{C}(\{b\}, \mathcal{D}) = \{1, 2, 3, 4\}$ while $\mathcal{C}(\{a, b\}, \mathcal{D}) = \{1, 2, 3\}$.

<table><caption>Table 1: Transaction Database</caption><thead><tr><td>TID</td><td>Transactions</td></tr></thead><tbody><tr><td>T<sub>1</sub></td><td>a b c d</td></tr><tr><td>T<sub>2</sub></td><td>a b c e</td></tr><tr><td>T<sub>3</sub></td><td>a b e</td></tr><tr><td>T<sub>4</sub></td><td>b d</td></tr><tr><td>T<sub>5</sub></td><td>d f g</td></tr><tr><td>T<sub>6</sub></td><td>f g h</td></tr><tr><td>T<sub>7</sub></td><td>h</td></tr></tbody></table>

**Cover constraint:** The following constraint allows us to capture all the transactions where the candidate itemset does not appear:

$$ \Phi_{\mathcal{D}}^{\text{cov}} = \bigwedge_{i=1}^{n} (\neg q_i \leftrightarrow \bigvee_{a \in \Omega \setminus \mathcal{I}_i} l_a) \qquad (1) $$

This constraint means that $q_i$ is true if and only if the candidate itemset is in the transaction $T_i$.

**Definition 2 (Support).** Let $\mathcal{D} = \{T_1, T_2, ..., T_n\}$ be a transaction database. The support of an itemset $\mathcal{I} \subseteq \Omega$ in $\mathcal{D}$, denoted by $\mathcal{S}(\mathcal{I}, \mathcal{D})$, is defined as follows: $\mathcal{S}(\mathcal{I}, \mathcal{D}) = |\mathcal{C}(\mathcal{I}, \mathcal{D})|$.

From the transaction database of Table 1, we have $\mathcal{S}(\{a, b\}, \mathcal{D}) = 3$.
**Definition 3 (Frequent Itemset Mining).** Given a transaction database $D$ and $\theta$ an explicit frequency user-specified support threshold. The problem of frequent itemset mining, denoted $FIM(D, \theta)$, can be defined as follows:

$$FIM(D, \theta) = \{I \subseteq \Omega \mid S(I, D) \geq \theta\}$$

As an example, consider again the transaction database depicted by Table 1, we have $FIM(D, 2) = \{\{a\}, \{b\}, \{c\}, \{d\}, \{e\}, \{g\}, \{h\}, \{a, b\}, \{a, c\}, \{a, e\}, \{b, c\}, \{b, e\}, \{b, d\}, \{f, g\}, \{a, b, c\}, \{a, b, e\}\}$.

Let us note that the frequency is a monotonic property w.r.t. set inclusion, meaning that if an itemset is not frequent, none of its supersets are frequent. Similarly, if an itemset is frequent, all of its subsets are frequent.

**Frequency constraint:** To express that the candidate pattern occurs at least $\theta$ times, we use the following 0/1 linear inequality:

$$\Phi_{D, \theta}^{freq} = \sum_{i=1}^{n} q_i \geq \theta \qquad (2)$$

Then, the SAT-based encoding of $FIM(D, \theta)$ is expressed as: $\Phi_{D, \theta}^{fim} = \Phi_{D}^{cov} \wedge \Phi_{D, \theta}^{freq}$. Obviously, the monotonic property is implicitly satisfied by the frequency constraint. Notice also that the constraint (2) corresponds to the well known boolean cardinality constraint, subject of several efficient CNF encoding that maintain generalized arc consistency via unit propagation [34,2,17].

Now, in order to reduce the size of the huge number of extracted itemsets, condensed representations have been introduced, by exploiting the structure of the itemsets data. We define below closed frequent itemsets as one of these condensed representations.

**Definition 4.** (Closed Itemsets): Let $D$ be a transaction database. We say that the itemset $I$ is closed if and only if for all $J \supset I$, $S(I, D) > S(J, D)$.

**Closeness constraint:** The constraint allowing to force the candidate itemset to be closed can be expressed by the following propositional formula:

$$\Phi_{D}^{clos} = \bigwedge_{a \in \Omega} ((\bigvee_{(tid_i, I_i) \in D, a \notin I_i} q_i) \vee l_a) \qquad (3)$$

That is, this formula means that if we have $S(I, D) = S(I \cup \{a\}, D)$, then $a \in I$ holds. This condition is necessary and sufficient to force the candidate itemset to be closed. Let us note that an expression of the form $a \in I_i$ corresponds to a constant, i.e., $a \in I_i$ corresponds to $\top$ if the item $a$ is in $I_i$, to $\bot$ otherwise.

The closed frequent itemset mining task **CFIM** can then be encoded as $\Phi_{D, \theta}^{fim} = \Phi_{D}^{clos} \wedge \Phi_{D, \theta}^{fim}$, i.e., the conjunction of the formulas (1), (2) and (3). In the sequel, for clarity reasons and when there is no ambiguity, we simply note $\Phi_{D, \theta}^{fim}$ as $\Phi_{D}$.

Let us consider again the transaction database $D$ of Table 1. Assume that the minimum support threshold $\theta = 2$. Then, the closed frequent itemsets are: $\{b\}, \{h\}, \{a, b\}, \{b, d\}, \{f, g\}, \{a, b, c\}$ and $\{a, b, e\}$.
## 3 Partition-based Parallel SAT Approach for CFIM

Through an illustrative example, we start by highlighting some weaknesses of the SAT-based encoding of CFIM task described in Section 2.3.

**Example 1.** Let $\mathcal{D}$ be a transaction database made of two sub-bases $\mathcal{D}_1$ and $\mathcal{D}_2$ built over two disjoint sets of items $\Omega_1$ and $\Omega_2$, respectively. Formally, let $\mathcal{D}_1 = \{T_1, T_2, ..., T_j\}$ and $\mathcal{D}_2 = \{T_{j+1}, T_{j+2}, ..., T_n\}$, such that for each $T_i = (tid_i, I_i)$, we have $I_i \subseteq \Omega_1$ (resp. $I_i \subseteq \Omega_2$) for $1 \le i \le j$ (resp. $j+1 \le i \le n$). In the SAT encoding of $CFIM(\mathcal{D}, \theta)$, the propositional variables associated to the items in $\Omega_1$ are used in the encoding of the sub-base $\mathcal{D}_2$ and vis-versa. Indeed, the cover constraint $\Phi_D^{cov}$ (resp. closeness constraint $\Phi_D^{ clos}$) involves for each transaction $T_i = (tid_i, I_i) \in \mathcal{D}$ the propositional variables associated to the items $a \in \Omega \setminus I_i$ (resp. $a \in \Omega$), whereas $\mathcal{D}$ is made of two independent transaction databases $\mathcal{D}_1$ and $\mathcal{D}_2$. In this worst case illustrative example, the encoding leads to a formula with a high number of large clauses. Indeed, the weakness of SAT-based approaches is the size of the encoding, which for large formulas can outgrow available memory or can make SAT solving otherwise inefficient.

To overcome this drawback, a possible encoding is to express the problem as two independent propositional formulas $\Phi_{\mathcal{D}_1}$ and $\Phi_{\mathcal{D}_2}$. An alternative compact encoding of the itemset mining task on the whole database $\mathcal{D}$ can be expressed as a single propositional formula:

$$ \Phi_{\mathcal{D}} = [y \rightarrow (\Phi_{\mathcal{D}_1} \wedge \bigwedge_{l_a \in \Omega_2} \neg l_a)] \wedge [\neg y \rightarrow (\Phi_{\mathcal{D}_2} \wedge \bigwedge_{l_a \in \Omega_1} \neg l_a)] \quad (4) $$

The formula (4) allows us to split in an efficient way the patterns of $\mathcal{D}_1$ and $\mathcal{D}_2$. Assigning $y$ to true (resp. false) leads to the enumeration of the models of $\Phi_{\mathcal{D}_1}$ (resp. $\Phi_{\mathcal{D}_2}$), where the propositional variables associated to the items from $\Omega_2$ (resp. $\Omega_1$) are assigned by unit propagation to false. Interestingly, the formula (4) can be easily translated into clausal form.

Clearly, the previous example illustrates the motivation behind partitioning the transaction database for an efficient SAT based itemsets enumeration tasks. The benefits are twofold: the size of the encoding can be reduced significantly while improving solving efficiency. Unfortunately, disjoint sub-bases are not very common in real datasets and there recognition is not an easy task. Nevertheless, partitioning can be performed differently. In fact, for a transaction database $\mathcal{D}$ and an item $a$, the set of frequent closed itemsets can be partitioned into those containing $a$ (models of $\Phi_D \wedge l_a$) and those without $a$ (models of $\Phi_D \wedge \neg l_a$). Interestingly, the models of $\Phi_D \wedge l_a$ are those of $\Phi_{D \downarrow a}$. While the models of $\Phi_D \wedge \neg l_a$ correspond to those of $\Phi_{D \uparrow a} \wedge \Psi_{D,a}$, where $\Psi_{D,a}$ is defined as:

$$ \Psi_{D,a} = \bigvee_{(tid_i, I_i) \in \mathcal{D}, a \notin I_i} q_i $$

Adding $\Psi_{D,a}$ allows to avoid such redundancies. In this way, any model of $\Phi_{D \uparrow a} \wedge \Psi_{D,a}$ must correspond to a pattern that covers at least one transaction not
containing a. Let us note that the constraint $\Psi_{D,a}$ can be derived from the closure constraint (3) by assigning $l_a$ to false.

As a summary, the assignment of the variable $l_a$ to true allows to restrict the mining process to the transactions containing the item a, while setting $l_a$ to false allows to remove the item a from the database $D$ with the addition of $\Psi_{D,a}$, so that to avoid redundancy.

Clearly, a less frequent item $a_1$ might lead to a CNF formula $\Phi_D \wedge l_{a_1}$ of reasonable size. But, $\Phi_D \wedge \neg l_{a_1}$ can remain very huge. Fortunately, the previous partitioning principle can be applied recursively on $\Phi_D \wedge \neg l_{a_1}$ by choosing other items. For example, if we choose a second item $a_2$, the formula $\Phi_D \wedge \neg l_{a_1}$ can also be divided into $\Phi_D \wedge \neg l_{a_1} \wedge l_{a_2}$ and $\Phi_D \wedge \neg l_{a_1} \wedge \neg l_{a_2}$. Let us note that $\Phi_D \wedge \neg l_{a_1} \wedge l_{a_2}$ is equivalent to $\Phi_{D\uparrow a_1\downarrow a_2}$. Figure 1 shows this recursive partitioning process.

<figure><img src="image_45.png" /><figcaption>Fig. 1: Item-based guiding paths tree</figcaption></figure>

Finally, if $\Omega = \{a_1, \dots, a_m\}$, then the models of $\Phi_D$ can be partitioned into disjoint sets of models as stated in Proposition 1.

**Proposition 1.** Let $D$ be a transaction database over $\Omega$. Then,

$$M^P(\Phi_D) = \bigcup_{i=1}^{m} M^P(\Phi_D^{a_i}), \quad \text{and} \quad M^P(\Phi_D^{a_i}) \cap M^P(\Phi_D^{a_j}) = \emptyset \quad (1 \le i < j \le m)$$

$$\text{where } \Phi_D^{a_i} = (\Phi_{D\downarrow a_i} \uparrow_{a_1} \dots \uparrow_{a_{i-1}} \wedge \bigwedge_{1 \le j < i} (\Psi_{D\downarrow a_i, a_j}).$$

*Proof (Sketch).* Using the sequence of totally ordered set of items $a_1, a_2, \dots, a_m$, the formula $\Phi_D$ can be decomposed into a sequence of formulas $\Phi_D^{a_1}, \Phi_D^{a_2}, \dots$, and $\Phi_D^{a_m}$. This partition by the set of item-based guiding paths is complete as depicted in Figure 1. Indeed, starting with the item $a_1$, the models of $\Phi_D$ correspond to the patterns of $D$ restricted to transaction containing $a_1$. The models of $\Phi_D$ correspond to the patterns of $D$ restricted to transactions containing $a_2$ while removing the item $a_1$. The constraint $\Psi_{D\downarrow a_2, a_1} = \bigvee_{(tid_i, \mathcal{I}_i) \in D\downarrow a_2}, a_1 \notin \mathcal{I}_i$ $q_i$ allows us to generate patterns that cover at least one additional transaction containing $a_2$ and not $a_1$, and so on.
**Remark 1.** As $\Phi_D$ corresponds to the SAT-based encoding of CFIM($D, \theta$), the constraint $\Psi_{D,a}$ avoiding patterns redundancy is derived from the closeness constraint (3) each time an item $a$ is removed from $D$ (i.e., $D \uparrow_a$) or equivalently $l_a$ is assigned to false (i.e., $\Phi_D \wedge \neg l_a$). Obviously, the formulas $\Phi_D^{a_i} \wedge l_{a_i}$ and $\Phi_D \wedge l_{a_i} \wedge \neg l_{a_1} \wedge \dots \wedge \neg l_{a_{i-1}}$ admit the same models over $\mathcal{P}$. However, as our goal is to partition the encoding of $D$ into several independent formulas of reasonable size, it is better to consider $\Phi_D^{a_i}$, where the encoding is done after restricting $D$ to transactions containing $a_i$, removing the items $a_1, \dots, a_{i-1}$ and adding the constraint $\bigwedge_{1 \le j < i} (\Psi_{D \downarrow a_j, a_j})$, than propagating the literals $l_{a_i} \wedge \neg l_{a_1} \wedge \dots \wedge \neg l_{a_{i-1}}$ on the formula encoding the whole transaction database.

As explained in Section 2.2, divide-and-conquer is an usual way for parallelizing SAT solvers. This strategy uses the notion of guiding path to split the search space. Each derived sub-formula is solved using a sequential SAT solver running on a particular processor. In fact, partitioning the search space can be done statically or dynamically in order to avoid the idleness of threads. Additionally, workload balancing is another criteria allowing to distribute approximately equal amounts of work among processors over time. In this paper, we consider a static divide-and-conquer approach, i.e., the set of guiding paths are generated in a preprocessing step. Our partition-based approach is based on the set of formulas $\Phi_D^{a_i}$ (see Proposition 1). We denote by $g^{a_i}$ the $i$th guiding path defined as: $g^{a_i} = \neg l_{a_1} \wedge \dots \wedge \neg l_{a_{i-1}} \wedge l_{a_i}$. The guiding path $g^{a_i}$ allows us to both restrict the search on a subset of transactions involving only $a_i$, with the items $a_j$ ($1 \le j < i$) removed. Each guiding path $g^{a_i}$ leads to a formula $\Phi_{g^{a_i}} = \Phi_D \wedge g^{a_i}$ associated to the $i$th branch of the item-based guiding paths tree depicted in Figure 1. As $\Phi_D$ is the propositional formula encoding CFIM($D, \theta$), the two formulas $\Phi_D^{a_i}$ and $\Phi_D^{a_j}$ are equivalent. Naturally, each guiding path $g^{a_i}$ can be extended with additional items to further reduce the size of the associated formula.

Notice that the total ordering over $\Omega$ used to generate the guiding paths greatly impacts the size of the associated sequence of formulas and therefore it can significantly affect the performance. Finding the best ordering for an efficient parallelization is clearly a challenging issue. Our goal is then to decompose the encoding into smaller propositional formulas in order to efficiently balance the load between the different cores. Definitions 5 and 6 formalize this issue.

**Definition 5.** Given a transaction database $\mathcal{D}$ on $\Omega = \{a_1, \dots, a_m\}$. Let $\sigma$ be a permutation over $\Omega$. We define $G^{\Omega, \sigma} = \{g^{\sigma(a_1)}, \dots, g^{\sigma(a_m)}\}$ as the set of guiding paths over $\Omega$ w.r.t. $\sigma$. We also define $\Phi(\mathcal{D}, \sigma)$ as the set of propositional formulas encoding $\mathcal{D}$ w.r.t. $\sigma$, i.e., $\Phi(\mathcal{D}, \sigma) = \{\Phi_{g^{\sigma(a_1)}}, \dots, \Phi_{g^{\sigma(a_m)}}\}$.

Finding an appropriate permutation is a hard task. In fact, the relevance of such permutation depends on the overall complexity of the model enumeration process on the associated formulas. Considering the size of the formula as a complexity measure, the issue can be formulated as an optimization problem:

**Definition 6.** Let $\mathcal{D}$ be a transaction database on $\Omega$. We define the Best Items Decomposition Ordering Problem as the problem of finding the best permutation $\sigma$ that leads to a set of formulas encoding $\mathcal{D}$ while minimizing the size of
the largest formula in $\Phi(D, \sigma)$: $\sigma^* = \arg \min_{\sigma \in \mathcal{P}_{\text{perm}}(\Omega)} \max\{|\phi|, \phi \in \Phi(D, \sigma)\}$, where $\mathcal{P}_{\text{perm}}(\Omega)$ is the set of all permutations over $\Omega$.

The main idea is to reduce the overall computational complexity of the model enumeration task among all the generated formulas under the set of guiding paths. Note that the size of each formula $\Phi_{g^{\sigma(a_i)}}$ depends on the number of transactions involving $\sigma(a_i)$ and on the frequency of $\sigma(a_j)$ for ($j < i$) in such transactions. From this observation, as a decomposition ordering we consider items from the less frequent to the most frequent one. This static ordering, easy to compute, proved to be a good compromise as shown in our experiments.

Algorithm 1, called paraSatMiner, summarizes the main components of our partition-based parallel SAT approach for CFIM. It takes as input a transaction database $D$ over $\Omega$, a permutation $\sigma$ on $\Omega$, a minimum support threshold $\theta$ and a fixed number of threads (cores), and returns the set of closed frequent itemsets as output. The number of threads is less or equal to the number of items ($n \le m$). The set of items are sorted in ascending order according to their frequency, i.e., the permutation $\sigma$ over $\Omega$ satisfies the following condition: $\forall 1 \le i < j \le m, S(D, \{\sigma(a_i)\}) \le S(D, \{\sigma(a_j)\})$. First, the SAT-based model enumeration solvers are initialized. Each one is associated to a given thread or core $i$, while initializing the set of models $M_i$ returned by each thread $i$ to an empty-set (lines 1-4). Now, the $n$ model enumeration solvers are launched in parallel (lines 7-11). For example, the solver $i$ is run successively on the formulas $\Phi_D^{\sigma(a_{i+k \times n})}$ corresponding to the guiding paths (or branches) number ($i+k \times n \le m$. The set of models computed by the solver $i$ are collected in the set variable $M_i$. In this way, the solver $i$ is run on the formulas $\Phi_D^{\sigma(a_i)}, \Phi_D^{\sigma(a_{i+n})}, \Phi_D^{\sigma(a_{i+2 \times n})}, \dots, \Phi_D^{\sigma(a_{i+k \times n})}$, with $i+k \times n \le m$. As the items are ordered according to their frequency, the sequences of formulas associated to the $n$ model enumeration solvers are approximately of closer sizes. This allows us to ensure load balancing between the different solvers. Finally, in lines 12-14, the set of closed frequent itemsets are collected by merging the model enumerated by each thread, projected on the variables encoding the itemsets $\mathcal{P}$.

# 4 Experimental Results

In this section, we evaluate the performance of paraSatMiner. The proposed parallel SAT mining solver is implemented using a model enumeration solver based on MiniSAT [9]. As our approach is based on the enumeration of all models of a propositional formula, we propose an extension of MiniSAT solver based on the DPLL (Davis-Putnam-Logemann-Loveland) procedure [8] to deal with this fundamental problem, marginally explored in the SAT community. More precisely, each time a model is found, a chronological backtracking is performed while inhibiting the restart component to ensure completeness. We also use OpenMP as an API that supports multi-platform shared memory multiprocessing programming in C and C++. Let us note that the cardinality constraints representing the support constraint is managed on the fly inside the solver. We also use the well-known MOMS variable ordering heuristic [21].
<caption>**Algorithm 1:** Parallel SAT for Closed Frequent Itemset Mining (paraSat-Miner)</caption>

**Input:** $\mathcal{D}$: a transaction database, $\Omega = \{a_1, ..., a_m\}$: a set of items, $\sigma$: a permutation over $\Omega$ (ordering), $\theta$: a minimum support threshold, $n$: number of Threads
**Output:** The set of Closed Frequent Itemsets $CFIM(\mathcal{D}, \theta)$
1 &nbsp; **foreach** $i \in \{1, ..., n\}$ **do**
2 &nbsp;&nbsp;&nbsp;&nbsp; **initEnumSatSolver**($i$);
3 &nbsp;&nbsp;&nbsp;&nbsp; $\mathcal{M}_i = \emptyset$;
4 &nbsp; **end**
5 &nbsp; $S = \emptyset$;
6 &nbsp; $k = 0$;
7 &nbsp; # in parallel;
8 &nbsp; **if** ($i + k \times n \le |\Omega|$) **then**
9 &nbsp;&nbsp;&nbsp;&nbsp; $\mathcal{M}_i \leftarrow \mathcal{M}_i \cup \text{enumModels}(\text{enumSatSolver}_i, \Phi_D^{\sigma(a_i+k \times n)})$;
10 &nbsp;&nbsp;&nbsp;&nbsp; $k$++;
11 &nbsp; **end**
12 &nbsp; **foreach** $i \in \{1, ..., n\}$ **do**
13 &nbsp;&nbsp;&nbsp;&nbsp; $S = S \cup \mathcal{M}_i^P$;
14 &nbsp; **end**
15 &nbsp; **Return** $S$

All the experiments were done on Intel Xeon quad-core machines with 32GB of RAM running at 2.66 Ghz. To evaluate the practical performance of our approach, we run the experiments on different datasets, taken from FIMI <fnref n="1" /> and CP4IM<fnref n="2" /> repositories. For each instance, we fix a timeout of 1000 seconds of CPU time. Table 2 presents the characteristics of the evaluated datasets. For each instance, we report the number of transactions (#Transactions), the number of items (#Items), the density, and the size of the dataset in bytes.

For our experiments, we denote by **paraSatMiner**-*c*<fnref n="3" /> our parallel SAT solver based itemset enumeration where (*) indicates the number of threads. We compare the performance of our approach with the following most prominent state-of-the-art CP-based CFIM systems: ClosedPattern<fnref n="4" />,<fnref n="5" /> and CoverSize<fnref n="6" />. As mentioned previously, ClosedPattern and CoverSize encode the closeness constraint as global constraints. These CP mining systems are implemented in C++ and Java using the or-tools solver [22] (or choco for the recent version) and the OscaR solver [30], respectively. In addition, we consider LCM<fnref n="7" /> known as the best specialized solver for frequent (closed) itemset mining. We perform two

<footnote n="1">¹http://fimi.ua.ac.be/data/</footnote>

<footnote n="2">²http://dtai.cs.kuleuven.be/CP4IM/datasets/</footnote>

<footnote n="3">³http://www.cril.univ-artois.fr/decMining/</footnote>

<footnote n="4">⁴http://www.lirmm.fr/~lazaar/cpminer.html</footnote>

<footnote n="5">⁵https://lemierev.users GREYC.fr/closedpattern/</footnote>

<footnote n="6">⁶https://www.info.ucl.ac.be/~pschaus</footnote>

<footnote n="7">⁷http://research.nii.ac.jp/~uno/code/lcm.html</footnote>
kinds of experiments. In the first evaluation, we carry out a comparison with all the considered itemset mining systems. In this case, **paraSatMiner** is run using 1 core as a sequential solver. In the second, we show that the performance of our **paraSatMiner** can be improved by increasing the number of threads. In this case, we vary the number of cores from 1 to 8.

<table><caption>Table 2: Data Characteristics</caption><thead><tr><td>Instance</td><td>#Transactions</td><td>#Items</td><td>Density</td><td>Size</td></tr></thead><tbody><tr><td>chess</td><td>3196</td><td>75</td><td>49.0%</td><td>340K</td></tr><tr><td>mushroom</td><td>8124</td><td>119</td><td>19.0%</td><td>516K</td></tr><tr><td>BMS-WebView-1</td><td>59601</td><td>497</td><td>0.5%</td><td>940K</td></tr><tr><td>T10I4D100K</td><td>100000</td><td>870</td><td>1.0%</td><td>3.9M</td></tr><tr><td>retail</td><td>88162</td><td>16470</td><td>0.06%</td><td>4.2M</td></tr><tr><td>connect</td><td>67558</td><td>129</td><td>35.62%</td><td>8.9M</td></tr><tr><td>T40I10D100K</td><td>100000</td><td>942</td><td>4.31%</td><td>15M</td></tr><tr><td>pumsb</td><td>49046</td><td>2113</td><td>3.0%</td><td>16.7M</td></tr><tr><td>kosarak</td><td>990002</td><td>41267</td><td>0.01%</td><td>32M</td></tr><tr><td>accidents</td><td>340183</td><td>468</td><td>7.0%</td><td>34M</td></tr></tbody></table>

## 4.1 Sequential Evaluation

Table 3 reports the comparative results of the considered systems using different minimum support threshold values. For each dataset, the number of models (patterns) and the total CPU time (in seconds) are given. For **CoverSize**, we also mention in parenthesis the solving CPU time without including the time spent for loading and encoding the instance. (`--`) means that the solver is not able to finish the enumeration under the fixed time out. According to the results, our **ParaSatMiner-1c** (with 1 core) solver outperforms considerably the CP approaches on almost all the datasets with several factors of magnitudes of gain. For instance, our approach allows to enumerate all the models of **connect** data in 180 seconds for $\theta = 5000$ when both **ClosedPattern** and **CoverSize** timed out. Except for **T10I4D100K** and $\theta = 50$, where **CoverSize** is the best. For all the remaining tested values, **ParaSatMiner-1c** is clearly the best. Interestingly, on the **kosarak** data with 990002 transactions the two CP systems are not able to enumerate the whole set of models under the time limit for all $\theta$ values. For the comparison with specialized algorithms, even if our approach reduced the performance gap, the **LCM** algorithm remains the best system.

<table><caption>Table 3: **paraSatMiner** vs (ClosedPattern, CoverSize, LCM)</caption><thead><tr><th>Instance</th><th>θ</th><th>Closed Pattern</th><th>Cover Size</th><th>paraSat Miner-1c</th><th>LCM</th><th>#Models</th></tr></thead><tbody><tr><td rowspan="5">retail</td><td>80</td><td>–</td><td>265.10 (42.84)</td><td>14.06</td><td>0.21</td><td>> 8.10<sup>3</sup></td></tr><tr><td>60</td><td>–</td><td>295.47 (72.04)</td><td>18.07</td><td>0.24</td><td>> 1.10<sup>4</sup></td></tr><tr><td>40</td><td>–</td><td>334.23 (113.14)</td><td>25.33</td><td>0.28</td><td>> 2.10<sup>4</sup></td></tr><tr><td>20</td><td>–</td><td>439.94 (216.68)</td><td>41.93</td><td>0.35</td><td>> 5.10<sup>4</sup></td></tr><tr><td>10</td><td>–</td><td>586.16 (361.71)</td><td>76.49</td><td>0.56</td><td>> 1.10<sup>5</sup></td></tr><tr><td rowspan="4">connect</td><td>40000</td><td>7.54</td><td>14.95 (9.67)</td><td>7.25</td><td>0.17</td><td>> 7.10<sup>4</sup></td></tr><tr><td>20000</td><td>50.22</td><td>75.48 (70.40)</td><td>22.73</td><td>0.55</td><td>> 5.10<sup>5</sup></td></tr><tr><td>10000</td><td>526.43</td><td>431.19 (426.34)</td><td>68.88</td><td>2.68</td><td>> 3.10<sup>6</sup></td></tr><tr><td>5000</td><td>–</td><td>–</td><td>179.17</td><td>9.82</td><td>> 1.10<sup>7</sup></td></tr></tbody></table>

*Continued on next page*
<table><caption>Table 3: paraSatMiner vs (ClosedPattern, CoverSize, LCM)</caption><thead><tr><th>Instance</th><th>θ</th><th>Closed Pattern</th><th>Cover Size</th><th>paraSat Miner-1c</th><th>LCM</th><th>#Models</th></tr></thead><tbody><tr><td rowspan="5">chess</td><td>2000</td><td>1.51</td><td>1.22 (0.51)</td><td>0.25</td><td>0.04</td><td>≈ 7.10<sup>4</sup></td></tr><tr><td>1500</td><td>6.30</td><td>4.09 (3.38)</td><td>0.8</td><td>0.20</td><td>> 5.10<sup>5</sup></td></tr><tr><td>1000</td><td>51.35</td><td>28.62 (27.93)</td><td>5.52</td><td>1.75</td><td>> 4.10<sup>6</sup></td></tr><tr><td>500</td><td>577.29</td><td>311.47 (310.74)</td><td>49.50</td><td>18.25</td><td>> 45.10<sup>6</sup></td></tr><tr><td>250</td><td>-</td><td>-</td><td>186.11</td><td>72.96</td><td>≈ 2.10<sup>8</sup></td></tr><tr><td>100</td><td>-</td><td>-</td><td>484.41</td><td>215.30</td><td>> 5.10<sup>8</sup></td></tr><tr><td rowspan="4">accidents</td><td>100000</td><td>101.68</td><td>145.96 (81.84)</td><td>74.14</td><td>1.72</td><td>≈ 1.10<sup>5</sup></td></tr><tr><td>80000</td><td>319.25</td><td>283.98 (220.86)</td><td>141.29</td><td>3.53</td><td>≈ 4.10<sup>5</sup></td></tr><tr><td>60000</td><td>-</td><td>866.21 (804.33)</td><td>299.94</td><td>5.66</td><td>> 1.10<sup>6</sup></td></tr><tr><td>40000</td><td>-</td><td>-</td><td>735.39</td><td>10.59</td><td>≈ 6.10<sup>6</sup></td></tr><tr><td rowspan="4">pumbs</td><td>40000</td><td>20.99</td><td>389.43 (1.83)</td><td>4.78</td><td>0.13</td><td>> 2.10<sup>4</sup></td></tr><tr><td>35000</td><td>103.20</td><td>325.42 (19.54)</td><td>10.33</td><td>0.25</td><td>≈ 2.10<sup>5</sup></td></tr><tr><td>30000</td><td>434.25</td><td>404.26 (97.85)</td><td>27.72</td><td>0.59</td><td>≈ 9.10<sup>5</sup></td></tr><tr><td>25000</td><td>-</td><td>994.35 (690.09)</td><td>147.64</td><td>3.18</td><td>≈ 6.10<sup>6</sup></td></tr><tr><td>20000</td><td>-</td><td>-</td><td>669.93</td><td>17.69</td><td>> 3.10<sup>7</sup></td></tr><tr><td rowspan="5">T40I10D100K</td><td>10000</td><td>4.16</td><td>51.43 (0.145)</td><td>3.15</td><td>0.34</td><td>≈ 1.10<sup>2</sup></td></tr><tr><td>8000</td><td>5.08</td><td>51.13 (0.352)</td><td>4.07</td><td>0.54</td><td>> 1.10<sup>2</sup></td></tr><tr><td>6000</td><td>10.38</td><td>52.39 (0.912)</td><td>6.43</td><td>0.79</td><td>> 2.10<sup>2</sup></td></tr><tr><td>4000</td><td>30.51</td><td>53.26 (2.221)</td><td>9.59</td><td>1.00</td><td>> 4.10<sup>2</sup></td></tr><tr><td>2000</td><td>144.89</td><td>58.22 (7.378)</td><td>22.74</td><td>1.64</td><td>> 1.10<sup>3</sup></td></tr><tr><td rowspan="5">T10I4D100K</td><td>500</td><td>106.87</td><td>24.04 (6.91)</td><td>2.90</td><td>0.35</td><td>> 1.10<sup>3</sup></td></tr><tr><td>400</td><td>147.14</td><td>25.56 (8.32)</td><td>3.32</td><td>0.37</td><td>> 1.10<sup>3</sup></td></tr><tr><td>300</td><td>217.40</td><td>27.73 (10.69)</td><td>4.31</td><td>0.40</td><td>> 4.10<sup>3</sup></td></tr><tr><td>200</td><td>314.17</td><td>29.12 (11.98)</td><td>6.16</td><td>0.44</td><td>> 1.10<sup>4</sup></td></tr><tr><td>100</td><td>497.10</td><td>32.40 (15.14)</td><td>14.66</td><td>0.48</td><td>> 2.10<sup>4</sup></td></tr><tr><td>50</td><td>-</td><td>45.05 (27.80)</td><td>76.37</td><td>0.58</td><td>> 4.10<sup>4</sup></td></tr><tr><td rowspan="4">Online-Retail</td><td>70</td><td>-</td><td>211.71 (97.76)</td><td>31.66</td><td>0.82</td><td>≈ 6.10<sup>3</sup></td></tr><tr><td>40</td><td>-</td><td>233.34 (120.48)</td><td>34.64</td><td>0.85</td><td>> 6.10<sup>3</sup></td></tr><tr><td>10</td><td>-</td><td>253.64 (141.61)</td><td>39.94</td><td>0.82</td><td>≈ 8.10<sup>3</sup></td></tr><tr><td>5</td><td>-</td><td>267.96 (156.74)</td><td>41.79</td><td>0.90</td><td>> 8.10<sup>3</sup></td></tr><tr><td rowspan="4">Kosarak</td><td>4000</td><td>-</td><td>-</td><td>29.37</td><td>1.32</td><td>> 2.10<sup>3</sup></td></tr><tr><td>3000</td><td>-</td><td>-</td><td>39.98</td><td>1.61</td><td>> 4.10<sup>3</sup></td></tr><tr><td>2000</td><td>-</td><td>-</td><td>65.12</td><td>2.16</td><td>> 3.10<sup>4</sup></td></tr><tr><td>1000</td><td>-</td><td>-</td><td>145.65</td><td>3.43</td><td>≈ 5.10<sup>5</sup></td></tr><tr><td rowspan="5">mushroom</td><td>250</td><td>1.14</td><td>2.54 (0.50)</td><td>1.33</td><td>0.05</td><td>> 1.10<sup>4</sup></td></tr><tr><td>100</td><td>1.64</td><td>1.91 (1.07)</td><td>1.94</td><td>0.06</td><td>> 3.10<sup>4</sup></td></tr><tr><td>50</td><td>2.70</td><td>2.47 (1.63)</td><td>2.44</td><td>0.09</td><td>> 5.10<sup>4</sup></td></tr><tr><td>25</td><td>2.82</td><td>3.16 (2.27)</td><td>2.90</td><td>0.11</td><td>≈ 8.10<sup>4</sup></td></tr><tr><td>5</td><td>5.57</td><td>4.20 (3.33)</td><td>3.90</td><td>0.17</td><td>> 1.10<sup>5</sup></td></tr><tr><td rowspan="5">BMS-WebView-1</td><td>48</td><td>203.51</td><td>220.67 (1.43)</td><td>8.69</td><td>0.06</td><td>> 9.10<sup>3</sup></td></tr><tr><td>36</td><td>833.76</td><td>220.20 (3.32)</td><td>10.08</td><td>0.16</td><td>> 6.10<sup>4</sup></td></tr><tr><td>34</td><td>-</td><td>219.19 (4.79)</td><td>10.50</td><td>0.21</td><td>> 8.10<sup>4</sup></td></tr><tr><td>32</td><td>-</td><td>227.80 (8.19)</td><td>10.89</td><td>0.32</td><td>> 1.10<sup>5</sup></td></tr><tr><td>30</td><td>-</td><td>231.89 (14.88)</td><td>11.37</td><td>0.53</td><td>> 1.10<sup>5</sup></td></tr></tbody></table>

## 4.2 Parallel Evaluation

On the parallel side, we perform the same experiments by varying the number of cores from 1 to 8 and by considering several minimum support threshold values. Figure 2 shows the obtained results on a representative sample of dataset. A first remark is that the parallel approach allows us to reduce considerably the
computation time. By increasing the number of cores, the time always decreases. The impressive gain is obtained from 1 to 2 cores as shown by Figure 2. For the transition from 4 to 8 cores, the gain is not very impressive. Overall, the strategy used to generate guiding paths by considering the less frequent items first is successful. For instance for pumsb data and $\theta = 2000$, the time is reduced from 700 seconds with 1 core to less than 200 seconds with 8 cores.

<figure><img src="image_46.png" /><figcaption>Fig. 2: Performance gain w.r.t. the number of cores</figcaption></figure>

## 4.3 Load Balancing

Finally, to assess the suitability of our load balancing strategy, we consider the datasets pumsb and T10I4D100K and we provide an empirical analysis of the number of models discovered by the different cores. Using the 4 (resp. 8) cores configuration, for each value of $\theta$ we report the average number of models among the 4 (resp. 8) cores (the curve), while mentioning the minimum and the maximum number of models (the interval) (see Figure 3). We note that the load
balancing strategy is better when the minimum and maximum number of models among those returned by the different cores are close to the average number of models. As we can observe, for T10I4D100K, our strategy is clearly interesting. Indeed, the relative load unbalancing is very limited. All the cores find approximately the same number of models. However, the load unbalancing is relatively high for pumsb, mainly for the transition between 4 to 8 cores.

Overall, our guiding paths generation strategy allows to balance the number of models between the different threads. These results indicate that our method is both efficient and scalable.

<figure><img src="image_47.png" /><figcaption>Fig. 3: Load unbalancing between cores</figcaption></figure>

# 5 Conclusion

In this paper, we proposed a parallel SAT-based framework for CFIM. We show that partitioning the formula using predefined guiding paths allows to push forward the performance of SAT-based itemset mining frameworks. Even in the sequential configuration, our approach outperforms the existing CP-based approaches while reducing considerably the time needed to compute all the itemsets. We have shown that such approach scales well and presents good load balancing among the different cores.

This work can be extended in different ways. First, we would like to consider a dynamic partitioning strategy. We also plan to implement a distributed version to handle very large datasets. Last, we plan to tackle other DM problems like discriminative itemsets, association rules mining, and skypatterns tasks.
References

1. R. Agrawal, T. Imieliński, and A. Swami. Mining association rules between sets of items in large databases. In *ACM SIGMOD International Conference on Management of Data*, pages 207–216, 1993.

2. O. Bailleux and Y. Boufkhad. Efficient CNF encoding of boolean cardinality constraints. In *International Conference on Principles and Practice of Constraint Programming CP*, pages 108–122, 2003.

3. Y. Bastide, N. Pasquier, R. Taouil, G. Stumme, and L. Lakhal. Mining minimal non-redundant association rules using frequent closed itemsets. In *Computational Logic*, volume 1861, pages 972–986, 2000.

4. C. Borgelt. Frequent item set mining. *Wiley Int. Rev. Data Min. and Knowl. Disc.*, 2(6):437–456, Nov. 2012.

5. A. Boudane, S. Jabbour, L. Sais, and Y. Salhi. A sat-based approach for mining association rules. In *IJCAI*, pages 2472–2478, 2016.

6. A. Boudane, S. Jabbour, L. Sais, and Y. Salhi. Clustering complex data represented as propositional formulas. In *Advances in Knowledge Discovery and Data Mining - 21st Pacific-Asia Conference, PAKDD 2017, Jeju, South Korea, May 23-26, 2017, Proceedings, Part II*, pages 441–452, 2017.

7. T. Dao, K. Duong, and C. Vrain. Constrained clustering by constraint programming. *Artif. Intell.*, 244:70–94, 2017.

8. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. *Communications of the ACM*, 5:394–397, 1962.

9. N. En and N. Srensson. An extensible sat-solver. In *Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03)*, pages 502–518, 2002.

10. M. Ganji, J. Bailey, and P. J. Stuckey. A declarative approach to constrained community detection. In *International Conference on Principles and Practice of Constraint Programming*, pages 477–494, 2017.

11. M. Gebser, T. Guyet, R. Quiniou, J. Romero, and T. Schaub. Knowledge-based sequence mining with ASP. In *International Joint Conference on Artificial Intelligence*, pages 1497–1504, 2016.

12. T. Guns, A. Dries, G. Tack, S. Nijssen, and L. D. Raedt. Miningzinc: A modeling language for constraint-based mining. In *International Joint Conference on Artificial Intelligence*, pages 1365–1372, 2013.

13. T. Guns, S. Nijssen, and L. D. Raedt. Itemset mining: A constraint programming perspective. *Artificial Intelligence*, 175(12-13):1951–1983, 2011.

14. Y. Hamadi, S. Jabbour, and L. Sais. Manysat: a parallel SAT solver. *JSAT*, 6(4):245–262, 2009.

15. R. Henriques, I. Lynce, and V. M. Manquinho. On when and how to use sat to mine frequent itemsets. *CoRR*, abs/1207.6253, 2012.

16. S. Jabbour, N. Mhadhbi, B. Raddaoui, and L. Sais. A sat-based framework for overlapping community detection in networks. In *Pacific-Asia Conference on Advances in Knowledge Discovery and Data Mining*, pages 786–798, 2017.

17. S. Jabbour, L. Sais, and Y. Salhi. A pigeon-hole based encoding of cardinality constraints. *TPLP*, 13(4-5-Online-Supplement), 2013.

18. S. Jabbour, L. Sais, and Y. Salhi. The top-k frequent closed itemset mining using top-k SAT problem. In *ECML/PKDD*, pages 403–418, 2013.

19. S. Jabbour, L. Sais, and Y. Salhi. Decomposition based SAT encodings for itemset mining problems. In *Pacific-Asia Conference on Advances in Knowledge Discovery and Data Mining*, pages 662–674, 2015.
20. S. Jabbour, L. Sais, and Y. Salhi. Mining top-k motifs with a SAT-based framework. *Artif. Intell.*, 244:30–47, 2017.

21. R. G. Jeroslow and J. Wang. Solving propositional satisfiability problems. *Annals of Mathematics and Artificial Intelligence*, 1:167–187, 1990.

22. N. Lazaar, Y. Lebbah, S. Loudni, M. Maamar, V. Lemière, C. Bessiere, and P. Boizumault. A global constraint for closed frequent pattern mining. In *International Conference on Principles and Practice of Constraint Programming*, pages 333–349, 2016.

23. Y. C. Lin, C. Wu, and V. S. Tseng. Mining high utility itemsets in big data. In *Pacific-Asia Conference on Advances in Knowledge Discovery and Data Mining*, pages 649–661, 2015.

24. L. Liu, E. Li, Y. Zhang, and Z. Tang. Optimization of frequent itemset mining on multiple-core processor. In *International Conference on Very Large Data Bases*, 2007.

25. S. Moens, E. Aksehirli, and B. Goethals. Frequent itemset mining for big data. In *IEEE International Conference on Big Data*, pages 111–118, 2013.

26. B. Négrevergne and T. Guns. Constraint-based sequence mining using constraint programming. In *International Conference on Integration of AI and OR Techniques in Constraint Programming*, pages 288–305, 2015.

27. B. Négrevergne, A. Termier, J. Méhaut, and T. Uno. Discovering closed frequent itemsets on multicore: Parallelizing computations and optimizing memory accesses. In *International Conference on High Performance Computing & Simulation*, pages 521–528, 2010.

28. L. D. Raedt, T. Guns, and S. Nijssen. Constraint programming for itemset mining. In *ACM SIGKDD*, pages 204–212, 2008.

29. A. Savasere, E. Omiecinski, and S. B. Navathe. An efficient algorithm for mining association rules in large databases. In *International Conference on Very Large Data Bases*, pages 432–444, 1995.

30. P. Schaus, J. O. R. Aoga, and T. Guns. Coversize: A global constraint for frequency-based itemset mining. In *International Conference on Principles and Practice of Constraint Programming*, pages 529–546, 2017.

31. T. Schubert, M. D. T. Lewis, and B. Becker. Pamiraxt: Parallel SAT solving with threads and message passing. *JSAT*, 6(4):203–222, 2009.

32. G. Tseitin. On the complexity of derivations in the propositional calculus. In *Studies in Mathematics and Mathematical Logic*, pages 115–125, 1968.

33. S. Wang, Y. Yang, Y. Gao, G. Chen, and Y. Zhang. Mapreduce-based closed frequent itemset mining with efficient redundancy filtering. In *IEEE International Conference on Data Mining Workshops*, ICDM, pages 449–453, 2012.

34. J. P. Warners. A linear-time transformation of linear inequalities into conjunctive normal form. *Information Processing Letters*, 68(2):63–69, 1998.

35. O. R. Zaïane, M. El-Hajj, and P. Lu. Fast parallel association rule mining without candidacy generation. In *IEEE International Conference on Data Mining*, pages 665–668, 2001.

36. M. J. Zaki. Mining non-redundant association rules. *Data Min. Knowl. Discov.*, 9(3):223–248, 2004.

37. H. ZHANG, M. P. BONACINA, and J. HSIANG. Psato: a distributed propositional prover and its application to quasigroup problems. *Journal of Symbolic Computation*, 21(4):543 – 560, 1996.

38. M. Zitouni, R. Akbarinia, S. B. Yahia, and F. Masseglia. Massively distributed environments and closed itemset mining: The DCIM approach. In *International Conference on Advanced Information Systems Engineering*, pages 231–246, 2017.