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

Introduction

Although modern deep learning has produced groundbreaking improvements in a variety of domains, state-of-the-art methods still struggle to capture “hard” and “global” constraints arising from discrete logical relationships. Motivated by this deficiency, there has been a great deal of recent interest in integrating logical or symbolic reasoning into neural network architectures (Palm et al., 2017; Yang et al., 2017; Cingillioglu & Russo, 2018; Evans & Grefenstette, 2018). However, with few exceptions, previous work primarily focuses on integrating preexisting relationships into a larger differentiable system via tunable continuous parameters, not on discovering the discrete relationships that produce a set of observations in a truly end-to-end fashion. As an illustrative example, consider the popular logic-based puzzle game Sudoku, in which a player must fill in a $9\times 9$ partially-filled grid of numbers to satisfy specific constraints. If the rules of Sudoku (i.e. the relationships between problem variables) are not given, then it may be desirable to jointly learn the rules of the game and learn how to solve Sudoku puzzles in an end-to-end manner.

We consider the problem of learning logical structure specifically as expressed by satisfiability problems – concretely, problems that are well-modeled as instances of SAT or MAXSAT (the optimization analogue of SAT). This is a rich class of domains encompassing much of symbolic AI, which has traditionally been difficult to incorporate into neural network architectures since neural networks rely on continuous and differentiable parameterizations. Our key contribution is to develop and derive a differentiable smoothed MAXSAT solver that can be embedded within more complex deep architectures, and show that this solver enables effective end-to-end learning of logical relationships from examples (without hard-coding of these relationships). More specifically, we build upon recent work in fast block coordinate descent methods for solving SDPs (Wang et al., 2017) to build a differentiable solver for the smoothed SDP relaxation of MAXSAT. We provide an efficient mechanism to differentiate through the optimal solution of this SDP by using a similar block coordinate descent solver as used in the forward pass. Our module is amenable to GPU acceleration, greatly improving training scalability.

Using this framework, we are able to solve several problems that, despite their simplicity, prove essentially impossible for traditional deep learning methods and existing logical learning methods to reliably learn without any prior knowledge. In particular, we show that we can learn the parity function, known to be challenging for deep classifiers (Shalev-Shwartz et al., 2017), with only single bit supervision. We also show that we can learn to play $9\times 9$ Sudoku, a problem that is challenging for modern neural network architectures (Palm et al., 2017). We demonstrate that our module quickly recovers the constraints that describe a feasible Sudoku solution, learning to correctly solve 98.3% of puzzles at test time without any hand-coded knowledge of the problem structure. Finally, we show that we can embed this differentiable solver into larger architectures, solving a “visual Sudoku” problem where the input is an image of a Sudoku puzzle rather than a binary representation. We show that, in a fully end-to-end setting, our method is able to integrate classical convolutional networks (for digit recognition) with the differentiable MAXSAT solver (to learn the logical portion). Taken together, this presents a substantial advance toward a major goal of modern AI: integrating logical reasoning into deep learning architectures.

Related work

Recently, the deep learning community has given increasing attention to the concept of embedding complex, “non-traditional” layers within deep networks in order to train systems end-to-end. Major examples have included logical reasoning modules and optimization layers. Our work combines research in these two areas by exploiting optimization-based relaxations of logical reasoning structures, namely an SDP relaxation of MAXSAT. We explore each of these relevant areas of research in more detail below.

Our work is closely related to recent interest in integrating logical reasoning into deep learning architectures (Garcez et al., 2015). Most previous systems have focused on creating differentiable modules from an existing set of known relationships, so that a deep network can learn the parameters of these relationships (Dai et al., 2018; Manhaeve et al., 2018; Sourek et al., 2018; Xu et al., 2018; Hu et al., 2016; Yang et al., 2017; Selsam et al., 2018). For example, Palm et al. (2017) introduce a network that carries out relational reasoning using hand-coded information about which variables are allowed to interact, and test this network on $9\times 9$ Sudoku. Similarly, Evans & Grefenstette (2018) integrate inductive logic programming into neural networks by constructing differentiable SAT-based representations for specific “rule templates.” While these networks are seeded with prior information about the relationships between variables, our approach learns these relationships and their associated parameters end-to-end. While other recent work has also tried to jointly learn rules and parameters, the problem classes captured by these architectures have been limited. For instance, Cingillioglu & Russo (2018) train a neural network to apply a specific class of logic programs, namely the binary classification problem of whether a given set of propositions entails a specific conclusion. While this approach does not rely on prior hand-coded structure, our method applies to a broader class of domains, encompassing any problem reducible to MAXSAT.

