<span></span><p dir="ltr"><span><b>The Problem</b></span></p><p dir="ltr"><span>Model counting (</span><a href="http://www.cs.cornell.edu/~sabhar/chapters/ModelCounting-SAT-Handbook-prelim.pdf"><span>http://www.cs.cornell.edu/~sabhar/chapters/ModelCounting-SAT-Handbook-prelim.pdf</span></a><span>) generalizes boolean satisfiability. Instead of finding a single solution or showing that no solution exists, it counts the total number of solutions of a given boolean formula. Unsurprisingly, it is also a much harder problem, harder than NP-complete and in fact complete for the class #P. This has a number of interesting applications, including certain forms of probabilistic inference.</span></p><p dir="ltr"><span><b>The Interface</b></span></p><p dir="ltr"><span>A string representing the formula (see </span><a href="http://algorithmia.com/algorithms/cloncaric/sat"><span>http://algorithmia.com/algorithms/cloncaric/sat</span></a><span> for an example of how to do the encoding), as well as whatever parameters your routine requires. It should output the number of solutions found. Given the difficulty of the problem, you may want to include a timeout, at which the algorithm will just return the number of solutions found so far.</span></p><p dir="ltr"><span><b>The Algorithm</b></span></p><span>Most successful algorithms for model counting involve modified forms of boolean satisfiability algorithms like local search and DPLL (</span><a href="http://en.wikipedia.org/wiki/DPLL_algorithm"><span>http://en.wikipedia.org/wiki/DPLL_algorithm</span></a><span>). It may be possible to built this on top of a preexisting SAT solver (see http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Algorithms_for_solving_SAT).</span>