Learning to Reason: Leveraging Neural Networks for Approximate DNF Counting

Propositional model counting (MC), or #SAT, is the task of counting the number of satisfying assignments for a given propositional formula [14]. Weighted model counting (WMC), or weighted #SAT, additionally incorporates a weight function over the set of all possible assignments. Offering an elegant formalism for encoding various probabilistic inference problems, WMC is a unifying approach for probabilistic inference. In particular, probabilistic graphical models [20], probabilistic planning [10], probabilistic logic programming [25], probabilistic databases [30] and probabilistic ontologies [2] can greatly benefit from advances in WMC. Two important special cases of WMC are weighted #CNF and weighted #DNF, where the former requires the input formula to be in CNF, and the latter to be in DNF. Both of these problems have a wide variety of applications. Inference in probabilistic graphical models typically reduces to solving weighted #CNF instances, while query evaluation in probabilistic databases reduces to solving weighted #DNF instances. The major bottleneck in WMC is its inherent computational complexity.