Our work also fits within a line of research leveraging optimization as a layer in neural networks. For instance, previous work has introduced differentiable modules for quadratic programs (Amos & Kolter, 2017; Donti et al., 2017), submodular optimization problems (Djolonga & Krause, 2017; Tschiatschek et al., 2018; Wilder et al., 2018), and equilibrium computation in zero-sum games (Ling et al., 2018). To our knowledge, ours is the first work to use differentiable SDP relaxations to capture relationships between discrete variables.

We build on a long line of research exploring SDP relaxations as a tool for solving MAXSAT and related problems. Classical work shows that such relaxations produce strong approximation guarantees for MAXCUT and MAX-2SAT (Goemans & Williamson, 1995), and are empirically tighter than standard linear programming relaxations (Gomes et al., 2006). More recent work, e.g. Wang et al. (2017); Wang & Kolter (2019), has developed low-rank SDP solvers for general MAXSAT problems. We extend the work of Wang et al. (2017) to create a differentiable optimization-based MAXSAT solver that can be employed in the loop of deep learning.

A differentiable satisfiability solver

The MAXSAT problem is the optimization analogue of the well-known satisfiability (SAT) problem, in which the goal is to maximize the number of clauses satisfied. We present a differentiable, smoothed approximate MAXSAT solver that can be integrated into modern deep network architectures. This solver uses a fast coordinate descent approach to solving an SDP relaxation of MAXSAT. We describe our MAXSAT SDP relaxation as well as the forward pass of our MAXSAT deep network layer (which employs this relaxation). We then show how to analytically differentiate through the MAXSAT SDP and efficiently solve the associated backward pass.

Despite its non-convexity, problem (2) can then be solved optimally via coordinate descent for all $i=\top,1,\ldots,n$. In particular, the objective terms that depend on $v_{i}$ are given by $v_{i}^{T}\sum_{j=0}^{n}s_{i}^{T}s_{j}v_{j}$, where $s_{i}$ is the $i$th column vector of $S$. Minimizing this quantity over $v_{i}$ subject to the constraint that $\|v_{i}\|=1$ yields the coordinate descent update

These updates provably converge to the globally optimal fixed point of the SDP (2) (Wang et al., 2017). A more detailed derivation of this update can be found in Appendix A.

2 SATNet: Satisfiability solving as a layer

Using our MAXSAT SDP relaxation and associated coordinate descent updates, we create a deep network layer for satisfiability solving (SATNet). Define $\mathcal{I}\subset\{1,\ldots,n\}$ to be the indices of MAXSAT variables with known assignments, and let $\mathcal{O}\equiv\{1,\ldots,n\}\setminus\mathcal{I}$ correspond to the indices of variables with unknown assignments. Our layer admits probabilistic or binary inputs $z_{\iota}\in,\iota\in\mathcal{I}$, and then outputs the assignments of unknown variables $z_{o}\in,o\in\mathcal{O}$ which are similarly probabilistic or (optionally, at test time) binary. We let $Z_{\mathcal{I}}\in^{|\mathcal{I}|}$ and $Z_{\mathcal{O}}\in^{|\mathcal{O}|}$ refer to all input and output assignments, respectively.

The outputs $Z_{\mathcal{O}}$ are generated from inputs $Z_{\mathcal{I}}$ via the SDP (2), and the weights of our layer correspond to the SDP’s low-rank coefficient matrix $S$. This forward pass procedure is pictured in Figure 1. We describe the steps of layer initialization and the forward pass in Algorithm 1, and in more detail below.

When initializing SATNet, the user must specify a maximum number of clauses $m$ that this layer can represent. It is often desirable to set $m$ to be low; in particular, low-rank structure can prevent overfitting and thus improve generalization.

Given this low-rank structure, a user may wish to somewhat increase the layer’s representational ability via auxiliary variables. The high-level intuition here follows from the conjunctive normal form (CNF) representation of boolean satisfaction problems; adding additional variables to a problem can dramatically reduce the number of CNF clauses needed to describe that problem, as these variables play a role akin to register memory that is useful for inference.

