MILP-SAT-GNN: Yet Another Neural SAT Solver

TL;DR

This paper introduces a novel GNN-based approach for solving SAT problems by transforming them into MILP problems, establishing theoretical properties, limitations, and approximation capabilities, with promising experimental results.

Contribution

It presents a new GNN method for SAT solving via MILP encoding, with theoretical invariance, limitations for certain formulae, and universal approximation guarantees.

Findings

Method achieves promising results on SAT problems.

Theoretical invariance under clause and variable reordering.

Limitations identified for foldable formulae.

Abstract

We proposes a novel method that enables Graph Neural Networks (GNNs) to solve SAT problems by leveraging a technique developed for applying GNNs to Mixed Integer Linear Programming (MILP). Specifically, k-CNF formulae are mapped into MILP problems, which are then encoded as weighted bipartite graphs and subsequently fed into a GNN for training and testing. From a theoretical perspective: (i) we establish permutation and equivalence invariance results, demonstrating that the method produces outputs that are stable under reordering of clauses and variables; (ii) we identify a theoretical limitation, showing that for a class of formulae called foldable formulae, standard GNNs cannot always distinguish satisfiable from unsatisfiable instances; (iii) we prove a universal approximation theorem, establishing that with Random Node Initialization (RNI), the method can approximate SAT solving to arbitrary precision on finite datasets, that is, the GNN becomes approximately sound and complete on such datasets. Furthermore, we show that for unfoldable formulae, the same approximation guarantee can be achieved without the need for RNI. Finally, we conduct an experimental evaluation of our approach, which show that, despite the simplicity of the neural architecture, the method achieves promising results.