A new algorithm for counting and checking satisfiability and a restricted unfavorable region for polynomial average time

The satisfiability (SAT) problem plays an important role in areas like AI, VLSI, OR and graph theory. The author (1989) introduced a complementary approach other than backtracking for this problem. The algorithm called IS counts the number of solutions of an instance of SAT and then answers to the testing of satisfiability. The method of counting is inspired by the Karnaugh method for simplification of Boolean functions. The algorithm described in this paper consists in searching disjoint groups of solutions. The number of solutions is then obtained by summing up the numbers of solutions of disjoint groups. We can observe at least three advantages for our algorithm. The method used is conceptually simpler than most existing ones because it does not handle heavy data structure and easier to implement because it does not have to control phenomena such as the overlapping of clauses on cells of the Karnaugh map, which makes the difficulty in IS. The second important one is that the space complexity of the algorithm is linear. The third and more interesting one lies in the fact that it is faster when counting and checking for satisfiability. For the latter the counting halts when the first group of solutions is found