Skip to content
Bridging deep learning and logical reasoning using a differentiable satisfiability solver.
Branch: master
Clone or download
Latest commit e452a19 May 30, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
docker Initial commit May 21, 2019
exps Add options for adam and SGD May 22, 2019
images Commit initial README.md May 22, 2019
notebooks Adding details to README and Sudoku notebook May 26, 2019
satnet Initial commit May 21, 2019
src Initial commit May 21, 2019
LICENSE Initial commit May 21, 2019
README.md Update colab tag link May 29, 2019
requirements.txt Initial commit May 21, 2019
setup.py Update colab link May 27, 2019

README.md

SATNet • PyPi colab License

Bridging deep learning and logical reasoning using a differentiable satisfiability solver.

This repository contains the source code to reproduce the experiments in the ICML 2019 paper SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver by Po-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter.

What is SATNet

SATNet is a differentiable (smoothed) maximum satisfiability (MAXSAT) solver that can be integrated into the loop of larger deep learning systems. This (approximate) solver is based upon a fast coordinate descent approach to solving the semidefinite program (SDP) associated with the MAXSAT problem.

How SATNet works

A SATNet layer takes as input the discrete or probabilistic assignments of known MAXSAT variables, and outputs guesses for the assignments of unknown variables via a MAXSAT SDP relaxation with weights S. A schematic depicting the forward pass of this layer is shown below. To obtain the backward pass, we analytically differentiate through the SDP relaxation (see the paper for more details).

Forward pass

Overview of experiments

We show that by integrating SATNet into end-to-end learning systems, we can learn the logical structure of challenging problems in a minimally supervised fashion. In particular, we show that we can:

  • Learn the parity function using single-bit supervision (a traditionally hard task for deep networks)
  • Learn how to play 9×9 Sudoku (original and permuted) solely from examples.
  • Solve a "visual Sudoku" problem that maps images of Sudoku puzzles to their associated logical solutions. (A sample "visual Sudoku" input is shown below.)

Installation

Via pip

pip install satnet

From source

git clone https://github.com/locuslab/SATNet
cd SATNet && python setup.py install

Package Dependencies

conda install -c pytorch tqdm

Via Docker image

cd docker
sh ./build.sh
sh ./run.sh

Running experiments

Jupyter Notebook and Google Colab

Jupyter notebook and Google Colab

Run them manually

Getting the datasets

The Sudoku dataset and Parity dataset can be downloaded via

wget -cq powei.tw/sudoku.zip && unzip -qq sudoku.zip
wget -cq powei.tw/parity.zip && unzip -qq parity.zip

Sudoku experiments (original, permuted, and visual)

python exps/sudoku.py
python exps/sudoku.py --perm
python exps/sudoku.py --mnist --batchSz=50

Parity experiments

python exps/parity.py --seq=20
python exps/parity.py --seq=40
You can’t perform that action at this time.