Learning a SAT Solver from Single-Bit Supervision
Authors: Daniel Selsam, Matthew Lamm, Benedikt B\"{u}nz, Percy Liang, Leonardo de Moura, David L. Dill
ICLR 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present Neuro SAT, a message passing neural network that learns to solve SAT problems after only being trained as a classifier to predict satisfiability. Although it is not competitive with state-of-the-art SAT solvers, Neuro SAT can solve problems that are substantially larger and more difficult than it ever saw during training by simply running for more iterations. Moreover, Neuro SAT generalizes to novel distributions; after training only on random SAT problems, at test time it can solve SAT problems encoding graph coloring, clique detection, dominating set, and vertex cover problems, all on a range of distributions over small random graphs. |
| Researcher Affiliation | Collaboration | Daniel Selsam, Matthew Lamm, Benedikt B unz, Percy Liang, David L. Dill Department of Computer Science Stanford University Stanford, CA 94305 {dselsam,mlamm,buenz,pliang,dill}@cs.stanford.edu Leonardo de Moura Microsoft Research Redmond, WA 98052 leonardo@microsoft.com |
| Pseudocode | No | The paper describes the model formally with mathematical equations for updates: “A single iteration consists of applying the following two updates: (C(t+1), C(t+1) h ) Cu([C(t) h , M Lmsg(L(t))]) (L(t+1), L(t+1) h ) Lu([L(t) h , Flip(L(t)), MCmsg(C(t+1))])”. However, it does not provide pseudocode or a clearly labeled algorithm block. |
| Open Source Code | No | The paper does not contain any explicit statement about releasing source code, nor does it provide a link to a code repository or mention code in supplementary materials for the described methodology. |
| Open Datasets | No | The paper describes generating its own datasets: “Given a distribution Ψ over SAT problems, we can construct datasets Dtrain and Dtest with examples of the form (P, φ(P)) by sampling problems P Ψ and computing φ(P) using an existing SAT solver (we used Minisat Sorensson & Een (2005)).” and “To force our network to learn something substantive, we create a distribution SR(n) over pairs of random SAT problems on n variables with the following property: one element of the pair is satisfiable, the other is unsatisfiable, and the two differ by negating only a single literal occurrence in a single clause.” However, it does not provide access information (link, DOI, citation) to these datasets for public use. |
| Dataset Splits | No | The paper mentions “datasets Dtrain and Dtest” and that it trained on SR(U(10, 40)) and evaluated on SR(40). It does not explicitly describe a separate validation set or provide specific percentages or counts for training/test splits. For example, “Given a distribution Ψ over SAT problems, we can construct datasets Dtrain and Dtest with examples of the form (P, φ(P)) by sampling problems P Ψ and computing φ(P) using an existing SAT solver.” |
| Hardware Specification | No | The paper does not provide any specific details about the hardware used to run the experiments, such as GPU or CPU models, memory, or cloud computing specifications. |
| Software Dependencies | No | The paper mentions some software used: “we used Minisat Sorensson & Een (2005)” and “We trained our model using the ADAM optimizer (Kingma & Ba, 2014)”. However, it does not provide specific version numbers for Minisat, the ADAM optimizer, or any other libraries or frameworks used, which are necessary for reproducibility. |
| Experiment Setup | Yes | We instantiated the Neuro SAT architecture described in 3 with d = 128 dimensions for the literal embeddings, the clause embeddings, and all the hidden units; 3 hidden layers and a linear output layer for each of the MLPs Lmsg, Cmsg, and Lvote; and rectified linear units for all non-linearities. We regularized by the ℓ2 norm of the parameters scaled by 10 10, and performed T = 26 iterations of message passing on every problem. We trained our model using the ADAM optimizer (Kingma & Ba, 2014) with a learning rate of 2 10 5, clipping the gradients by global norm with clipping ratio 0.65 (Pascanu et al., 2012). We batched multiple problems together, with each batch containing up to 12,000 nodes (i.e. literals plus clauses). |