On the Impact of Junction-Tree Topology on Weighted Model Counting

We present and evaluate the power of a new framework for weighted model counting and inference in graphical models, based on exploiting the topology of the junction tree representing the formula. The proposed approach uses the junction tree topology in order to craft a reduced set of partial assignments that are guaranteed to decompose the formula. We show that taking advantage of the junction tree structure, along with existing optimization methods borrowed from the CNF-SAT domain, can translate into significant time savings for weighted model counting algorithms.