Source-linked AI summary
SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver
Po-Wei Wang, Priya L. Donti, Bryan Wilder, Zico Kolter
TL;DR
Deep networks have struggled to learn discrete logical structure without hand-specified relationships. SATNet introduces a differentiable smoothed MAXSAT layer based on an SDP relaxation and coordinate descent, enabling end-to-end learning across parity, Sudoku, and visual Sudoku. The paper reports successful learning of these logical tasks, including 98.3% test accuracy on 9 × 9 Sudoku and 63.2% correct visual Sudoku boards.
Problem
Deep-learning methods struggle with hard, global discrete constraints, while prior differentiable systems generally use preexisting logical relationships rather than discovering them end to end.
Method
SATNet embeds a differentiable smoothed MAXSAT solver based on coordinate descent for an SDP relaxation, with analytical differentiation through the SDP solution.
Results
SATNet learns parity from single-bit supervision, solves 98.3% of 9 × 9 Sudoku puzzles, and correctly solves 63.2% of visual Sudoku boards at test time.
Takeaways & Limitations
The results show promise for integrating logical structure into deep networks and learning relationships without hard-coding them.
Takeaways & Limitations
SATNet requires the user to specify a maximum number of clauses m, and low-rank structure is often desirable to prevent overfitting and improve generalization.
Abstract
from arXiv · showhide
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.
1. Introduction
SATNet addresses the difficulty of learning hard, global logical constraints by embedding a differentiable smoothed MAXSAT solver into deep architectures. The resulting systems learn logical structure end to end, including parity, Sudoku, and visual Sudoku tasks.
- State-of-the-art deep learning methods struggle with hard and global constraints arising from discrete logical relationships.
- SATNet develops a differentiable smoothed MAXSAT solver that can be embedded in larger deep architectures without hard-coding logical relationships.The solver uses an SDP relaxation, block coordinate descent, and an efficient differentiable backward pass.
- SATNet learns parity from single-bit supervision, addressing a task known to be challenging for deep classifiers.
- SATNet learns the rules and solutions of 9 × 9 Sudoku, correctly solving 98.3% of test puzzles without hand-coded problem structure.
- The method combines a convolutional network for digit recognition with the differentiable MAXSAT solver to solve visual Sudoku end to end.
2. Related work
Prior work introduced differentiable reasoning and optimization modules, but generally relied on known logical relationships or narrower problem classes. SATNet combines differentiable optimization with an SDP relaxation of MAXSAT to target broader discrete-logic domains.
- SATNet combines logical reasoning and optimization-layer research through an SDP relaxation of MAXSAT.
- Deep-learning systems commonly make known logical relationships differentiable so networks can learn their parameters.
- Some systems jointly learn rules and parameters, but their captured problem classes remain limited compared with domains reducible to MAXSAT.
- Differentiable optimization research has addressed quadratic programs, submodular optimization, and equilibrium computation in zero-sum games.
- SATNet is presented as the first work to use differentiable SDP relaxations to capture relationships between discrete variables.
- Prior MAXSAT research established SDP relaxations and developed low-rank SDP solvers, which SATNet builds upon for differentiable reasoning.
3. A differentiable satisfiability solver
SATNet embeds a differentiable, smoothed MAXSAT solver into neural networks by relaxing satisfiability as an SDP, solving it with coordinate descent, and differentiating through the solution. The layer transforms known assignments into guesses for unknown variables and supports end-to-end learning with low-rank structure and auxiliary variables.
- Solver formulation and differentiation: The solver uses a fast coordinate descent approach for an SDP relaxation of MAXSAT and analytically computes gradients through the SDP solution.The backward pass directly computes gradients with respect to layer inputs and weights rather than explicitly unrolling forward computations.
- Solver formulation and differentiation: MAXSAT maximizes satisfied clauses, while the relaxation replaces binary assignments with continuous unit vectors relative to a truth direction.The continuous formulation can be rewritten as an SDP and recovered by sufficiently large rank.
- SATNet layer: SATNet accepts binary or probabilistic assignments for known variables and uses the SDP to infer binary or probabilistic assignments for unknown variables.Known inputs are relaxed into random unit vectors; coordinate descent updates are applied only to output variables before rounding or probability computation.
- Layer design choices: Low-rank structure can reduce overfitting, while auxiliary variables increase representational ability by reducing the clauses needed in conjunctive normal form.The minimum rank parameter k = 2n + 1 recovers the optimal solution of the associated SDP, where n includes auxiliary variables.
- SATNet layer: The forward pass maintains a matrix term for efficient rank-one updates, with per-iteration runtime O(nmk) and typically few iterations required for convergence.The algorithm initializes output vectors, updates them through coordinate descent, and returns the final output relaxation.
- Output generation: SATNet converts continuous outputs through thresholding or randomized rounding, while training uses the rounding probability as a differentiable output.At test time, repeated randomized rounding can select the Boolean solution maximizing the MAXSAT objective.
4. Experiments
The experiments evaluate SATNet on parity, traditional Sudoku, and visual Sudoku, showing that differentiable MAXSAT can learn logical structure under limited supervision and integrate with convolutional processing.
- 4.1. Learning parity (chained XOR): The parity model chains L − 1 SATNet layers with tied weights, passing each rounded output to the next layer to compose XOR operations.The layers must coordinate a long sequence of SAT problems without intermediate supervision.
- 4.1. Learning parity (chained XOR): SATNet learns parity for sequences of length L = 20 and L = 40 from single-bit supervision, while an LSTM struggles.SATNet’s held-out error converges to zero within 20 epochs; the LSTM reaches testing error at best 0.476 across both lengths.
- 4.2. Sudoku (original and permuted): On traditional 9 × 9 Sudoku, SATNet reaches 95.0% test accuracy after 22 epochs and 98.3% board-wise accuracy after 100 epochs.The model uses one SATNet layer with auxiliary variables and low-rank structure, whereas the comparison networks use convolutional architectures.
- 4.2. Sudoku (original and permuted): The ConvNet reaches 72.6% training accuracy but at most 0.04% held-out accuracy, while ConvNetMask reaches 15.1% held-out accuracy.These baselines therefore generalize substantially less effectively than SATNet on the reported Sudoku task.
- 4.3. Visual Sudoku: SATNet correctly solves 63.2% of visual Sudoku boards after 100 epochs, reaching 85% of the theoretical 74.7% best accuracy.The baseline convolutional networks fail to improve out-of-sample performance over the same training period.
5. Conclusion
The paper presents a low-rank differentiable MAXSAT layer that supports efficient neural integration and learns logical structures without hard-coded variable relationships. Results on parity, 9 × 9 Sudoku, and visual Sudoku support its promise for combining logical reasoning with deep learning.
- 5. Conclusion: SATNet uses a low-rank differentiable MAXSAT layer with block coordinate descent for efficient forward and backward passes, including GPU acceleration.The layer is designed for integration into neural network architectures.
- 5. Conclusion: The architecture learns parity and 9 × 9 Sudoku structure, and integrates with larger networks for end-to-end visual Sudoku training.These results address logical learning without hard-coding relationships between variables.
- 5. Conclusion: The work targets a gap between deep learning and logical reasoning by reducing reliance on hand-specified logical rules and groundings.The authors frame MAXSAT as a generic differentiable primitive for more end-to-end systems.
A. Derivation of the forward pass coordinate descent update
The forward pass rewrites the MAXSAT SDP objective into coordinate-wise terms and updates each unit vector by minimizing its local expression under a unit-norm constraint.
- A. Derivation of the forward pass coordinate descent update: The formulation represents S as an m × (n + 1) matrix and v_i as the i-th column vector of V.These quantities parameterize the low-rank SDP factorization used by the solver.
- A. Derivation of the forward pass coordinate descent update: The SDP objective is rewritten using trace identities so the terms depending on a given v_i can be isolated.The derivation uses symmetry of S^T S and cyclic permutation inside the trace.
- A. Derivation of the forward pass coordinate descent update: The term v_i^T v_i cancels to 1, leaving a coefficient that is constant with respect to v_i.This simplifies the coordinate-wise optimization problem.
- A. Derivation of the forward pass coordinate descent update: Minimizing the simplified expression over v_i subject to ||v_i|| = 1 yields the block coordinate descent update.The update is the forward-pass rule used to optimize the low-rank SDP formulation.
B. Details on backpropagation through the MAXSAT SDP
Backpropagation differentiates through the coordinate descent fixed point by taking total differentials, rewriting them as an implicit linear system, and extracting gradients through matrix operations.
- B. Details on backpropagation through the MAXSAT SDP: The backward pass takes total differentials of the coordinate descent updates at the optimal fixed-point solution.This provides the route for propagating gradients through the SDP solution procedure.
- B. Details on backpropagation through the MAXSAT SDP: The differentials are rewritten over all output variables as a linear system involving the coordinate-descent quantities.The construction includes OSO, diag(||s_o||^2), and P = diag(P_o).
- B. Details on backpropagation through the MAXSAT SDP: The chain rule converts the resulting implicit form into gradients with respect to V_I and S.The matrix U is defined with zero columns for I and coordinate-descent-derived columns U_O for O.
- B. Details on backpropagation through the MAXSAT SDP: Individual gradients can be computed by setting one differential component to 1 and all others to zero, then assembling the results in matrix form.For ∂ℓ/∂v_i, the procedure sets dv_i = 1 while the remaining gradients vanish.
C. Proof of pseudoinverse computations
The appendix derives pseudoinverse relationships used to obtain the implicit total differential for vec(dVO).
- Lemma C.1 identifies a quantity as the solution of a linear system.
- Examining the equation with respect to dvi shows that each dvi can be written as Piyi for some yi.
- Substitution and projector identities yield the solution for dVO after setting vec(dVO) = P vec(Y).
D. Derivation of the backward pass coordinate descent algorithm
The backward pass solves for UO using block coordinate descent, with closed-form variable updates and projection invariance maintained after each update.
- The backward-pass computation for UO is formulated as a linear system.
- Block coordinate descent isolates the uo variable and exploits the initialization UO = 0 to assume P vec(Uo) = vec(Uo).
- Defining −dgi from the equation's right-hand-side terms gives a closed-form feasible update for uo.
- After updating uo, a rank 1 update maintains the auxiliary term Ψ.
- Algorithm 3 summarizes the procedure, and projection by Po preserves P vec(UO) = vec(UO) after each update.
E. Results for the 4 × 4 Sudoku problem
On 4 × 4 Sudoku, SATNet converges rapidly to perfect board-wise test accuracy and outperforms conventional convolutional baselines, while matching OptNet performance more efficiently.
- 100% board-wise test accuracy is reached by SATNet in just two epochs across 9K training and 1K testing examples.
- 12 minutes versus 2 minutes for 20 epochs on a GTX 1080 Ti: SATNet runs substantially faster than OptNet.
- 3-4 epochs versus 1 epoch: OptNet takes longer to converge than SATNet to similar performance.
- 93% accuracy: the traditional ConvNet overfits and generalizes worse than SATNet and OptNet.
- 99% test accuracy: ConvNetMask improves over ConvNet but remains below the perfect performance of SATNet and OptNet.
F. Convergence plots for 9 × 9 Sudoku experiments
For 9 × 9 logical and visual Sudoku, SATNet generalizes better than convolutional baselines, although visual whole-board accuracy is limited by the end-to-end MNIST classifier.
- 9 × 9 Sudoku: SATNet performs nearly identically on original and permuted 9 × 9 Sudoku and generalizes well at every epoch without overfitting.
- 9 × 9 Sudoku: ConvNet and ConvNetMask overfit in the original setting, while both make little progress on permuted inputs lacking usable spatial locality.
- Visual Sudoku: SATNet generalizes well in loss throughout visual Sudoku training and somewhat well in whole-board accuracy.
- Visual Sudoku: The visual-versus-logical Sudoku generalization gap is attributed to the end-to-end MNIST classifier's generalization performance.
- Lower mean NLL and MSE losses and higher whole-board accuracy indicate better performance in both experiment plots.