Finally, we set $k=\sqrt{2n}+1$, where here $n$ captures the number of actual problem variables in addition to auxiliary variables. This is the minimum value of $k$ required for our MAXSAT relaxation (2) to recover the optimal solution of its associated SDP (Barvinok, 1995; Pataki, 1998).

2.2 Step 1: Relaxing layer inputs

(This equation is derived from the probabilistic relationship described in Section 3.1 between discrete variables and their continuous relaxations.) Constraint (4) can be satisfied by

2.3 Step 2: Generating continuous relaxations of outputs via SDP

Our coordinate descent algorithm for the forward pass is detailed in Algorithm 9. This algorithm maintains the term $\Omega=VS^{T}$ needed to compute $g_{o}$, and then modifies it via a rank-one update during each inner iteration. Accordingly, the per-iteration runtime is $O(nmk)$ (and in practice, only a small number of iterations is required for convergence).

2.4 Step 3: Generating discrete or probabilistic outputs

Given the relaxed outputs $V_{\mathcal{O}}$ from coordinate descent, our layer converts these outputs to discrete or probabilistic variable assignments $Z_{\mathcal{O}}$ via either thresholding or randomized rounding (which we describe here).

The main idea of randomized rounding is that for every $v_{o},o\in\mathcal{O}$, we can take a random hyperplane $r$ from the unit sphere and assign

During training, we do not explicitly perform randomized rounding. We instead note that the probability that $v_{o}$ and $v_{\top}$ are on the same side of any given $r$ is

During testing, we can either output probabilistic outputs in the same fashion, or output discrete assignments via thresholding or randomized rounding. If using randomized rounding, we round multiple times, and then set $z_{o}$ to be the boolean solution maximizing the MAXSAT objective in Equation (1). Prior work has observed that such repeated rounding improves approximation ratios in practice, especially for MAXSAT problems (Wang & Kolter, 2019).

3 Computing the backward pass

where we obtain $\nicefrac{{\partial z_{o}}}{{\partial v_{o}}}$ by differentiating through Equation (7) (or, more readily, by implicitly differentiating through its rearrangement $\cos(\pi z_{o})=-v_{\top}^{T}v_{o}$).

3.2 Backpropagation through the SDP

where $S_{\mathcal{I}}$ is the $\mathcal{I}$-indexed column subset of $S$, and the gradient with respect to the layer weights is

We defer the derivation of Theorem 11 to Appendix B. Although this derivation is somewhat involved, the concept at a high level is quite simple: we differentiate the solution of the SDP problem (Section 3.1) with respect to the problem’s parameters and input, which requires computing the (relatively large) matrix-vector solve given in Equation (9).

To solve Equation (9), we use a coordinate descent approach that closely mirrors the coordinate descent procedure employed in the forward pass, and which has similar fast convergence properties. This procedure, described in Algorithm 9, enables us to compute the desired gradients without needing to maintain intermediate Jacobians explicitly. Mirroring the forward pass, we use rank-one updates to maintain and modify the term $\Psi=US^{T}$ needed to compute $\mathsf{d}g_{o}$, which again enables our algorithm to run in $O(nmk)$ time. We defer the derivation of Algorithm 9 to Appendix D.

3.3 From relaxed to original inputs

4 An efficient GPU implementation

The coordinate descent updates in Algorithms 9 and 9 dominate the computational costs of the forward and backward passes, respectively. We thus present an efficient, parallel GPU implementation of these algorithms to speed up training and inference. During the inner loop of coordinate descent, our implementation parallelizes the computation of all $g_{o}$ ($\mathsf{d}g_{o}$) terms by parallelizing the computation of $\Omega$ ($\Psi$), as well as of all rank-one updates of $\Omega$ ($\Psi$). This underscores the benefit of using a low-rank SDP formulation in our MAXSAT layer, as traditional full-rank coordinate descent cannot be efficiently parallelized. We find in our preliminary benchmarks that our GPU CUDA-C implementation is up to $18-30$x faster than the corresponding OpenMP implementation run on Xeon CPUs. Source code for our implementation is available at https://github.com/locuslab/SATNet.

Experiments

