Complementary Branching for #SAT: Bounded-Degree Bounds and Faster #3-SAT

摘要

We present complementary branching, a new branching approach for model counting based on the complement counting paradigm. Instead of branching on individual variables, complementary branching decomposes the counting problem for arbitrary CNF formulas into several subformulas, which naturally augments the classic DPLL branching. We show two novel results in which the main tool is complementary branching. First, we design new #SAT algorithms for sparse CNF formulas running in time O*(2^(alpha n)), for some constant alpha < 1. As a second application, we improve the best known deterministic upper bound for #3-SAT to O*(1.637^n) by using a version of clause learning based on complementary branching. These results demonstrate that complementary branching is a powerful tool for designing faster exact algorithms for propositional model counting.