SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver
Authors: Po-Wei Wang, Priya Donti, Bryan Wilder, Zico Kolter
ICML 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We test our MAXSAT layer approach in three domains that are traditionally difficult for neural networks: learning the parity function with single-bit supervision, learning 9 9 Sudoku solely from examples, and solving a visual Sudoku problem that generates the logical Sudoku solution given an input image of a Sudoku puzzle. |
| Researcher Affiliation | Collaboration | 1School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA 2Department of Engineering & Public Policy, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA 3Department of Computer Science, University of Southern California, Los Angeles, California, USA 4Bosch Center for Artificial Intelligence, Pittsburgh, Pennsylvania, USA. |
| Pseudocode | Yes | Algorithm 1 SATNet Layer, Algorithm 2 Forward pass coordinate descent, Algorithm 3 Backward pass coordinate descent |
| Open Source Code | Yes | Source code for our implementation is available at https://github.com/locuslab/SATNet. |
| Open Datasets | No | For each sequence length, we generate a dataset of 10K random examples (9K training and 1K testing). The paper mentions using MNIST digits for Visual Sudoku, but the constructed Sudoku puzzles are not made available. No specific links, DOIs, or citations are provided for the generated datasets used in their experiments. |
| Dataset Splits | No | For each sequence length, we generate a dataset of 10K random examples (9K training and 1K testing). The paper only mentions training and testing splits, not a separate validation split. |
| Hardware Specification | Yes | 95.0% test accuracy in 22 epochs/37 minutes on a GTX 1080 Ti GPU |
| Software Dependencies | No | The paper mentions using 'Adam optimizer' and 'GPU CUDA-C implementation' but does not specify any version numbers for these or other relevant software dependencies such as deep learning frameworks or libraries. |
| Experiment Setup | Yes | We train our model using cross-entropy loss and the Adam optimizer (Kingma & Ba, 2015) with a learning rate of 10 1. Our model architecture consists of a single SATNet layer with 300 auxiliary variables and low rank structure m = 600, and we train it to minimize a digitwise negative log likelihood objective (optimized via Adam with a 2 10 3 learning rate). For the visual Sudoku problem, learning rates 2 10 3 for the SATNet layer and 10 5 for the convolutional layer. |