We test our MAXSAT layer approach in three domains that are traditionally difficult for neural networks: learning the parity function with single-bit supervision, learning $9\times 9$ Sudoku solely from examples, and solving a “visual Sudoku” problem that generates the logical Sudoku solution given an input image of a Sudoku puzzle. We find that in all cases, we are able to perform substantially better on these tasks than previous deep learning-based approaches.

This experiment tests SATNet’s ability to differentiate through many successive SAT problems by learning to compute the parity function. The parity of a bit string is defined as one if there is an odd number of ones in the sequence and zero otherwise. The task is to map input sequences to their parity, given a dataset of example sequence/parity pairs. Learning parity functions from such single-bit supervision is known to pose difficulties for conventional deep learning approaches (Shalev-Shwartz et al., 2017). However, parity is simply a logic function – namely, a sequence of XOR operations applied successively to the input sequence.

Hence, for a sequence of length $L$, we construct our model to contain a sequence of $L-1$ SATNet layers with tied weights (similar to a recurrent network). The first layer receives the first two binary values as input, and layer $d$ receives value $d$ along with the rounded output of layer $d-1$. If each layer learns to compute the XOR function, the combined system will correctly compute parity. However, this requires the model to coordinate a long series of SAT problems without any intermediate supervision.

Figure 2 shows that our model accomplishes this task for input sequences of length $L=20$ and $L=40$. For each sequence length, we generate a dataset of 10K random examples (9K training and 1K testing). We train our model using cross-entropy loss and the Adam optimizer (Kingma & Ba, 2015) with a learning rate of $10^{-1}$. We compare to an LSTM sequence classifier, which uses 100 hidden units and a learning rate of $10^{-3}$ (we tried varying the architecture and learning rate but did not observe any improvement). In each case, our model quickly learns the target function, with error on the held-out set converging to zero within 20 epochs. In contrast, the LSTM is unable to learn an appropriate representation, with only minor improvement over the course of 100 training epochs; across both input lengths, it achieves a testing error rate of at best 0.476 (where a random guess achieves value 0.5).

2 Sudoku (original and permuted)

In this experiment, we test SATNet’s ability to infer and recover constraints simply from bit supervision (i.e. without any hard-coded specification of how bits are related). We demonstrate this property via Sudoku. In Sudoku, given a (typically) $9\times 9$ partially-filled grid of numbers, a player must fill in the remaining empty grid cells such that each row, each column, and each of nine $3\times 3$ subgrids contains exactly one of each number from 1 through 9. While this constraint satisfaction problem is computationally easy to solve once the rules of the game are specified, actually learning the rules of the game, i.e. the hard constraints of the puzzle, has proved challenging for traditional neural network architectures. In particular, Sudoku problems are often solved computationally via tree search, and while tree search cannot be easily performed by neural networks, it is easily expressible using SAT and MAXSAT problems.

We construct a SATNet model for this task that takes as input a logical (bit) representation of the initial Sudoku board along with a mask representing which bits must be learned (i.e. all bits in empty Sudoku cells). This input is vectorized, which means that our SATNet model cannot exploit the locality structure of the input Sudoku grid when learning to solve puzzles. Given this input, the SATNet layer then outputs a bit representation of the Sudoku board with guesses for the unknown bits. Our model architecture consists of a single SATNet layer with 300 auxiliary variables and low rank structure $m=600$, and we train it to minimize a digit-wise negative log likelihood objective (optimized via Adam with a $2\times 10^{-3}$ learning rate).

We compare our model to a convolutional neural network baseline modeled on that of Park (2016), which interprets the bit inputs as 9 input image channels (one for each square in the board) and uses a sequence of 10 convolutional layers (each with 512 3$\times$3 filters) to output the solution. The ConvNet makes explicit use of locality in the input representation since it treats the nine cells within each square as a single image. We also compare to a version of the ConvNet which receives a binary mask indicating which bits need to be learned (ConvNetMask). The mask is input as a set of additional image channels in the same format as the board. We trained both architectures using mean squared error (MSE) loss (which gave better results than negative log likelihood for this architecture). The loss was optimized using Adam (learning rate $10^{-4}$). We additionally tried to train an OptNet (Amos & Kolter, 2017) model for comparison, but this model made little progress even after a few days of training. (We compare our method to OptNet on a simpler $4\times 4$ version of the Sudoku problem in Appendix E.)

