On the Average Number of Solutions for SAT Instances

Abstract

In this paper, we are interested in counting solutions for instances of satisfiability and more precisely we try to extend the formula for the average number of solutions of random instances proposed in [4] to a large class of instances. In fact the formula given in this reference works for the specific class of instances where all clauses are dependent. When we consider the independence characteristic of clauses, we find a more general mathematical expression. The computation of the average number of solutions with the actual formula depends only on the structure of independence of the instance. The latter is defined to be the set of subsets of independent clauses.
Searching the structure of independence for an instance is shown to be NP-hard. An algorithm in time O (nk2)  is designed for finding an approximate structure of an instance, k being the number of clauses and n the number of variables of the instance. Even though an approximate structure of independence is considered in the calculation of the average number of solutions, our formula yields results with more accuracy.