NSNet: A General Neural Probabilistic Framework for Satisfiability Problems

TL;DR

NSNet introduces a neural probabilistic framework that models satisfiability problems using graph neural networks inspired by belief propagation, enabling effective SAT solving and model counting with explainability.

Contribution

It proposes a novel GNN-based approach that unifies SAT and #SAT solving through probabilistic inference, with improved accuracy and efficiency.

Findings

Achieves competitive accuracy on SAT and #SAT datasets.

Provides a flexible framework for different satisfiability tasks.

Demonstrates explainability through probabilistic modeling.

Abstract

We present the Neural Satisfiability Network (NSNet), a general neural framework that models satisfiability problems as probabilistic inference and meanwhile exhibits proper explainability. Inspired by the Belief Propagation (BP), NSNet uses a novel graph neural network (GNN) to parameterize BP in the latent space, where its hidden representations maintain the same probabilistic interpretation as BP. NSNet can be flexibly configured to solve both SAT and #SAT problems by applying different learning objectives. For SAT, instead of directly predicting a satisfying assignment, NSNet performs marginal inference among all satisfying solutions, which we empirically find is more feasible for neural networks to learn. With the estimated marginals, a satisfying assignment can be efficiently generated by rounding and executing a stochastic local search. For #SAT, NSNet performs approximate model counting by learning the Bethe approximation of the partition function. Our evaluations show that NSNet achieves competitive results in terms of inference accuracy and time efficiency on multiple SAT and #SAT datasets.