Graph Neural Networks for Propositional Model Counting
Gaia Saveri · 2022
Graph Neural Networks (GNNs) have been recently leveraged to solve several logical reasoning tasks.Nevertheless, counting problems such as propositional model counting (#SAT) are still mostly approached with traditional solvers.Here we tackle this gap by presenting an architecture based on the GNN framework for belief propagation (BP) of [1], extended with self-attentive GNN and trained to approximately solve the #SAT problem.We experimentally show that our model, trained on a small set of random Boolean formulae, is able to scale effectively to much larger problem sizes, outperforming state of the art approximate solvers.Moreover, we show that it can be efficiently fine-tuned to provide good generalization results on different formulae distributions, such as those coming from SATencoded combinatorial problems.