Frequent Patterns Mining for the Satisfiability Problem

This paper presents a novel approach for solving the Satisfiability problem by reducing its complexity. First, an improved, ‘divide and conquer’version of the Apriori algorithm is introduced. It consists in dividing the problem instance into two or more if necessary, sub-instances and then in executing an ameliorated version of the Apriori algorithm for extracting the frequent variables appearing in the sub-instances. These most frequent variables are grouped into clusters and the corresponding problem are considered for resolution. Once done, the clusters can be shown as new smaller instances that are solvable separately using either the DPLL procedure or the BSO algorithm according to the number of variables to be solved.