NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan,, Risto Miikkulainen
TL;DR
NeuroBack enhances CDCL SAT solvers by using a graph neural network to predict variable phases with a single offline inference, improving problem-solving success rates while eliminating GPU dependency.
Contribution
This paper introduces NeuroBack, a practical GNN-based method that predicts variable phases offline, enabling CPU-only execution and improved SAT solver performance.
Findings
NeuroBack solved up to 7.4% more problems in SAT competitions.
It requires only one offline GNN inference before solving.
NeuroBack operates efficiently on CPU without GPU resources.
Abstract
Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model…
Peer Reviews
Decision·ICLR 2024 poster
Using ML to enhance CDCL SAT solver is promising research, which is more likely to yield improvement in SAT solving than end-to-end learning on SAT. I like the idea in this paper of using ML to give an initial assignment for the CDCL solvers by training on predicting the value of backdoor variables. The paper mentions the importance of backdoor valuables and the intuition of why training on backdoor variables can help predict the values for all variables that appear in the majority of the variab
While training on backdoor variables yields a good predictor for the value of all variables, why this approach works is still a bit mysterious. It would be helpful to have more experiments showing that initialization is actually better than a random assignment. Therefore I would like to see some behavior studies of NeuroBack on different kinds of benchmarks. Possible ways include comparing the distance from this initial assignment given by NeuroBack with the nearest solution. Or evaluating the p
- The paper is clearly written and easy to follow. Normally, papers on applying ML for improving combinatorial problem solving are written in Greek, if seen from the perspective of a researcher with expertise in the combinatorial problem of interest. This paper serves as a nice exception. - The idea is reasonable. It is simple to implement and it can be used with any SAT solver. - The experimental results reported although not amazing look solid.
- Although everything the paper describes is described well, there are bits that aren't detailed sufficiently - some ML people may find it to be a minus. - The paper says nothing about the usability of this heuristic for unsatisfiable instances. There are no backbones in those but I presume some variable phases may still be more useful in practice than the others. - Despite the claimed experimental results, nothing is shown for the unsatisfiable instances. This and the point above
Providing a dataset Competing with SAT 2022
I think some citations are missing https://cs.stanford.edu/~jure/pubs/g2sat-neurips19.pdf Neurogift: Using a machine learning-based sat solver for cryptanalysis Role of Machine Learning for Solving Satisfiability Problems and its Applications in Cryptanalysis It would be nice to have a use case in Cryptanalysis (solving AES or small AES instance)
Code & Models
Videos
Taxonomy
TopicsBayesian Modeling and Causal Inference · Advanced Graph Neural Networks · Logic, Reasoning, and Knowledge