|Previous||[1 ]||[2 ]||||||||||7|||
LAFORIA, Universite Paris VI,
4 place Jussieu, 75252 Paris Cedex 05, France
The originality of this work is the use of statistical tests in enumerating the solutions of SAT instances in probability in order to avoid the combinatory combinatory explosion caused by the complexity of the problem. Basically, statistical tests are common tools in the behavioral sciences to explore data analysis or to verify hypotheses derived from theories of behavior.
In our study of the satisfiabillity problem (SAT for short), We consider exploratory and confirmatory statistical tests to suggest possible theoretical probabillity laws for a sample of a number of solutions of 200 SAT instances. This latter is luilt up by geneerating random SAT instances and calculating their respective numbers of solutions.
Among the goodness-of-fit nonparametric statistical tests, the Kolmogorov-Smirnov distribution test has been chosen because its efficiency is highest. It has yielded a very interesting result: among an important set of theoretical probability laws tested, only the normal distribution is not rejected for some data depending on their parameters, namely the number of variables and the number of clauses in the data.
In addition, in Section 5 we suggest a design for an acceptance region depending on the parameters of SAT data for which the number of solutions follows the normal probability distribution based on the statistical analysis in the previous parts of the paper. For other kinds of data, a naive discussion of the probaility laws of the numbers of solutions is provided.
Keywords: computational complexity, counting problems, satisfifability problem, probability laws, kolmogorov-smirnor statistical test
Received April 5, 1992; revised October 15, 1992.
Communicated by Y. S. Kuo.