This paper considers "the problem of learning logical structure [...] as expressed by satisfiability problems". This is an attempt at incorporating symbolic AI into neural networks. The key contribution of the paper is the introduction of "a differentiable smoothed MAXSAT solver", that is able to learn logical relationships from examples. 

The example given in the paper is Sudoku. The proposed model is able to learn jointly the rules of the game and how to solve the puzzles, **without prior on the rules**.

The core of the system is a new layer that learns satisfiability constraints while being differentiable. This layer can be embedded in a typical ConvNet:
![satnet](https://user-images.githubusercontent.com/8659132/59875340-85ae7780-936e-11e9-946c-c8e8bcb2f869.png)

Previous attempts to solve Sudoku with a neural network were unsuccessful. The networks were able to reach a high accuracy on the training set but were completely unable to generalize on new puzzles, showing they were unable to learn the underlying logic. SATNet reaches 99% test accuracy on an encoded representation of Sudoku puzzles and 63% test accuracy on images of Sudoku puzzles. 

# Comments

This layer can probably be used to solve other puzzle games, but I'm not familiar enough with SAT to know what kind of practical problems can be solved with this system. Operational research problems maybe?

Code: https://github.com/locuslab/SATNet