Two phase clustering method for CNF clauses

Aimed at the Boolean clauses clustering, a two phases clustering method for CNF clauses is proposed. At the beginning, each clause is treated as a cluster. In the first phase, by a link based clustering method, the common neighbors between two clusters is used to determine how to merge the clusters. In the second phase, a similarity based clustering method is used. The first phase uses a global view to cluster the clauses, so the global optimum can be achieved in some sense. The second phase uses similarity to merge clusters, so the setting of the number of the final clusters in the algorithm is unnecessary. Experimental results show that the proposed method can lead to better clustering results with fewer common variables.