Our results for the traditional $9\times 9$ Sudoku problem (over 9K training examples and 1K test examples) are shown in Table 1. (Convergence plots for this experiment are shown in Appendix F.) Our model is able to learn the constraints of the Sudoku problem, achieving high accuracy early in the training process (95.0% test accuracy in 22 epochs/37 minutes on a GTX 1080 Ti GPU), and demonstrating 98.3% board-wise test accuracy after 100 training epochs (172 minutes). On the other hand, the ConvNet baseline does poorly. It learns to correctly solve 72.6% of puzzles in the training set but fails altogether to generalize: accuracy on the held-out set reaches at most 0.04%. The ConvNetMask baseline, which receives a binary mask denoting which entries must be completed, performs only somewhat better, correctly solving 15.1% of puzzles in the held-out set. We note that our test accuracy is qualitatively similar to the results obtained in Palm et al. (2017), but that our network is able to learn the structure of Sudoku without explicitly encoding the relationships between variables.

To underscore that our architecture truly learns the rules of the game, as opposed to overfitting to locality or other structure in the inputs, we test our SATNet architecture on permuted Sudoku boards, i.e. boards for which we apply a fixed permutation of the underlying bit representation (and adjust the corresponding input masks and labels accordingly). This removes any locality structure, and the resulting Sudoku boards do not have clear visual analogues that can be solved by humans. However, the relationships between bits are unchanged (modulo the permutation) and should therefore be discoverable by architectures that can truly learn the underlying logical structure. Table 1 shows results for this problem in comparison to the convolutional neural network baselines. Our architecture is again able to learn the rules of the (permuted) game, demonstrating the same 98.3% board-wise test accuracy as in the original game. In contrast, the convolutional neural network baselines perform even more poorly than in the original game (achieving 0% test accuracy even with the binary mask as input), as there is little locality structure to exploit. Overall, these results demonstrate that SATNet can truly learn the logical relationships between discrete variables.

3 Visual Sudoku

In this experiment, we demonstrate that SATNet can be integrated into larger deep network architectures for end-to-end training. Specifically, we solve the visual Sudoku problem: that is, given an image representation of a Sudoku board (as opposed to a one-hot encoding or other logical representation) constructed with MNIST digits, our network must output a logical solution to the associated Sudoku problem. An example input is shown in Figure 3. This problem cannot traditionally be represented well by neural network architectures, as it requires the ability to combine multiple neural network layers without hard-coding the logical structure of the problem into intermediate logical layers.

Our architecture for this problem uses a convolutional neural network connected to a SATNet layer. Specifically, we apply a convolutional layer for digit classification (which uses the LeNet architecture (LeCun et al., 1998)) to each cell of the Sudoku input. Each cell-wise probabilistic output of this convolutional layer is then fed as logical input to the SATNet layer, along with an input mask (as in Section 4.2). This SATNet layer employs the same architecture and training parameters as described in the previous section. The whole model is trained end-to-end to minimize cross-entropy loss, and is optimized via Adam with learning rates $2\times 10^{-3}$ for the SATNet layer and $10^{-5}$ for the convolutional layer.

We compare our approach against a convolutional neural network which combines two sets of convolutional layers. First, the visual inputs are passed through the same convolutional layer as in our SATNet model, which outputs a probabilistic bit representation. Next, this representation is passed through the convolutional architecture that we compared to for the original Sudoku problem, which outputs a solution. We use the same training approach as above.

Table 1 summarizes our experimental results (over 9K training examples and 1K test examples); additional plots are shown in Appendix F. We contextualize these results against the theoretical “best” testing accuracy of 74.7%, which accounts for the Sudoku digit classification accuracy of our specific convolutional architecture; that is, assuming boards with 36.2 out of 81 filled cells on average (as in our test set) and an MNIST model with 99.2% test accuracy (LeCun et al., 1998), we would expect a perfect Sudoku solver to output the correct solution 74.7% ($=0.992^{36.2}$) of the time. In 100 epochs, our model learns to correctly solve 63.2% of boards at test time, reaching 85% of this theoretical “best.” Hence, our approach demonstrates strong performance in solving visual Sudoku boards end-to-end. On the other hand, the baseline convolutional networks make only minuscule improvements to the training loss over the course of 100 epochs, and fail altogether to improve out-of-sample performance. Accordingly, our SATNet architecture enables end-to-end learning of the “rules of the game” directly from pictorial inputs in a way that was not possible with previous architectures.

