  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.
