Counting the number of solutions for instances of satisfiability (Q2277848): Difference between revisions

We attempt to count the number of solutions of SAT instances by combinatorial formulas. For this a notion of independence between clauses is introduced. A formula for computing the number of solutions of independent clauses in linear time is given. We establish a formula for computing the number of solutions of a set of any clauses. Transformation of a set of any clauses into an equivalent set of independent clauses is proposed. The transformation allows all solutions of a SAT instance to be determined with a time complexity less than \(L2^ n\) (L being the length of the instance), i.e. \(O(kr_{\max}2^{r_{\max}}\alpha^ n_{r_{\max}})\), n being the numbers of variables, k the number of clauses and \(r_{\max}\) the maximum length of clauses (for example for 3-SAT \(\alpha_ 3\approx 1.84)\). Finally, experimental results are provided for variations of number of solutions by number of clauses for random 2-SAT and 3-SAT instances. These experimental results are in agreement with the theoretical results established in \textit{O. Dubois} and \textit{J. Carlier} [Probabilistic approach to the satisfiability problem, Theor. Comput. Sci. 81, 65-76 (1991)] concerning the mathematical expectation of the number of solutions.