Conclusion

In this paper, we have presented a low-rank differentiable MAXSAT layer that can be integrated into neural network architectures. This layer employs block coordinate descent methods to efficiently compute the forward and backward passes, and is amenable to GPU acceleration. We show that our SATNet architecture can be successfully used to learn logical structures, namely the parity function and the rules of $9\times 9$ Sudoku. We also show, via a visual Sudoku task, that our layer can be integrated into larger deep network architectures for end-to-end training. Our layer thus shows promise in allowing deep networks to learn logical structure without hard-coding of the relationships between variables.

More broadly, we believe that this work fills a notable gap in the regime spanning deep learning and logical reasoning. While many “differentiable logical reasoning” systems have been proposed, most of them still require fairly hand-specified logical rules and groundings, and thus are somewhat limited in their ability to operate in a truly end-to-end fashion. Our hope is that by wrapping a powerful yet generic primitive such as MAXSAT solving within a differentiable framework, our solver can enable “implicit” logical reasoning to occur where needed within larger frameworks, even if the precise structure of the domain is unknown and must be learned from data. In other words, we believe that SATNet provides a step towards integrating symbolic reasoning and deep learning, a long-standing goal in artificial intelligence.

Acknowledgments

Po-Wei Wang is supported by a grant from the Bosch Center for AI; Priya Donti is supported by the Department of Energy’s Computational Science Graduate Fellowship under grant number DE-FG02-97ER25308; and Bryan Wilder is supported by the National Science Foundation Graduate Research Fellowship.

References

Appendix A Derivation of the forward pass coordinate descent update

Our MAXSAT SDP relaxation (described in Section 3.1) is given by

We rewrite the objective of (A.1) as $\langle S^{T}S,V^{T}V\rangle\equiv\operatorname{tr}((S^{T}S)^{T}(V^{T}V))=\operatorname{tr}(V^{T}VS^{T}S)$ by noting that $S^{T}S$ is symmetric and by cycling matrices within the trace. We then observe that the objective terms that depend on any given $v_{i}$ are given by

where $s_{i}$ is the $i$th column vector of $S$. Observe $v_{i}^{T}v_{i}$ in the last term cancels to $1$, and the remaining coefficient

is constant with respect to $v_{i}$. Thus, (A.2) can be simply rewritten as

Minimizing this expression over $v_{i}$ with respect to the constraint $\|v_{i}\|=1$ yields the block coordinate descent update

Appendix B Details on backpropagation through the MAXSAT SDP

Computing the total differential of the updates (3) and rearranging, we see that for every $o\in\mathcal{O}$,

and where $P_{o}\equiv I_{k}-v_{o}v_{o}^{T},o\in\mathcal{O}$ and $\mathcal{I}^{\prime}\equiv\{\top\}\,\cup\,\mathcal{I}$.

Rewriting Equation B.1 over all $o\in\mathcal{O}$ as a linear system, we obtain

where $C=S_{\mathcal{O}}^{T}S_{\mathcal{O}}-\operatorname{diag}(\|s_{o}\|^{2})$, $P=\operatorname{diag}(P_{o})$, and the second step follows from the lemma presented in Appendix C.

where the second equality comes from plugging in the result of (B.3).

Then, we see that (B.4) can be written as

which is the implicit linear form for our gradients.

where $u_{i}$ is the $i$th column of $U$, and where $S_{\mathcal{I}}$ denotes the $\mathcal{I}$-indexed column subset of $S$.

Appendix C Proof of pseudoinverse computations

We prove the following lemma, used to derive the implicit total differential for $\operatorname{vec}(\mathsf{d}V_{\mathcal{O}})$.

where $P=\operatorname{diag}(I_{k}-v_{o}v_{o}^{T})$, $C=S_{\mathcal{O}}^{T}S_{\mathcal{O}}-\operatorname{diag}(\|s_{o}\|^{2})$, $D=\operatorname{diag}(\|g_{i}\|)$, and $\xi_{o}$ is as defined in Equation (B.2).

Examining the equation with respect to $\mathsf{d}v_{i}$ gives

