G2SAT: Learning to Generate SAT Formulas
Authors: Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, Jure Leskovec
NeurIPS 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments demonstrate that G2SAT is able to generate formulas that closely resemble the input real-world SAT instances in many graph-theoretic properties such as modularity and the presence of scale-free structures, with 24% lower relative error compared to state-of-the-art methods. We use 10 small real-world SAT formulas from the SATLIB benchmark library [21] and past SAT competitions. |
| Researcher Affiliation | Academia | Jiaxuan You1 jiaxuan@cs.stanford.edu Haoze Wu1 haozewu@stanford.edu Clark Barrett1 barrett@cs.stanford.edu Raghuram Ramanujan2 raramanujan@davidson.edu Jure Leskovec1 jure@cs.stanford.edu 1Department of Computer Science, Stanford University 2Department of Mathematics and Computer Science, Davidson College |
| Pseudocode | Yes | Algorithm 1 G2SAT at training time; Algorithm 2 G2SAT at inference time |
| Open Source Code | Yes | Link to code and datasets: http://snap.stanford.edu/g2sat/ |
| Open Datasets | Yes | We use 10 small real-world SAT formulas from the SATLIB benchmark library [21] and past SAT competitions.1 The two data sources contain SAT formulas generated from a variety of application domains, such as bounded model checking, planning, and cryptography. (Footnote 1 provides http://www.satcompetition.org/) |
| Dataset Splits | No | We use the Adam optimizer [25] with a learning rate of 0.001 to train the model until the validation accuracy plateaus. (No specific split percentages or counts are provided for training, validation, or test sets). |
| Hardware Specification | No | The largest graph we have generated has 39,578 nodes and 102,927 edges, which only took 489 seconds (data-processing time excluded) on a single GPU. (No specific GPU model, CPU, or other hardware details are provided). |
| Software Dependencies | No | We implement G2SAT with a 3-layer Graph SAGE model using mean pooling and Re LU activation [18] with hidden and output embedding size of 32. We use the Adam optimizer [25] with a learning rate of 0.001 to train the model until the validation accuracy plateaus. (No specific version numbers for Graph SAGE, Adam, or the underlying deep learning framework are provided). |
| Experiment Setup | Yes | We implement G2SAT with a 3-layer Graph SAGE model using mean pooling and Re LU activation [18] with hidden and output embedding size of 32. We use the Adam optimizer [25] with a learning rate of 0.001 to train the model until the validation accuracy plateaus. We conduct a grid search over two of its hyperparameters the variable decay vd, that influences the ordering of the variables in the search tree, and the clause decay cd, that influences which learned clauses are to be removed [12]. We sweep over the set {0.75, 0.85, 0.95} for vd, and the set {0.7, 0.8, 0.9, 0.99, 0.999} for cd. |