SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver

By Po-Wei Wang, Priya Lekha Donti, Bryan Wilder, Zico Kolter. 2019

319 citations recorded by the source corpus.

Integrating logical reasoning within deep learning architectures has been a major goal of modern AI systems. In this paper, we propose a new direction toward this goal by introducing a differentiable (smoothed) maximum satisfiability (MAXSAT) solver that can be integrated into the loop of larger deep learning systems. Our (approximate) solver is based upon a fast coordinate descent approach to solving the semidefinite program (SDP) associated with the MAXSAT problem. We show how to analytically differentiate through the solution to this SDP and efficiently solve the associated backward pass. We demonstrate that by integrating this solver 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) and learn how to play 9x9 Sudoku solely from examples. We also solve a "visual Sudok" problem that maps images of Sudoku puzzles to their associated logical solutions by combining our MAXSAT solver with a traditional convolutional architecture. Our approach thus shows promise in integrating logical structures within deep learning.

Subfields: Electrical and Electronic Engineering, Management Science and Operations Research, Numerical Analysis

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Electrical and Electronic Engineering

In Management Science and Operations Research

In Numerical Analysis

Citations in the corpus

Implicit Behavioral Cloning (2021, background): “Many other works have investigated using the notion of implicit functions in learning, including works that investigate implicit layers [39, 40, 41, 42, 43].”
Deep Equilibrium Models (2019, background): “There has been a growing interest in implicit layers in recent years [37, 3, 37, 50], but the precise formulation of the DEQ is quite different, and our current models represent the largest-scale practical application of implicit layers in deep learning of which we are aware.”
Sub-Task Decomposition Enables Learning in Sequence to Sequence Tasks (2022, methodology): “…original input is maximized conditioned on the input, and at test time only the original input is given to the model. shown, e.g. , Chang et al. (2020) showed that SATNet (Wang et al., 2019) could not solve visual Sudoku without using intermediate labels to identify individual Sudoku digit images.”
Deep Declarative Networks (2019, background): “However, many other interesting nodes will require specialized solvers for their forward functions (e.g., the coordinate-based SDP solver proposed by Wang et al. [47]).”
Combinatorial optimization and reasoning with graph neural networks (2021, background): “Although promising ways to tackle the issue of gradient estimation have already emerged in the literature [Knöbelreiter et al., 2017; Wang et al., 2019; Vlastelica et al., 2020; Mandi and Guns, 2020], another critical issue to consider is data efficiency.”
SenticNet 6: Ensemble Application of Symbolic and Subsymbolic AI for Sentiment Analysis (2020, background): “Integrating logical reasoning within deep learning architectures has been a major goal of modern AI systems [19, 61, 65].”
Implicit Deep Learning (2019, background): “For example, [20] show promise in integrating logical structures into deep learning by incorporating a semidefinite programming (SDP) layer into a network in order to solve a (relaxed) MAXSAT problem.”
On the Paradox of Learning to Reason from Data (2022, methodology): “For examples, SAT (Selsam et al., 2019), maxSAT (Wang et al., 2019), temporal logical problems (Hahn et al., 2021), DNF counting (Crouse et al., 2019), logical reasoning by learning the embedding of logical formula (Crouse et al., 2019; Abdelaziz et al., 2020) and mathematical problems (Saxton et…”
Neural Learning of One-of-Many Solutions for Combinatorial Problems in Structured Output Spaces (2020, methodology): “Sudoku: We also experiment on Sudoku, which has been used as the task of choice for many recent neural reasoning works [Palm et al., 2018, Wang et al., 2019].”
Differentiation of Blackbox Combinatorial Solvers (2019, background): “Another approach is to provide neural network building blocks that are specialized to solve some types of combinatorial problems such as satisfiability (SAT) instances [51].”
Neurosymbolic Programming (2021, methodology): “programs, and neural models for combinatorial tasks such as MAX-SAT solving (Wang et al., 2019).”