which implies that for all $i$, $\mathsf{d}v_{i}=P_{i}y_{i}$ for some $y_{i}$. Substituting $y_{i}$ into the equality gives

Note that the last equation comes form $D\otimes I_{k}P=D\otimes I_{k}PP=P(D\otimes I_{k})P$ due to the block diagonal structure of the projection $P$. Thus, by the properties of projectors and the pseudoinverse,

Note that the first equation comes from the idempotence property of $P$ (that is, $PP=P$). Substituting $\operatorname{vec}(\mathsf{d}V_{\mathcal{O}})=P\operatorname{vec}(Y)$ back gives the solution of $\mathsf{d}V_{\mathcal{O}}$. ∎

Appendix D Derivation of the backward pass coordinate descent algorithm

Consider solving for $U_{\mathcal{O}}$ as mentioned in Equation (B.5):

where $C=S_{\mathcal{O}}^{T}S_{\mathcal{O}}-\operatorname{diag}(\|s_{o}\|^{2})$. The linear system can be computed using block coordinate descent. Specifically, observe this linear system with respect to only the $u_{o}$ variable. Since we start from $U_{\mathcal{O}}=0$, we can assume that $P\operatorname{vec}(U_{o})=\operatorname{vec}(U_{o})$. This yields

Let $\Psi=(U_{\mathcal{O}})S^{T}_{\mathcal{O}}$. Then we have

Define $-\mathsf{d}g_{i}$ to be the terms contained in parentheses in the right-hand side of the above equation. Note that $\mathsf{d}g_{i}$ does not depend on the variable $u_{o}$. Thus, we have the closed-form feasible solution

After updating $u_{o}$, we can maintain the term $\Psi$ by replacing the old $u^{\text{prev}}_{o}$ with the new $u_{o}$. This yields the rank 1 update

The above procedure is summarized in Algorithm 9. Further, we can verify that the assumption $P\operatorname{vec}(U_{\mathcal{O}})=\operatorname{vec}(U_{\mathcal{O}})$ still holds after each update by the projection $P_{o}$.

Appendix E Results for the 4×4444\times 4 Sudoku problem

We compare the performance of our SATNet architecture on a $4\times 4$ reduced version of the Sudoku puzzle against OptNet (Amos & Kolter, 2017) and a convolutional neural network architecture. These results (over 9K training and 1K testing examples) are shown in Figure E.1. We note that our architecture converges quickly – in just two epochs – to 100% board-wise test accuracy.

OptNet takes slightly longer to converge to similar performance, in terms of both time and epochs. In particular, we see that OptNet takes 3-4 epochs to converge (as opposed to 1 epoch for SATNet). Further, in our preliminary benchmarks, OptNet required 12 minutes to run 20 epochs on a GTX 1080 Ti GPU, whereas SATNet took only 2 minutes to run the same number of epochs. In other words, we see that SATNet requires fewer epochs to converge and takes less time per epoch than OptNet.

Both our SATNet architecture and OptNet outperform the traditional convolutional neural network in this setting, as the ConvNet somewhat overfits to the training set and therefore does not generalize as well to the test set (achieving 93% accuracy). The ConvNetMask, which additionally receives a binary input mask, performs much better (99% test accuracy) but does not achieve perfect performance as in the case of OptNet and SATNet.

Appendix F Convergence plots for 9×9999\times 9 Sudoku experiments

Convergence plots for our $9\times 9$ Sudoku experiments (original and permuted) are shown in Figure F.1. SATNet performs nearly identically in both the original and permuted settings, generalizing well to the test set at every epoch without overfitting to the training set. The ConvNet and ConvNetMask, on the other hand, do not generalize well. In the original setting, both architectures overfit to the training set, showing little-to-no improvement in generalization performance over the course of training. In the permuted setting, both ConvNet and ConvNetMask make little progress even on the training set, as they are not able to rely on spatial locality of inputs.

Convergence plots for the visual Sudoku experiments are shown in Figure F.2. Here, we see that SATNet generalizes well in terms of loss throughout the training process, and generalizes somewhat well in terms of whole-board accuracy. The difference in generalization performance between the logical and visual Sudoku settings can be attributed to the generalization performance of the MNIST classifier trained end-to-end with our SATNet layer. The ConvNetMask architecture overfits to the training set, and the ConvNet architecture makes little-to-no progress even on the training set.