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

In 1975, Knuth proposed a simple statistical method for investigating search trees. We use this technique for estimating the number of solutions of constraint satisfaction problem (CSP) and boolean satisfiability problem (SAT) instances. We show that, depending on domain reductions, tree-based 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.