locuslab/SATNet locuslab/SATNet

  • Stars
    star
    404
  • Rank 106,897 (Top 3 %)
  • Language
    Python
  • License
    MIT License
  • Created over 5 years ago
  • Updated almost 2 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
locuslab/SATNet
github

locuslab

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

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

The package also depends on the nvcc compiler. If it doesn't exist (try nvcc from commandline), you can install it via

conda install -c conda-forge cudatoolkit-dev

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

More Repositories

1

TCN

Sequence modeling benchmarks and temporal convolutional networks
Python
4,122
star
2

convmixer

Implementation of ConvMixer for "Patches Are All You Need? 🀷"
Python
1,059
star
3

mpc.pytorch

A fast and differentiable model predictive control (MPC) solver for PyTorch.
Python
865
star
4

deq

[NeurIPS'19] Deep Equilibrium Models
Python
719
star
5

qpth

A fast and differentiable QP solver for PyTorch.
Python
673
star
6

wanda

A simple and effective LLM pruning approach.
Python
602
star
7

optnet

OptNet: Differentiable Optimization as a Layer in Neural Networks
Python
507
star
8

trellisnet

[ICLR'19] Trellis Networks for Sequence Modeling
Python
473
star
9

fast_adversarial

[ICLR 2020] A repository for extremely fast adversarial training using FGSM
Python
422
star
10

convex_adversarial

A method for training neural networks that are provably robust to adversarial attacks.
Python
378
star
11

smoothing

Provable adversarial robustness at ImageNet scale
Python
357
star
12

pytorch_fft

PyTorch wrapper for FFTs
Python
313
star
13

lcp-physics

A differentiable LCP physics engine in PyTorch.
Python
292
star
14

icnn

Input Convex Neural Networks
Python
274
star
15

differentiable-mpc

Python
239
star
16

mdeq

[NeurIPS'20] Multiscale Deep Equilibrium Models
Python
232
star
17

e2e-model-learning

Task-based end-to-end model learning in stochastic optimization
Python
195
star
18

ect

Consistency Models Made Easy
Python
188
star
19

deq-flow

[CVPR 2022] Deep Equilibrium Optical Flow Estimation
Python
177
star
20

robust_overfitting

Python
153
star
21

DC3

DC3: A Learning Method for Optimization with Hard Constraints
Python
133
star
22

cfd-gcn

Python
113
star
23

massive-activations

Code accompanying the paper "Massive Activations in Large Language Models"
Python
95
star
24

tofu

Landing Page for TOFU
Python
86
star
25

FLYP

Code for Finetune like you pretrain: Improved finetuning of zero-shot vision models
Python
85
star
26

projected_sinkhorn

Python
85
star
27

torchdeq

Modern Fixed Point Systems using Pytorch
Python
74
star
28

perturbation_learning

Learning perturbation sets for robust machine learning
Python
64
star
29

scaling_laws_data_filtering

Python
59
star
30

lml

The Limited Multi-Label Projection Layer
Python
58
star
31

deq-ddim

Python
58
star
32

chatllm-vscode

TypeScript
58
star
33

edge-of-stability

Python
55
star
34

robust-nn-control

Enforcing robust control guarantees within neural network policies
Python
52
star
35

monotone_op_net

Monotone operator equilibrium networks
Jupyter Notebook
51
star
36

orthogonal-convolutions

Implementations of orthogonal and semi-orthogonal convolutions in the Fourier domain with applications to adversarial robustness
Jupyter Notebook
41
star
37

convmixer-cifar10

Simple CIFAR-10 classification with ConvMixer
Python
40
star
38

newton_admm

A Newton ADMM based solver for Cone programming.
Python
38
star
39

tta_conjugate

Test-Time Adaptation via Conjugate Pseudo-Labels
Python
36
star
40

T-MARS

Code for T-MARS data filtering
Python
34
star
41

stable_dynamics

Companion code to "Learning Stable Deep Dynamics Models" (Manek and Kolter, 2019)
Jupyter Notebook
31
star
42

ImpSq

Implicit^2: Implicit model for implicit neural representations
Python
27
star
43

robust_union

[ICML'20] Multi Steepest Descent (MSD) for robustness against the union of multiple perturbation models.
Python
25
star
44

breaking-poisoned-classifier

Code for paper "Poisoned classifiers are not only backdoored, they are fundamentally broken"
Jupyter Notebook
24
star
45

diffusion-model-hallucination

Python
24
star
46

acr-memorization

Python
24
star
47

gradient_regularized_gan

Code for "Gradient descent GAN optimization is locally stable"
Python
21
star
48

get

Generative Equilibrium Transformer
Python
17
star
49

smoothinv

Single Image Backdoor Inversion via Robust Smoothed Classifiers
Python
16
star
50

intermediate_robustness

Python
16
star
51

mixing

The Mixing method: coordinate descent for low-rank semidefinite programming
C
15
star
52

dreaml

dreaml: dynamic reactive machine learning
JavaScript
12
star
53

ase

Analogous Safe-state Exploration (ASE) is an algorithm for provably safe and optimal exploration in MDPs with unknown, stochastic dynamics.
Python
11
star
54

sdp_clustering

Jupyter Notebook
11
star
55

JIIO-DEQ

Efficient joint input optimization and inference with DEQ
Python
10
star
56

uniform-convergence-NeurIPS19

The code for the NeurIPS19 paper and blog on "Uniform convergence may be unable to explain generalization in deep learning".
Jupyter Notebook
10
star
57

sdp_mrf

Jupyter Notebook
3
star
58

mixsat

Low-rank semidefinite programming for the MAX2SAT problem
C
3
star
59

MonotoneDBM

Python
2
star
60

lipschitz_mondeq

Jupyter Notebook
1
star
61

mugrade

Python
1
star