A Divide and Conquer Approach to All Solutions Satisfiability Problem

SAT, is one of the fundamental topics in computer science, which has a long history in AI. As a variant of SAT, the all solutions satisfiability problem(AllSAT) is widely used in the field of electronic design automation. It is to generate all or part solutions of a given SAT instance. The computational complexity of AllSAT is higher than general SAT, which leads to less research related and poor performance of existing AllSAT solvers. In this paper, we propose to solve AllSAT by a divide-and-conquer-based approach called DIV2, which solve more instances within the time limit. Besides, we present a segmentation strategy for DIV2, called Jaccard similarity segmentation, which improves the efficiency of DIV2. The experimental result shows that the method proposed in this paper, has a better performance than the state-of-the-art algorithms, with regarding to the number of instances solved and the total number of solutions found for SAT 2014 competition benchmark.