Complete Search Algorithms for Model Counting, Inference, and Optimization Problems

Although NP-complete problems including satisfiability testing (SAT) are traditionally thought as intractable, the efficiency of SAT solvers has been hugely improved over the past decade and a half, and modern SAT solvers are successfully used to solve many practical hard problems in hardware/software verification, planning, diagnosis, and other areas. Despite the popularity of SAT, #SAT, the problem of counting models of a formula, has been much less exploited. That is partly due to the #P hardness of model counting, which may remain hard even if SAT is in P. This thesis focuses on how to design a new sound, complete, and efficient #SAT algorithm, which is a novel integration of several major techniques including dynamic decomposition, component caching, clause learning, branching heuristics binary clause propagation and backtracking. Finally, it shows how to apply the resulting #SAT solver Cachet to (1) Bayesian inference via CNF encoding and weighted model counting, and (2) various optimization problems such as Most Probable Explanation (MPE), Maximum Satisfiability (MAX-SAT) and Maximum A Posteriori (MAP) by extending it with dynamic bounding. This thesis reports empirical results on a wide range of problem domains, compares our solver with other state-of-the-art solvers and concludes that our approach is often significantly better than or at least very competitive with others. The main contribution of this work is to present new efficient #SAT-based algorithms and show how they can be successfully applied to some hard AI problems that require exhaustive search.