Olivier Bailleux Counting by Statistics on Search Trees: Application to Constraint Satisfaction Problems

In 1975, D. Knuth proposed a simple statistical method for investigating search trees. We use this technique for estimating the number of solutions of CSP (Constraint Satisfaction Problem) and SAT (Boolean Satisfiability Problem) instances. We show that, depending on domain reductions, treebased estimates have a lower variance than estimates based on uniform sampling from the search space. Nevertheless, because the variance remains extremely high in the general case, a confidence interval cannot be derived but a lower bound of the number of solutions. These results are confirmed by many experiments. Keywords: Statistical counting, #P-Complete problems, Constraint satisfaction, Satisfiability.