Graph Neural Networks for Propositional Model Counting
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 Kuch et al., extended with self-attentive GNN and trained to approximately solve the #SAT problem. We ran a thorough experimental investigation, showing that our model, trained on a small set of random Boolean formulae, is able to scale effectively to much larger problem sizes, with comparable or better performances of 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 SAT-encoded combinatorial problems.
Code (0)
등록된 구현이 없습니다.
Tasks
Logical ReasoningmodelSimilar Papers 제목 키워드 기반
Hypergraph Acyclicity and Propositional Model Counting
We show that the propositional model counting problem #SAT for CNF- formulas with hypergraphs that allow a disjoint branches decomposition can be solved in polynomial time. We show that this class of hypergraphs is incom…
modelPre and Post Counting for Scalable Statistical-Relational Model Discovery
Statistical-Relational Model Discovery aims to find statistically relevant patterns in relational data. For example, a relational dependency pattern may stipulate that a user's gender is associated with the gender of the…
Model DiscoveryRelational ReasoningStable Model Counting and Its Application in Probabilistic Logic Programming
Model counting is the problem of computing the number of models that satisfy a given propositional theory. It has recently been applied to solving inference tasks in probabilistic logic programming, where the goal is to …
Complexity of Faceted Explanations in Propositional Abduction
Abductive reasoning is a popular non-monotonic paradigm that aims to explain observed symptoms and manifestations. It has many applications, such as diagnosis and planning in artificial intelligence and database updates.…
Top-Down Knowledge Compilation for Counting Modulo Theories
Propositional model counting (#SAT) can be solved efficiently when the input formula is in deterministic decomposable negation normal form (d-DNNF). Translating an arbitrary formula into a representation that allows infe…
Negation