Distribution-Aware Sampling and Weighted Model Counting for SAT ∗ †

Given a CNF formula and a weight for each assign-ment of values to variables, two natural problems are weighted model counting and distribution-aware sam-pling of satisfying assignments. Both problems have a wide variety of important applications. Due to the inher-ent complexity of the exact versions of the problems, in-terest has focused on solving them approximately. Prior work in this area scaled only to small problems in prac-tice, or failed to provide strong theoretical guarantees, or employed a computationally-expensive most proba-ble explanation (MPE) oracle that assumes prior knowl-edge of a factored representation of the weight distri-bution. We present a novel approach that works with a black-box oracle for weights of assignments and re-quires only an NP-oracle (in practice, a SAT-solver) to solve both the counting and sampling problems. Our approach works under mild assumptions on the distri-bution of weights of satisfying assignments, provides strong theoretical guarantees, and scales to problems in-volving several thousand variables. We also show that the assumptions can be significantly relaxed while im-proving computational efficiency if a factored represen-tation of the weights is known.