Learning Reliable Logical Rules with SATNet
Authors: Zhaoyu Li
Jinpei Guo
Yuhe Jiang
Xujie Si
Venue: NeurIPS 2023 poster (2023)
Keywords: Logical Reasoning
Rule Learning
Interpretation
SATNet

Abstract: Bridging logical reasoning and deep learning is crucial for advanced AI systems. In this work, we present a new framework that addresses this goal by generating interpretable and verifiable logical rules through differentiable learning, without relying on pre-specified logical structures. Our approach builds upon SATNet, a differentiable MaxSAT solver that learns the underlying rules from input-output examples. Despite its efficacy, the learned weights in SATNet are not straightforwardly interpretable, failing to produce human-readable rules. To address this, we propose a novel specification method called ``maximum equality'', which enables the interchangeability between the learned weights of SATNet and a set of propositional logical rules in weighted MaxSAT form. With the decoded weighted MaxSAT formula, we further introduce several effective verification techniques to validate it against the ground truth rules. Experiments on stream transformations and Sudoku problems show that our decoded rules are highly reliable: using exact solvers on them could achieve 100% accuracy, whereas the original SATNet fails to give correct solutions in many cases. Furthermore, we formally verify that our decoded logical rules are functionally equivalent to the ground truth ones.

Learning Reliable Logical Rules with SATNet
Zhaoyu Li Jinpei Guo", Yuhe Jiang', Xujie Si University of Toronto, Vector Institute, Mila, *Shanghai Jiao Tong Univeristy {zhaoyu, six} toronto. edu
Abstract
Bridging logical reasoning and deep learning is crucial for advanced AI systems. this work, we present a new framework that addresses this goal by generating interpretable and verifiable logical rules through differentiable learning, without relying on pre-specified logical structures. Our approach builds upon SATNet, a differentiable MaxSAT solver that learns the underlying rules from input-output examples. Despite its efficacy, the learned weights in SATNet are not straight- forwardly interpretable, failing to produce human-readalee rules. To address this, we propose novel specification method called "maximum equality", which en- ables the interchangeability between the leameed weights of SATNet and a of propositional logical rules in weighted MaxSAT form. With the decoded weighted MaxSAT formula, we further introduce several effective verification techniques validate it against the ground truth rules, Experiments on stream transformations and Sudoku problems show that our decoded rules highly reliable: using exact solvers on them could achieve 100% accuracy, whereas the original SATNet fails to give correct solutions in many cases. Furthermore, we formally verify that our decoded logical rules are functionally equivalent to the ground truth ones.
Introduction
Logical reasoning is fundamental cognitive skill that empowers humans to organize knowledge structured form, reason about relationships between different pieces of information, and draw inferences based on logical rules and constraints. In recent years, there has been growing research interest in integrating advanced deep learning systems with the ability of logical reasoning 19 I0 23 (2]. A notable outcome in this field is SATNet (32), differenniablee MaxSAT solver based on a low-rank semidefinite programming (SDP) approach. SATNet utilizes a learnable matrix to capture the underlying structure of logical rules and dynamically adjusts its weight from input-output examples. This innovative design enables SATNet to learn sophisticated logical rules, such as the parity function and Sudoku puzzles.
Despite the promising results SATNet, the interpretability of its learned weights remains unclear. This limitation arises from the fact that the clause matrix S learned by SATNet is not ternary preventing its explicit interpretation as a set logical rules as originally motivated [33]. Consequently, this poses challenge the wider adoption of SATNet in real-world applications that require transparent decision decision-making making processes.
To address this limitation, we present a new framework that extracts a set of interpretable logical rules from the learned weights in SATNet. We first demonstrate that merely rounding S to a ternary matrix is insufficient for interpretation and then show empirical and theoretical evidence that S may fail to capture the underlying logical rules in certain cases. Instead of directly decoding S, we propose utilizing the matrix C 5" 5 to derive explicit logical rules, based on the SDP formulation in
In SATNet's ss original formulation, it assumes the S matrix only consist of 1, -1, and 0 elements represent the logical formula in MaxSAT form. However, after training, S is continuous rather than ternayy.
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

f=028=03
Map
SDP reloattion (welght
Round
(Trining)
di 12- m Asp =2R
Zue 0.
Beland
Beband
Aupo ti-a uuuusaty
Portial ecsignments
Inputs
Input variables
Domain knowledge (optionat)
Output veriables
Labels
Inferonce)
piont SE 56780
peot 3057 2077
h12
2 0,5
9 110011122 12.0
Verificatioon
h333660
sclver
Map
h- 1063 hiss 5557 1-10070
0 Fox
31 6300
Ground truth rules
Decaded rules
Octput variables
Ounputs
[SAT formula)
(Weighted MixsAT fonmula)
Figure 1: An example pipeline of our framework for 4 x Sudoku problem. We first train SATNNet to learn the Sudoku rules from data. After training, we use maximum equality specification to decode set of interpretable rules as weighted MaxSAT formula from the learned weight C. Given the decoded rules, we call an exact solver for inference and further verify them with ground truth rules. Optional domain knowledge can be incorporated through numerical weights propositional rules.
SATNet. Specifically, we introduce novel specification formulation called "maximum equality", which transforms the learned matrix C' into a weighted MaxSAT formula. We rigorously prove that our proposed formulation has a powerful expressive ability, enabling C' to represent any propositional logical rules under proper parameterization.
With the decoded logical rules, we can employ an exact solver (e.g., Gurobi [13] to replace SATNet during inference, rendering the solving process more accurate and transparent. Additionally, our specification method offers flexibility incorporating prior domain knowledge in propositional logic, This integration can be done through either the learned weights C' or the weighted MaxSAT formula, bolstering the reliability of our learned or decoded rules. To further validate the correctness of the decoded logical rules, we propose several verification techniques that prove the equivalence between our decoded weighted MaxSAT formula and the numan-written written rules in SAT form. In particular, we establish that if the optimal solution of the weighted MaxSAT formula always corresponds to satisfying assignment the SAT formula for any valid partial inputs, then these two formulas function equivalently. Notably, when the space of inputs becomes excessively huge, we introduce a sufficient condition for an efficient equivalence check, which assures not only the functional equivalence but also similar distribution of solution space. We summarize our proposed framework in Figure
To evaluate the efficacy of our proposed framework, conduct a series of experiments various tasks, including stream transformations (i.e., the parity function, addition, and counting) and Sudoku puzzles. For stream transformations, we strictly verify that our decoded weighted MaxSAT formula is functionally equivalent to the human-written logical rules, which ensures that it accurately captures the underlying logic these tasks. On Sudoku puzzles, we show that using exact solvers on our generated formula could achieve 100% accuracy the testing set and further verify that it functions equivalently the ground truth for all unique puzzle inputs. Conversely, SATNet fails to achieve perfect accuracy Sudoku puzzles, where we certify this is because SATNet gives sub-optimal solution to our decoded weighted MaxSAT formula.
In summary, our contributions include:
We pinpoint the interpretability challenges inherent in the original SATNet and present both empirical and theoretical insights into SAT'et''s inability to capture logical rules in some cases.
We introduce a novel interpretation method that decodes a set of logical rules as a weighted MaxSAT formula from SATNet and enables the flexible integration of domain knowledge.
We propose multiple verification approaches validate the correctness of our decoded rules with human-written ground truth rules.
Experiments on stream transformations and Sudoku puzzles show that our decoded weighted MaxSAT formula exactly captures the underlying logical rules and is verifiably reliable.

---

2 Background
2.1 Problem Formulation
In this paper, we focus on problems whose inherent logical rules can be expressed using propositional logic. For a given logical problem, define set of na problem Boolean variables 21, 2na to represent the potential relationships within the problem and express the ground truth logical rules as SAT formula ((21, Znz). The dataset DD consists of input-output examples (x; yi), where each example partitions nd variables to an input set Zz and an output set Zo and assigns a value to each variable accordingly. The task is to learn the underlying logical rules from the datasets D such that the learned rules ø' can accurately map the input variables 2; E Zz to the output variables 2n E Zo. similar how the ground truth rules & conduct the mapping.
Let's take 4 x 4 Sudoku as an example. In this case, we have a total of 64 variables, where each successive group of 4 variables represents single grid in the puzzle that can hold values ranging from to 4. Each input xj in the dataset D corresponds to the initially provided values in a Sudoku puzzle, and the output y1 represents the solved values of that puzzle. We transform each input-output example to construct an input set 2, E Zz and an output set 2, E Ze. For instance, if variables 21; 22, 23, 24 correspond to the values of the first grid in the Sudoku board, and the given value is 4, then variables 21,..... 24 E Zz with the configuration 21 = 0, 2/ = O, 23 = 0, 24 = 1. The task is to learn the inherent Sudoku rules from the dataset D such that given the initial known values of Sudoku puzzle, the learned logical rules can accurately determine the values of the remaining cells.
2.2 SATNet
SATNet [32] is a differentiable MaxSAT solver that models the underlying rules é in the data as a MaxSAT problem and solves using SDP relaxation. It assumes that the logical rules are written in conjunctive normal form with ny defined variables 2 E {-1, 1]" and m clauses, which can be represented by a clause matrix $ {1, 11,001m0m4 Specifically, each element 8,y in S denotes the sign of variable &; in clause j. The MaxSAT problem can be formulated as follows:
na VV 15,22 0).
maximize 2E1-1,13
(1)
SATNet applies semidefinite relaxation to Equation by relaxing each variable to unit vector 2 E R$ with respect to a unit "truth direction" " ut based on the randomized rounding [12].
additionally introduces coefficient vector sT {-1] associated with the truth vector and writes
the SDP relaxation of the MaxSAT problem as:
s.t. ||:||| 1, (T, na), minimize (S S, V'V),, VER*x("g-1)
where = [UT, 01,
Uny] E (x and S [ST, .,...,, 5n] E Rmx (n+11)
Given the input variables 2j E Zz, SATNet relaxes their values to unit vectors and solves Equation 2 by the mixing method [31], a fast coordinate descent approach. In this method, each output vector to is updated iteratively as follows:
-9o/ Ilsoll. where 9. = V s, - 1| vo. for o O.
The updates in Equation 3 are proven to converge the globally optimal fixed point of the SDP 31 After obtaining the relaxed outputs u, from coordinate descent, SATNet converts each output variable vector probabilistic value by p(=,- 1) cos cos (- UT) / and computes the binary cross- entropy loss between the ground-truth variable assignments 2.. When back-propagee
the loss, SATNet employs a custom algorithm that uses an efficient coordinate descent algorithm directly compute the gradient of S, without explicitly unrolling the forward-pass computations. Such features enable SATNet to learn the S matrix efficiently from input-output examples.
is worth noting that SATNet requires to specify the number of clauses m before learning a clause matrix S. Moreover, to improve the representational power of S, SATNet further incorporates n. auxiliary variables alongside the nı problem-defined variables. These auxiliary variables are considered output variables but not involved in the loss computation.
IIn the original paper of SATNet (32) each row of S is also normalized using the constant /4E, [8iy However, in cases where S is learned (rather than provided), this normalization can be omitted for simplicity.
3

---

3 Methodology
In this section, we first explore the issue of uninterpretability in SATNet by analyzing the clause matrix S. We then revisit the formulation of SATNet and present our specification approach that decodes set of interpretable logical rules from the learned weights C = S" S. After this, we show that our method also allows for the flexible incorporation of domain knowledge via additional rules in propositional logic or the additive weights of C. To validate the correctness of our decoded rules, we introduce several verification strategies to compare them with the human-writter ones.
3.1 Uninterpretability of SATNet
SATNet utilizes the clause matrix S to capture the underlying structure of logical rules and learns its weight through input-output examples. However, SATNet doesn't 't enforce S to be ternary during training. making it hard to directly obtain set of interpretable logical rules from S. Towards deriving human-readable rules from SATNet, we first conduct a range of experiments on the matrix
Rounding S to a ternary matrix. One straightforward idea to derive a ternary matrix from S is to round its weights to the values {1, (1,-1,0}, 0}. To test this approach, we first train SATNet on the 4 x Sudoku dataset, which achieves 100% training accuracy and 99.89% testing accuracy. Subsequently, we apply a threshold function fihre round each entry of S with a threshold value >> O:
finee { 8:j/ Pej//ssll if |sayl >E
O,
otherwise.
In our experiments, we exhaustively evaluate all possible threshold values and round S to set of ternary matrices. We assess the correctness of these matrices by solving Sudoku test instances using an exact MTxSAT solver applied the corresponding MaxSAT formulas. Our empirical result shows that none of these ternary matrices could yield the correct logical rules, as they fail to solve any Sudoku puzzles in the testing set. This finding demonstrates that simply rounding S is insufficient for interpreting the learned weights in SATNet.
Substituting ground truth rules into S. To investigate the representational capability of the clause matrix S. we conduct an experiment by injecting human-written ground truth rules of x 4 Sudoku puzzles into S. If S is truly capable of capturing such logical rules, we would expect SATNet to solve Sudoku test instances quite well when provided with the ground truth rules. Contrarily, SATNet achieves only 53.95% solving accuracy on the testing dataset, giving incorrect solutions for a substantial number of Sudoku puzzles. On the other hand, after training from examples, SATNet could reach near near-perfect solving accuracy without the use of ground truth rules. This discrepancy highlights the difficulty in representing and interpreting the underlying logical rules using S alone.
Limitations of S in representing logical rules. We further supplement our empirical observations with theoretical evidence demonstrating the limitations of the clause matrix S in capturing certain logical rules. Let's consider the parity function example, which has specific ground truth rules and the corresponding (unnormalized) S matrix defined as follows:
1
-1
1
1
Rules in matrix form:
-1
1
S =
1
-1
In this example, the first two variables in the ground truth rules denote the input bits, while the third variable indicates the parity the output bit. SATNet, however, introduces additional truth variable and incorporates it in each clause of with negative polarity. As a result, the matrix C S S becomes diagonal matrix 4- 7, where / is the identity matrix. Given the SDP formulation of SATNet, its optimization remains unaffected by the diagonal elements of C, as the calculations associated with these elements result in constants. When all the off-diagonal entries of C are zero, the SDP becomes trivial, thereby preventing SATNet from capturing any meaningful rules from data. This limitation is not unique the parity function but also extends other logical rules with similar symmetrical properties. Therefore, the clause matrix S defined in SATNet confronts a challenge in interpretability, as theoretically fails represent a range of logical rules.
Our detailed experimental settings are provided in Section

---

3.2 Decoding Interpretable Logical Rules from SATNet
Given the lack of interpretability in SATNet's clause matrix S. the questions of why SATNet is capable of learning the underlying logical rules and how we can decode these rules remain unanswered. To address these questions, we start by revising the optimization formulation of SATNet to a more general form. Building upon this reformulation, we introduce our novel specification approach, "maximum equality", which not only offers a viable interpretation of SATNet but also enables us to derive a set of logical rules in the form of weighted AT using the learned weights of SATNet.
Maximum equality specification. Instead of using the clause matrix S, reformulate Equation in terms of the matrix C = =S (with na auxiliary variables) and decompose it as:
na+ta
minimize VER*x
Σ
Gjj Gy-uu of Ugs s.t. ||vll| = for E (T, na + na).
i=TJ=T
In Equation the objective is to minimize the weighted sum of dot products between all pairs of variable vectors. Considering that all variable vectors are unit vectors, we can view the dot product of By as a measure of similarity between iy and 1/. From this perspective, the objective of Equation 4 is to minimize the similarity between each pair of variable vectors, with the weight cij dictates the importance of each similarity. Based on this observation, we can further view Equation as a relaxation of the following objective:
the
maximize 2E(0.1p"atma
-2. ((z,) 2z)-
(5)
T
Here, .(...) is the Kronecker delta function such that 5(2;, zz) = when 2; =j and 0 else. Equation 5 applics the Kronecker delta function to each pair of Boolean variable assignments (z,, zj) and aims to maximizes the overall values according to each weight -2 cij. Note that The factor of 2 is incorporated because the product of two unit vectors vi 1/ ranges between [-1. 1J. while the Kronecker delta function can only take on values of 0 or 1. We refer to Equation 5 as the "maximum equality" formulation, as it maximizes the weighted equality among pairs of variable assignments.
Expressive power of maximum equality formulation. To dive deeper into the maximum equality formulation, we first prove its representational power in expressing any propositional logical rules. Proposition 1. Our proposed maximum equality formulation can represent arbitrary logical rules within propositional logic, under proper parameterization.
Proof. It is well-established that Max2SAT is NP-Complete [II. To demonstrate that any propo- sitional logical formula can be reduced to a maximum equality formula, we only need to show the reduction from Max2SAT to maximum equality. Given clause (a V b) in Max2SAT formula, can transform it into three maximum equality clauses:
-w (a b) A w (a (a=vT)AA
A (b= (b=
where uT is the truth variable and w can be any weight value. Similarly, the clauses (aV -b). Vb), and (-a V -b) can be mapped to three maximum equality clauses, where each satisfying assignment of the original clause has a weight of 2 - w more than the unsatisfying one. Compiling these translated clauses gives us direct transition from Max2SAT formula to its maximum equality counterpart. While Max2SAT can be transformed to maximum equality by merely introducing a truth variable, general propositional formulas might necessitate more auxiliary variables to reduce to Max2SAT formula. Therefore, to represent any propositional logical formula using maximum equality, we may also need incorporate enough auxiliary variables by setting an appropriate value na-
Transforming maximum equality to weighted MaxSAT. For a maximum equality formula, we can also transform it into more standard form, i.e., weighted MaxSAT formula. Technically, for every clause w (a = b) in a maximum equality formula, we convert it into multiple weighted MaxSAT clauses by introducing
variable d to represent the equality condition a = b follows:
(-a V bbv dd A h Va -bV dd) A w (d), w >
h (-a V dV d) A h VV d) ^ -w if < 0, where h denotes the hard constraint, which indicates the infinite weight. Using this transformation, we can decode the learned rules in terms of C to set of logical rules weighted MaxSAT formula.
5

---

Substituting ground truth rules into C. To validate the efficacy of our proposed maximum equality specification as viable interpretation for SATNet, we directly inject numan-written rules into the C matrix, bypassing the use of the clause matrix S. This substitution process involves transforming the ground truth rules into a Max2SAT formula and then converting it to the corresponding maximum equality formula. We perform experiments specifically on the parity function, as utilizing the S matrix directly in this case can lead to a trivial SDP formulation for SATNet. As expected, when given the ground truth rules to C, SATNet perfectly solves the parity function. This result serves as compelling evidence that the maximum equality formulation could effectively capture and express the logical rules inherent in the problem.
Learning a sparse C matrix in SATNet. It is also worth noting that our specification method would result in a weighted MaxSAT formula with approximately 3 ( clauses if is a dense matrix that contains no zero elements. For SATNet, C' = S S is always such a dense matrix. However, solving with such large number of clauses can be computationally expensive when invoking an exact solver for the weighted MaxSAT formula. To reduce the size of our decoded logical rules, we modify the implementation of SATNet learn the C. matrix directly and further apply the Iterative Hard Thresholding (IHT) algorithm
to sparsify it.
Specifically, during each training epoch, we employ thresholding function with a threshold to set some small magnitude elements in C' to zero, thereby inducing sparsity. By iteratively applying this thresholding procedure, we progressively obtain sparser representation of the learned rules, which helps to alleviate the computational burden when solving the weighted MaxSAT problem. The IHT algorithm strikes balance between the sparsity of C and the performance of SATNet, ensuring that the learned rules remain effective in capturing the underlying logical structure while achieving a more manageable size for the weighted MaxSAT formula. In practice, we can set the threshold to be a fraction (e.g., one-fifth) of the average absolute value of non-zero elements in C.
3.3 Incorporating Domain Knowledge
The interpretability of C' makes it feasible to incorporate domain knowledge in many flexible ways. One straightforward approach is to directly add symbolic constraints representing domain knowledge Ødomiin (e.g.. Sudoku puzzle constraint where each cell contains only one digit) to the weighted MaxSAT formula, Φc. which is derived from the learned matrix C. Although the feasibility of introducing domain knowledge in this way is obvious, the reliable interpretability of C' plays central role. Another less obvious but more interesting way to incorporate domain knowledge is to "compile" them into additive weights. That is, symbolic knowledge Pdomuin can be properly reduced into weights AC, which can be further added to C. In fact, it is not hard to show that these two ways essentially equivalent, i.e., Qdomain A &0 OC+AG- In Proposition] I we have shown that any propositional constraints (e.g., Odommin) can be reduced into maximum equality constraints (e.g.. AC), and this reduction guarantees that cDaomain = Φac- To prove the equivalence, we only need show the following property of encoding C into equivalent weighted MaxS AT constraints $c.
Proposition For any two matrices C₁ C2 representing maximum equality constraints, we have: éc, A ΦC2- = $ci+C2, where &c represents the weighted MaxSAT constraints reduced from C.
Proof. This proposition holds because of the following two properties of weighted MaxSAT con- straints: (1) (de- die-jduulicating hard constraints results in equivalent MaxSAT constraints; (2) weighted soft constraints can be split into multiple constraints (or merged into a single one) long as the total weight for each unique clause remains unchanged. Considering the matrices C₁ and C2 operate as weights of equality relations, which consequently become weights of the underlying MaxSAT constraints, and given that the reduction process ensures that original weights are preserved, we can conclude that the weight matrix C' can be split or/and merged without affecting equivalence.
The interchangeability between symbolic knowledge and the weights of C opens up many interesting interactions between these two different worlds. On one front, domain knowledge can be incorpo- rated into C' as the additive weights at various phases, from initialization and training to inference, improving the efficiency and robustness of SATNet. On the other hand, we can also decode the learned matrix C' to a set of symbolic constraints, where domain knowledge within propositional logical rules can be directly integrated. In this work, we focus on adding domain knowledge during the inference stage via both approaches.

---

3.4 Verifying Decoded Logical Rules
Once we have the decoded logical rules, the intuitive next step is to formally validate their "correctnes"" by comparing them with the human-wrine written rules (if available). However, verifying the correctness of a weighted MaxSAT formula based on ground truth expressed in a SAT formula poses inherent difficulties. This complexity stems from two challenges: (1) the lack of well-defined general equivalence between a SAT formula and a weighted MaxSAT formula, and (2) the potential presence of auxiliary variables in the learned weighted MaxSAT formula that are absent in the ground truth.
To address this issue, we introduce two equivalence definitions between weighted MaxSAT formula and a SAT formula, based on the concept of functional equivalence. At its core, we perceive SAT (or MaxSAT) solving as a function, with a partial assignment serving input, that yields an output, which represents a satisfying (or maximally satisfying) assignment. Informally, to be claimed equivalent, the two formulas should "agree" on all possible imput and output pairs. While the intuition behind functional equivalence might seem straightforward, special attention has to be taken into account. This is because SAT (or MTxSAT) solving may not be functional the output may not be unique or not even exist for given input. Taking Sudoku an illustrative example, if the number of input cells is too few, there may exist more than one solution to complete the puzzle; or if the given input cells already have conflicts, there is no way to complete the puzzle.
Here, we consider several formal equivalence definitions follows.
Definition 1 (Unique Functional Equivalence). For any partial assignment to the ground truth expressed in an SAT formula, if a satisfying output exists and is unique, the optimal solution of the weighted MaxSAT formula is also unique and corresponds to the same output (after projecting away auxiliary variables).
This definition considers functionally dependent input and output (IO) pairs and also suggests a simple enumeration- based method for checking whether the unique functional equivalence holds. We empirically find that such an enumeration- such as 4 x 4 Sudoku, which has around 85,000 functionally dependent IO pairs with minimal inputs. Definition 2 (General Functional Equivalence). For any partial assignments to the ground truth expressed in an SAT formula, if there exists satisfying output(s), the optimal solution(s) of the weighted MaxSAT correspond to a subset of the satisfying assignments of the SAT formula.
approach is sufficient for checking small puzzles
This equivalence definition is stricter than Definition ass it additionally constrains the solution space of the weighted MaxSAT formula when the output cannot be uniquely determined by the given input. In this scenario, exhaustively enumerating all possible IO pairs might become prohibitive, even for small puzzles like x 4 Sudoku. To address this challenge, we introduce a sufficient condition for proving general functional equivalence, which can be much more efficient to check compared to the enumeration-basee approaches.
Definition (Sufficient Condition for General Functional Equivalence). Given a weighted MaxSAT formula, if there exists a threshold 0 such that each of its assignments that results a weight greater (or less) than 0 is meanwhile a satisfiable (or unsatisfiable) solution to an SAT formula, then the general functional equivalence between the two formulas must hold.
This sufficient condition has limitation in that may not always exist for certain weight MaxSAT formulas even if they are functionally equivalent to the ground-truth rules. However, we empirically find that incorporating domain knowledge could often help to make the decoded logical rules meet such a sufficient condition, thereby successfully establishing general functional equivalence.
4 Experiments
We present the evaluation results in this section. We test our proposed framework on the tasks of stream transformations and Sudoku puzzles. We train both original SATNet (32) and our modified version SATNet* to learn the underlying logical rules in the data and decode them into a weighted MaxSAT formula using our specification approach. Given the generated rules, we utilize Gurobi [I3] for exact inference and use the state-of-the-art MaxSAT solver MASHA [66 for verification. All experiments are carried out on single RTX8000 GPU and 16 CPU cores across 100 epochs, using the Adam optimizer with learning rate of 10-3 3, All other hyperparameters are also set the same as in the paper (32].
7

---

4.1 Stream Transformations
Experiment setup. In this experiment, we evaluate our proposed framework on three stream transformation tasks, i.e. the parity function, binary bit addition, and symbol counting. The parity function is the chained XOR of an input 0-1 stream. Following SATNet (32), we set the length of the input stream to 20 and 40 and generate a dataset of 10, 000 examples for each length. The binary bit addition task aims to calculate the sum of two binary strings with the corresponding carry bit. We set the input length to 10, 20, and 30 and randomly sample 4, 000 instances for each length. The symbol counting adds the occurrence number N of one specific symbol (e.g., bit 1) of one stream and computes N modulo k. The input stream has length of 40, and we explore different values of k, namely 2, 4, 8, and 16. For each value of k, we randomly generate a dataset comprising 1, 000 samples. For all these datasets, we split them into training/testing sets with 90% /10% proportions.
Results. On all three datasets, both SATNet and SATNet* can learn the underlying logical rules in the data perfectly, solving all testing instances. Since valid (partial) input spaces for these tasks are relatively small and can be efficiently enumerated, we verify the decoded rules with the ground truth using the general functional equivalence. As expected, given any partial input, the optimal solutions of our decoded weighted MaxSAT formula align with the satisfying assignments in the ground truth rules. This result shows that our decoded rules from the matrix C' are verifiably reliable.
4.2 Sudoku Puzzles
Experiment Setup. In this experiment, we evaluate the performance of our approach on Sudoku puzzles of varying board sizes: 4 x and 9 x 9. For the x 4 Sudoku puzzles, we construct a dataset by enumerating all possible puzzles that have a unique solution with minimal inputs, resulting in total of 85,632 puzzles. To ensure proper evaluation, we split this dataset into training and testing sets with ratio of 9:1. For the 9 x 9 Sudoku puzzles, use the same dataset in SATNet (32) consisting of 9,000 instances for training and 1,000 instances for testing. It is also noteworthy that the original experiment in SATNet implicitly enforces that each group of variables corresponding to the same cell has exactly one value of during inference. However, our experiments discard these constraints and instead round all variable values based threshold for both SATNet and SATNer*
Results. On the x 4 Sudoku dataset, both SATNet and SATNet exhibit remarkable performance, achieving testing accuracies of 99.89% and 99.90%. Notably, the learned C' matrix in SATNet* is much sparser than that in SATNet, containing approximately 53% zero elements. On the other hand, when leveraging Gurobi to solve the weighted MaxSAT formulas derived from SATNet and SATNet" we can achieve perfect accuracy on the testing set. To further validate the robustness of our decoded rules, we consider the unique functional equivalence between decoded MaxSAT formula and the human-written rules and successfully verify such a functional equivalence. This result demonstrates that our decoded logical rules are highly reliable, despite originating from SATNet and SATNer* which inherently involves some errors during the approximate solving process.
Furthermore, we conduct experiments to add domain knowledge into our framework during inference. Specifically, by incorporating the partial Sudoku constraints (one cell cannot contain more than one digit) to our decoded weighted MaxSAT formula, we are able to efficiently verify that our augmented logical rules satisfy the sufficient condition for general functional equivalence with the ground truth rules. Alternatielyy, if we integrate this knowledge into the weight matrix C a' a "weight repair", SATNet* can also successfully solve all Sudoku puzzles in the testing set, rectifying the previously failed cases. These results demonstrate the flexibility and adaptability of our approach when incorporating additional symbolic knowledge.
On the 9 x 9 Sudoku dataset, SATNet achieves a testing accuracy of 88.30% and decodes into a weighted MaxSAT formula with hundreds of thousands of clauses [] Given the enormous size of the decoded rules, both Gurobi and CASHWMaxSAT fail to verify or find counterexample in hours. Therefore, in this case, we only compare the weight of the failed predictions against the ground truth one (with the same assignments of auxiliary variables). Our results show that the wrong predictions always have strictly lower weights than the ground truth ones, demonstrating that the mistakes of SATNet are due to the suboptimal solutions according to decoded weighted MT formula.
We also experiment with SATNer but find its convergence rate is slower than that of SATNet in 100 epochs and the resulted number of clauses is still in the hundreds of thousands. As such, we use SATNet in this scenario.
8

---

5 Related Work
Differentiable learning of logical rules. Our work is closely related to recent research that focuses on learning underlying logical rules from data in end-to-end manner, without relying on pre- specified rule templates. Several approaches [ 32 6 21 28 formalize the task of learning logical rules constrained optimization procedure, using different relaxations logical operators to solve it. For example, OptNet [ models the problem as quadratic program and learns 4 x Sudoku rules from input-output games, while SATNet (32] and its variant [T8 apply differentiable SDP relaxations to solve 9 x 9 Sudoku puzzles and Rubik's cube. Some alternative works [2 27 9 37 view the rule learning process as a black box and utilize neural networks as function approximators to learn logical rules. These efforts include Neural Logic Machines [9]. which uses simple multi-layer perceptrons to recover lifted rules in first-order logic, and Recurrent Transformers (37), which employs an extended version of transformers to solve both textual and visual Sudoku puzzles [ 29] However, all these attempts embed the learned rules into weights of neural networks, failing to give human-readable interpretations and making them infeasible for verification. To our best knowledge, our proposed framework is the first attempt decode a set of interpretable logic structures through differentiable learning, and formally verify their functional correctness.
Differentiable logic programming. Logic programming [9] is programming paradigm that expresses facts and rules about problems within system of formal logic. Recently, there have been tremendous efforts to combine neural networks with logic programming, enabling neural networks
to generate explicit logical programs from examples. A line of research 25
10,
14
26 35
augments inductive logic programming (ILP) [22] with neural networks. For instance, Neural LP 34
learns first-order logical rules for knowledge base reasoning, while ØILP [T0] generalizes ILP to learn robust rules from noisy data. Besides ILP, some approaches integrate neural networks with other types of logic programming: DeepProbLog 20 extends Problog (24] by learning the weights for each probabilistic logical rule, ABL (8 and NeuroLog 300 entangle abductive logic programming [T5] with machine learning models through gradient-descen based optimization, and NeurASP [6 applies a similar idea to answer set programming 177. While the integration of logic programming with neural networks has shown promise in deriving interpretable logical rules, a common challenge in these approaches is the reliance predefined rule templates. This requirement often necessitates significant expertise and careful design, making it a highly non-trivial task. In contrast, our proposed framework climinates the need for such templates, offering more flexible and efficient approach to learning interpretable logical rules from data.
6 Discussions
Limitations and future work. There are a few limitations to our proposed framework. Firstly, our current framework builds on SATNet, which is limited learning propositional logical rules and cannot handle rules in first-order or higher-order logic. Additionally, if SATNet fails to capture the underlying logic structures in the data, our decoded rules may be incorrect and unreliable. Secondly, given the number of variables n. our approach may result in a weighted MaxSAT formula with O (n²²) con-cmnnu inference processes, especially
clauses the worst case. This can potentially lead when utilizing an exact solver for large values of n in practical scenarios. We would like to expand our approach to support more expressive rule representations and explore alternative optimization approaches to reduce the size of our learned logical rules as future work.
Conclusion. In this work, we present a novel framework for extracting interpretable logical rules from the Iearned weights in SATNet. We demonstrate, both empirically and theoretically, that the original formulation in SATNet lacks clear interpretability. To address this, we introduce maximum equality specification, which enables the interchangeability between the weights of SATNet and a set of logical rules in the weighted MaxSAT form, as well as the flexible integration with domain knowledge. To verify the correctness of our decoded formula, we introduce multiple verification approaches that compare the solution space of our generated rules with the ground truth. Experimental evaluations conducted on the stream transformations and Sudoku puzzles demonstrate that the rules generated by our framework are highly accurate and formally verifiable. We hope our approach will lay the groundwork for bridging deep learning and interpretable rule learning and stimulate further innovation in this exciting field.

---

Acknowledgments and Disclosure of Funding
We thank the anonymous reviewers for their insightful comments. This work was supported, in part, by Individual Discovery Grants from the Natural Sciences and Engineering Research Council of Canada, and the Canada CIFAR AI Chair Program.
References
[1] Brandon Amos and J. Zico Kolter. Optnet: Differentiable optimization as a layer in neural networks. In International Conference Machine Learning (ICML), 2017.
[2] Peter W. Battaglia, Razvan Pascanu, Matthew Lai, Danilo Jimenez Rezende, and Koray Kavukcuoglu, Interaction networks for learning about objects, relations and physics. In Advances in Neural Information Processing Systems (NeurIPS), 2016.
[3] Mathieu Blondel, Olivier Teboul, Quentin Berthet, and Josip Djolonga. Fast differentiable sorting and ranking. In International Conference on Machine Learning (ICML), 2020.
[4] Thomas Blumensath and Mike E Davies. Iterative hard thresholding for compressed sensing. Applied and Computational Harmonic Analysis, 2009.
[5] Oscar Chang, Lampros Flokas, Hod Lipson, and Michael Spranger. Assessing satnet's ability to solve the symbol grounding problem. In Advances in Neural information Processing Systems (NeurIPS), 2020.
[6] Nuri Cingillioglu and Alessandra Russo. Deeplogic: Towards end-to-end differentiable logical reasoning. In AAAI 2019 Spring Symposium on Combining Machine Learning with Knowledge Engineering (AAAI-MAKE), 2019.
[7] Robert Crandall, Bin Dong, and Ali Bilgin. Randomized iterative hard thresholding for sparse approximations. In Data Compression Conference, (DCC), 2014.
[8] Wang-Zhou Dai, Qiu-Ling Xu, Yang Yu, and Zhi-Hua Zhou. Bridging machine learning and logical reasoning by abductive learning. In Advances in Neural Information Processing Systems (NeurIPS), 2019.
[9] Honghua Dong, Jiayuan Mao, Tian Lin, Chong Wang, Lihong Li, and Denny Zhou. Neural logic machines. In International Conference on Learning Representations (ICLR), 2019.
[10] Richard Evans and Edward Grefenstette. Learning explanatory rules from noisy data. Journal of Artificial Intelligence Research, 2018.
[11] M. R. Garey, David S. Johnson, and Larry J. Stockmeyer. Some simplified np-complete graph problems, Annual ACM Symposium on Theory of Computing (STOC), 1976.
[12] Michel X. Goemans and David P. Williamson. Improved approximation algorithms for max- imum cut and satisfiability problems using semidefinite programming. Journal of the ACM (JACM), 1995.
[13] Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2023.
[14] Zhengyao Jiang and Shan Luo. Neural logic reinforcement learning. In International Conference on Machine Learning (ICML), 2019.
[15] Antonis C Kakas, Robert A. Kowalski, and Francesca Toni. Abductive logic programming. Journal of Logic and Computation, 1992.
[16] Zhendong Lei, Shaowei Cai, Dongxu Wang. Yongrong Peng, Fei Geng, Dongdong Wan, Yiping Deng, and Pinyan Lu. Cashwmaxsat: Solver description. MaxSAT Evaluation, 2021.
[17] Vladimir Lifschitz. What answer set programming? AAAI Conference on Artificial Intelligence (AAAI), 2008.
10

---

[18] Sangho Lim, Eun Eun-Gyeol Oh, and Hongseok Yang. Learning symmetric rules with satnet. In Advances Neural Information Processing Systems (NeurIPS). 2022.
[19] John W. Lloyd. Foundations of Logic Programming. 2nd Edition. Springer, 1987.
[20] Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester, and Luc De Raedt. Deepproblog: Neural probabilistic logic programming. In Advances in Neural Informa- fion Processing Systems (NeurlPS), 2018.
[21] Tao Meng and Kai-Wei Chang. An integer linear programming framework for mining constraints from data. In International Conference on Machine Learning (ICML), 2021.
[22] Stephen Muggleton. Inductive logic programming. New Generation Computing, 1991.
[23] Rasmus Palm, UIrich Paquet, and Ole Winther. Recurrent relational networks. Advances in Neural Information Processing Systems (NewrIPS), 2018.
[24] Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. Problog: A probabilistic prolog and its application in link discovery. In International Joint Conference Artificial Intelligence (IJCAI), 2007.
[25] Tim Rocktäschel and Sehastian Riedel. End-to-end differentiable proving. In Advances in Neural Information Processing Systems (NeurIPS), 2017.
[26] Ali Sadeghian, Mohammadreza Armandpour, Patrick Ding, and Daisy Zhe Wang, DRUM: end-to-end differentiable rule mining on knowledge graphs. Advances in Neural Information Processing Systems (NeurIPS), 2019.
[27] Adam Santoro, David Raposo, David G. Barrett, Mateusz Malinowski, Razvan Pascanu, Peter W. Battaglia, and Tim Lillierap. A simple neural network module for relational reasoning. In Advances in Neural Information Processing Systems (NeurIPS), 2017.
[28] Mokanarangan Thayaparan, Marco Valentino, Deborah Ferreira, Julia Rozanova, and André Freitas. Diff-explainer: Differentiable convex optimization for explainable multi-hop inference. Transactions of the Association for Computational Linguistics, 2022.
[29] Sever Topan, David Rolnick, and Xujie Si. Techniques for symbol grounding with satnet. In Advances in Neural Information Processing Systems (NeurIPS), 2021.
[30] Efthymia Tsamoura, Timothy M. Hospedales, and Loizos Michael. Neural-symbolic integration: compositional perspective. In AAAI Conference on Artificial Intelligence (AAAI), 2021.
[31] Po-Wei Wang, Wei-Cheng Chang, and Zico Kolter. The mixing method: low-rank co- ordinate descent for semidefinite programming with diagonal constraints. arXiv preprint 17Xiv: 2017.
[32] Re-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter. Satnet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. In International Conference on Machine Learning (ICML). 2019.
[33] Po-Wei Wang and J. Zico Kolter. Low-rank semidefinite programming for the MAX2SAT problem. AAAI Conference on Artificial Intelligence (AAAI), 2019.
[34] Fan Yang, Zhilin Yang, and William W Cohen. Differentiable learning of logical rules for knowledge base reasoning. Advances in Neural Information Processing Systems (NeurIPS), 2017.
[35] Yuan Yang and Le Song. Learn explain efficiently via neural logic inductive learning. In International Conference on Learning Representations (ICLR), 2020.
[36] Zhun Yang, Adam Ishay, and Joohyung Lee. Neurasp: Embracing neural networks into answer set programming. In International Joint Conference Artificial Intelligence (IJCAI), 2020.
[37] Zhun Yang, Adam Ishay, and Joohyung Lee. Learning solve constraint satisfaction problems with recurrent transformer. In International Conference on Learning Representations (ICLR), 2023.


Reviews:
[{"review_id": "nhOz5RyFf1", "reviewer": "Reviewer_ASVp", "summary": "The work investigates the problem of generating interpretable and verifiable logical rules through differential learning. Specifically,  a deep network layer for satisfiability solving (SATNet) in a differentiable maximum satisfiability (MAXSAT) solver that learns logical rules from input-output examples was used. Through experiments, the authors claim that the learned weights in SATNet lack explainability. To address this issue, a method called maximum equality is proposed to interpretate the weights of SATNet into a set of propositional logical rules. Stream transformations and Sudoku problems were taken as the tasks to evaluate the method.\n\nPost rebuttal: I have read the authors' rebuttal and I appreciate the authors' effort in addressing my concerns. I agree with the authors' point on interpretable logical rules in the rebuttal. My concerns on the application of the proposed methods to models beyond SATNet and other more complex tasks still hold.", "questions": "-Would it be feasible to use a deep neural network to interpret S of SATNet?\n-Is c_{ij} predefined or learnable?\n-How is an appropriate value set for n_a?\n-The visual Sudoku problem was used in the SATNet work, have you tested your maximum equality method on this task as well?", "limitations": "The authors have mentioned the limitation of this work in only learning propositional logical rules and not being able to handle rules in first-order or higher-order logic.", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "+The work proposes a method called maximum equality to interpretate the weights of SATNet into a set of propositional logical rules to improve the explainability of SATNet.\n+The method was evaluated on the Stream transformations and Sudoku tasks and the results show that decoded rules from the maximum equality method are better than the ones out of the original SATNet.\n+To a certain extent, it improves the explainability of learned logical rules from input-output examples.", "weaknesses": "-The work builds upon a specific satisfiability solving method (SATNet), which limits the impact of the work.\n-It is claimed that the lack of interpretation of SATNet was due to that the clause matrixS is not enforced as ternary and a method of rounding S to a ternary matrix didn't yield correct logical rules. However, it would be interesting to investigate how to interpretate S through a learnable network or another approach.\n-The matrix C = S^T S is decomposed, and the objective of maximum equality is to minimize the similarity between each pair of variable vectors of S. A weight c_{ij} is associated with the similarity between each pair of variable vectors. It is not clear how c_{ij} will affect the generated logical rules.\n-The work relies on the prior work SATNet and a few terms are not explained, which hinders understanding the work. For example, SATNet -   satisfiability solving network; MaxSAT - maximum satisfiability (MAXSAT) solver.\n-In Eq. 2 and Eq. 3, mimimize -> minimize", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for your comments and feedback. In the following, we will address your questions point by point.\n\n> The work builds upon a specific satisfiability solving method (SATNet), which limits the impact of the work. \n\nIndeed, SATNet is an award-winning architecture (ICML 2019 Best paper Honorable mention) that achieves state-of-the-art performance for learning *neural representations* of logical rules from data without using specified rule templates. While our approach builds upon SATNet, it is important to highlight that our work represents the *first* contribution in the logical rule learning/logic programming field, enabling the learning of *interpretable* and *verifiable* logical rules directly from data without any prior rule templates. By focusing on interpretability, our work expands the potential applications of differential logical rule learning that requires the transparent solving process and provides a novel perspective in this domain.\n\n> It would be interesting to investigate how to interpret $S$ through a learnable network or another approach / Would it be feasible to use a deep neural network to interpret $S$ of SATNet?\n\nYou raise an interesting point about interpreting the $S$ matrix through a learnable network. However, it is essential to clarify that interpretable logical rules aim to be human-readable, enabling white-box problem-solving processes. While neural networks themselves are challenging to interpret, decoding reliable human-readable rules directly from the $S$ matrix using neural networks becomes even more complex. To our best knowledge, there is no existing learnable approach that can reliably interpret $S$ to generate a set of logical rules in an interpretable form. Our approach naturally aligns with the optimization process of SATNet and enables the *interchangeability* between weights and propositional logical rules, providing a viable and effective solution for decoding a set of interpretable rules.\n\n> It is not clear how $c_{ij}$ will affect the generated logical rules / Is $c_{ij}$ predefined or learnable?\n\nIn SATNet*, the only learnable parameter is the $C$ matrix, which is fully learned from the data. Each element $c_{ij}$ contributes to the weights in our maximum equality formulation.\n\n> The work relies on the prior work SATNet and a few terms are not explained, which hinders understanding the work.\n\nThanks for pointing out this issue and our typos. In the revised version of our paper, we will provide a comprehensive explanation of SATNet and clarify all relevant terms to ensure a better understanding for readers.\n\n> How is an appropriate value set for n_a?\n\nThe value of $n_a$ is set differently for various problems. Generally, $n_a$ can be chosen around the number of defined variables ($n$). In our experiments, we set $n_a$ to the same value as the original SATNet paper to ensure a fair comparison.\n\n> The visual Sudoku problem was used in the SATNet work, have you tested your maximum equality method on this task as well?\n\nThanks for the suggestions. We conduct additional experiments on 4 $\\times$ 4 visual Sudoku datasets. Similar to the non-visual setting, using SATNet and SATNet* alone could achieve a solving accuracy of 99.83\\% and 99.28\\% respectively, whereas using exact solver Gurobi on our decoded rules could achieve 100\\% accuracy. Moreover, we further verify that the decoded rules in this setting satisfy the *unique functional equivalence* as well."}, {"review_id": "lC7OpTNz5b", "reviewer": "Reviewer_un3V", "summary": "This paper builds on SATNet, a differentiable MaxSMT solver that was proposed in the past to learn logical rules from input-output examples. SANet is based on a \"low rank semidefinite programming approach\" and uses a learnable matrix S to capture the logical rules. SATNet was shown to learn to solve e.g. Sudoku puzzles with near perfect accuracy. The problem addressed in this paper is that the S matrix and the learned weights in SATNet lack a clear, logical meaning. The authors first describe a set of (failed) experiments that aim to extract the meaning from S. Then they describe a new formulation called maximum equality which enables them to formulate MaxSMT formulas that can be solved with off-the-shelf solvers. The authors demonstrate both theoretically and empirically that this new formulation indeed captures the underlying logical rules; it also opens up the possibility of new applications, such as adding domain specific constraints to a problem", "questions": "none", "limitations": "The paper describes carefully the limitations of the proposed approach.", "rating": 7, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "* The paper is very well written. It provides a gentle introduction to teh problem and a clear running example to illustrate the technique.\n* The paper makes a clear contribution over the previous SATNet approach.The proposed approach is very interesting and has many practical applications.\n* The novelty is not only in the \"decoding\" but also in teh functional comparison between the decoded rules and teh ground truth.", "weaknesses": "none", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks a lot for your positive comments and feedback! If you have further questions, we are happy to answer them!"}, {"review_id": "V8HXQjjjAw", "reviewer": "Reviewer_cdcd", "summary": "The authors show that interpreting the SATNet model is not reliable. They reformulate the SATNet objective to a 'maximum equality specification' on matrix $C$. Assuming $C$ is ternary instead of continuous, the objective can be interpreted as a MaxSat problem. This problem can then be verified. Furthermore, the new objective is amenable to injecting symbolic background knowledge.\n\nPost rebuttal: I appreciate in-depth responses of the authors. I will keep my score.", "questions": "- Limitations of $S$ (p4, 145-155): The matrix given does not represent parity / XOR. I think coordinate (3, 4) should be a -1 (ie the last row is -1 -1 -1). Otherwise the (correct) input $110$ is rejected. On this corrected matrix $S$, I computed $S^T S$ and did not get a zero matrix as claimed but a diagonal matrix ($4 I$ in particular). This is not due to the correction, as $S_\\top^T S_\\top = 4$, so coordinate (1, 1) is necessarily 4.\n- Same part: The claim is that since $S^T S$ collapses, SATNet cannot theoretically represent a range of logical rules. I think this claim should be made a bit stronger: What (I think) you want to show is that two non-semantically equivalent CNF formulas map to the same $S^T S$. For instance, is there another problem than parity for which $S^T S$ equals $4 I$? \n- Have you tried interpreting the matrix $S$ instead when using the sparsification procedure? Instead of the MaxSAT procedure? Would that be worse than the MaxSAT interpretation? \n- Experiments: What exactly makes SATNet* different from SATNet? The sparsification?\n- 348: Why is SATNet* not evaluated on 9x9 sudokus?", "limitations": "While the authors developed a sparsification method, the MaxSAT problem will likely be huge and hard to interpret or verify. The verification part of this limitation is mentioned, not the interpretability. \n\nThe verification method amounts to enumerating IO Pairs. I would have hoped the interpretable rules would allow symbolic reasoning to prove equivalence. The authors argue this is impossible because it would require a transformation of SAT into MaxSAT (or vice-versa).", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 4, "contribution": 3, "strengths": "The paper is well-written and easy to follow. The structure is excellent, interleaving some experiments to motivate some choices. The problem of interpretability of learned rules is important and often overlooked in these logic-inspired architectures. I do not believe SATNet has been studied in this context before. \nThe paper presents interesting failure cases of SATNet. The symbolic background knowledge injection through compiling inside matrix $C$ is a very useful result, increasing the model's applicability.", "weaknesses": "I have some questions about the theoretical ideas presented in the paper, particularly on the limitations of SATNet. The experiments are somewhat simple and could be presented more clearly or on more tasks (for instance, on ILP benchmarks like in $\\partial$ILP [1]). \n\n- The experiments could be a lot clearer with a table for the different tasks and the different evaluations. Ie, Compare SATNet and SATNet* as a continuous model and in the MaxSAT version. \n- The benefits of the maximum equality specification for interpretability are not entirely apparent to me (see questions).\n\n[1] Evans, R., & Grefenstette, E. (2018). Learning explanatory rules from noisy data. Journal of Artificial Intelligence Research, 61, 1-64.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the detailed and in-depth comments and questions! In the following, we hope to address the stated weaknesses and questions of our paper.\n\n> The experiments are somewhat simple and could be presented more clearly or on more tasks like ILP benchmarks in $\\partial$ILP.\n\nWe want to clarify that the setting of SATNet is quite different than that in ILP: SATNet aims to learn propositional logical rules directly from data without any predefined rules, while ILP requires background knowledge and predefined rules (or templates). Thus, applying SATNet to ILP tasks might not be fair for comparison due to the contrasting problem settings.\n\n> Limitations of $S$ / The claim that SATNet cannot theoretically represent a range of logical rules.\n\nWe apologize for the typos in our paper and appreciate your attention to detail. The last row in the ground truth rules should be (-1, -1, -1), and the corresponding matrix $C = S^TS = 4 I$. However, what we are particularly concerned about are the off-diagonal elements in the matrix $C$. Due to the SDP formulation of SATNet, its optimization is not affected by the diagonal elements of $C$, as the calculations associated with these diagonal elements lead to constants (specifically, $v_i^Tv_i$ = 1). When all the off-diagonal elements of $S^TS$ are zero, the SDP becomes trivial, and SATNet fails to capture any meaningful logical rules. This issue also exhibits in other symmetric rules like $(\\neg x \\lor y) \\land (x \\lor \\neg y)$. In our revision, we will provide a more detailed explanation of this aspect to enhance clarity.\n\n> Have you tried interpreting the matrix instead when using the sparsification procedure?\n\nWe initially attempted several regularization methods to enforce $S$ to be a ternary matrix during the training process, but unfortunately, these approaches did not yield successful results.\n\n> What exactly makes SATNet* different from SATNet? The sparsification?\n\nWe want to first emphasize that SATNet* and SATNet can be both used to learn rules from data and our specification methods (with exact inference) and verification methods can be applied to both of them. Here are two main technical differences between SATNet* and SATNet:\n\n* Learning procedure: SATNet learns the $S$ matrix, while SATNet* considers the $C$ matrix as the parameters and directly learns the weights of $C$. This distinction leads to a reduction in both the number of parameters and hyperparameters in our model. Specifically, $S \\in \\mathbb{R}^{m \\times n}$ and $C \\in \\mathbb{R}^{n \\times n}$, where $n$ is the number of variables (including the auxiliary variables), and $m$ is the number of clauses. In many cases, $m > n$, which means that SATNet* may have fewer parameters than SATNet. Moreover, when setting hyperparameters, SATNet considers the number of clauses and auxiliary variables, while SATNet* only considers the number of auxiliary variables. This makes SATNet* a more convenient and practical choice for real-world applications.\n\n* The Sparsification: The sparsification technique is another key distinction. It strikes a balance between the expressivity and the size of the learned logical rules. By employing sparsification, SATNet* can reduce the size of decoded logical rules in some cases, which in turn accelerates exact inference using Gurobi (with more than 10$\\times$ speed up).\n\n> Why is SATNet* not evaluated on 9 $\\times$ 9 sudokus?\n\nWe did attempt to use SATNet* on 9 $\\times$ 9 sudokus; however, the convergence rate of SATNet* was slower than SATNet in 100 epochs. Although SATNet* could indeed reduce the size of decoded logical rules, the number of clauses is still in the hundreds of thousands. As a result, we chose to use SATNet instead for $9 \\times 9$ Sudokus. Besides 9 $\\times$ 9 Sudoku datasets, we find that SATNet* could converge as quickly as SATNet and could effectively reduce the size of decoded rules."}, {"review_id": "wq03YqaT7c", "reviewer": "Reviewer_sq5Z", "summary": "This paper builds on the SATNet framework on MaxSAT problems, adds an interpretation method that allows the conversion between its weight and propositional logical rules. Effective verification methods are proposed to see if the decoded rules from SATNet are functionally equivalent to the ground truth. Experiments on stream transformation and Sudoku problems show that the decoded \"hard\" logical rules achieve better performance than SATNet itself. The logical rules are verified to be equivalent to the ground truth.", "questions": "What challenges do you foresee when extending this work to more expressive logics like FOL and HOL, apart from the scaling issues mentioned in the discussions section? Are there fundamental bottlenecks to this? I would like to see more discussions on this, as propositional logic seems slightly limiting.", "limitations": "The authors addressed the limitations and scoped the work well.", "rating": 8, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "- The proposed interpretation method is well motivated and grounded theoretically.\n- The proposed interpretation method allows for the integration of symbolic knowledge as additive weights, which is flexible for the injection of human domain knowledge.\n- The verification methods are sound and have been practised on the experimental tasks of stream transformations and Sudoku.\n- The paper is well-written.\n- The decoded logical rules outperform SATNet on the experimental tasks, showing its practical effectiveness.\n\nOverall, it's a solid contribution to the interpretability of deep learning and neuro-symbolic computation communities.", "weaknesses": "For the machine learning readers, perhaps the authors can give a bit more elaboration when propositions are stated. A couple of worked examples can also help the reader understand a lot better. ", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks a lot for your positive review and valuable feedback! We would elaborate on our propositions in our revision. In this response, we discuss the challenges we anticipate when extending our work to more expressive logic like FOL and HOL:\n\n* Representing logic rules in FOL/HOL using a simple matrix form and formulating the entire procedure as a clear mathematical optimization becomes challenging. Unlike propositional rules, these logics involve more complex structures (especially with quantifiers) that are difficult to encapsulate within a continuous optimization framework. To extend our work to more expressive logic, we anticipate the need for innovative approaches that incorporate efficient *quantifier elimination* as well as *lifted inference* techniques into the differentiable optimization process.\n\n* FOL/HOL entails a significantly larger rule space compared to propositional logic, making it difficult to learn from data *without predefined constraints*. The expanded search space poses challenges in identifying meaningful and interpretable rules from the vast possibilities. Addressing this challenge may involve developing a domain-specific language (DSL) / meta rules to limit the rule space.\n\n* Verifying the learned rules against ground truth rules in FOL/HOL is not straightforward. Due to the inherent complexity of these logics, the design of the verification process requires more careful consideration. Proving the equivalence of two FOL/HOL logical rules may necessitate the use of theorem provers (e.g., Coq), which requires considerable expertise. Beyond scalability, automating the verification process presents another challenge.\n\nFor example, one potential future work is to explore building specification/interpretation methods on the top of Neural Logic Machines (NLM) [1], which focuses on learning FOL rules with only nullary, unary, and binary predicates from data. However, unlike SATNet, which stores learned rules in a single $S$ (or $C$) matrix, NLM stores rules in the weights of neural networks (several MLPs). The optimization objective in NLM is not as straightforward as SATNet's, which can be expressed as a SDP. Additionally, interpreting MLPs is more challenging than interpreting a matrix alone. To decode interpretable rules from NLM, one may explore replacing MLPs with learnable matrices and transforming the entire neural architecture into a clear mathematical optimization form. By doing so, our similar specification methods may be applied to the revised NLM to derive interpretable rules effectively.\n\n[1] Dong, Honghua, et al. \"Neural Logic Machines.\" In International Conference on Learning Representations (ICLR), 2019"}, {"review_id": "YAeZefE9iJ", "reviewer": "Reviewer_fiQw", "summary": "The authors propose a new framework to generate interpretable and verifiable logical rules through differentiable learning. The framework is built upon SATNet, but the paper proposes a new interpretation method called maximum equality to decode the weights of SATNet into logical rules. The paper also proposes several verification methods to validate the decoded rules against ground truth rules. Experiments show that the decoded rules are highly reliable and functionally equivalent to the ground truth rules.", "questions": "- The paper mentions that the thresholding function was set to be approximately one-fifth of the average absolute value of non-zero elements in C. How was this decided, and how sensitive is the performance relative to the chosen threshold? It would be nice to see a graph of this.", "limitations": "The limitations section was well-written. If possible, I'd like to see an extended discussion of future work (perhaps in the Appendix), so the authors can provide useful directions for future research.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The impressive contribution of this paper is to distill the black box weights of a differentiable logic program like SATNet into human interpretable rules (boolean expressions) that can be verified.\n- Moreover, while the initial SATNet itself fails to achieve 100% test accuracy, the decoded interpretable rules manage to achieve perfect 100% test accuracy. This is remarkable because in the realm of logical reasoning, true generalization is a binary outcome: either the logical rules have truly been learned or they have not. In this paper, they show that they indeed have been learned, and verifiably so.", "weaknesses": "- A major caveat to this work is that the 100% test accuracy was achieved by adding symbolic constraints that represent domain knowledge (e.g. rules of Sudoku). However, this is not necessarily a weakness, because incorporating domain knowledge is a useful thing to do in general, and it's great that the authors propose a recipe for doing so.\n- It would be nice to see the authors apply their technique to visual Sudoku. That was one of the hallmark contributions of the original SATNet paper that learned to play Sudoku by looking at images of digits.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the positive feedback and comments! In the following, please let us address your raised concerns and questions.\n\n> The 100% test accuracy was achieved by adding symbolic constraints that represent domain knowledge (e.g. rules of Sudoku).\n\nWe want to clarify that our approach could achieve 100% accuracy *without* adding any additional constraints on the 4 $\\times$ 4 Sudoku dataset when employing the exact solver Gurobi on our decoded logical rules, and we can also verify the decoded rules satisfy the *unique functional equivalence* with the ground truth rules. Given the vast input space of 4 $\\times$ 4 Sudoku puzzles, exhaustively enumerating all IO pairs for *general functional equivalence* verification is infeasible. Instead, we discover that by incorporating *partial* Sudoku rules (e.g., the constraints that each cell can only contain one digit) into our decoded rule sets, we can efficiently verify that our logical rules satisfy *the sufficient condition* for general functional equivalence. Furthermore, in practical real-world scenarios, we acknowledge the potential benefit of utilizing *partial* domain knowledge/commonsense knowledge (as prior symbolic constraints). By applying our approach to learn interpretable rules from data and subsequently adding this domain knowledge into our rule sets, we can further enhance the reliability of our decoded logical rules. This adaptability to integrate domain-specific information makes our approach more versatile and suitable for real-world applications.\n\n> It would be nice to see the authors apply their technique to visual Sudoku.\n\nThanks for the suggestions. We conduct additional experiments on 4 $\\times$ 4 visual Sudoku datasets. Similar to the non-visual setting, using SATNet and SATNet* alone could achieve a solving accuracy of 99.83\\% and 99.28\\% respectively, whereas using exact solver Gurobi on our decoded rules could achieve 100\\% accuracy. Moreover, we further verify that the decoded rules in this setting satisfy the *unique functional equivalence* as well.\n\n> How was the threshold function for sparsity decided, and how sensitive is the performance relative to the chosen threshold?\n\nThe threshold function we design is based on our empirical evaluation. During our experiments, we observe that the expressivity of the decoded rules remains relatively stable across different threshold values. To validate this further, we conduct additional experiments using various threshold values for SATNet* on the 4 × 4 Sudoku dataset. The results are summarized below (denoting the average nonzero elements of $C$ as $\\mu$):\n\n| threshold | Sparsity | Solving Accuracy with Gurobi | Solving Time with Gurobi (per instance)|\n| :-: | :-: | :-: | :-: |\n| 0.05 $\\mu$ | 0.12 | 100\\% | 4.37s |\n| 0.10 $\\mu$ | 0.15 | 100\\% | 3.91s |\n| 0.20 $\\mu$ | 0.53 | 100\\% | 0.92s |\n| 0.25 $\\mu$ | 0.53 | 100\\% | 0.93s |\n| 0.50 $\\mu$ | 0.57 | 100\\% | 0.66s |\n| 0.60 $\\mu$ | 0.74 | 100\\% | 0.37s |\n\n> More discussion on future work.\n\nWe further discuss one possible way to improve our work as future work. As stated in our paper, our approach may result in a weighted MaxSAT formula with $O(n^2)$ clauses in the worst case. One promising avenue for improving our approach is to address the challenge of learning lifted rules. By effectively learning and incorporating lifted rules into the model, we can significantly reduce the size of the resulting rule sets. For example, representing concepts such as rows, columns, and $3 \\times 3$ squares on the Sudoku board as variables would allow us to capture more concise and interpretable rules. Accomplishing this involves developing a domain-specific language (DSL) that efficiently represents a wide range of logical rules. The designed DSL would enable the lifting process, allowing SATNet to learn and leverage high-level concepts and relationships, leading to improved performance and compact decoded rule sets. "}]

Author rebuttal:

Meta-review: This paper aims to improve the interpretability of SATNet by directly learning the matrix $C=S^T S$ rather than $S$ directly, transforming the learned matrix $C$ into a weighted MaxSAT formula, and then using an exact solver on the weighted MaxSAT formula during inference (optionally with additional domain knowledge incorporated). The reviewers felt that the proposed method was interesting and valuable in providing an interpretable representation of learned SATNet rules, that the intermediate experimental results were well-chosen to validate design choices, and that the evaluation on the 4 $\times$ 4 Sudoku experiment was convincing. The reviewers would have appreciated additional discussion on why the proposed method does not currently scale to 9 $\times$ 9 Sudokus (e.g., as mentioned in the reviewer discussion, by including the results on slow convergence and including more discussion on why the number of decoded clauses is so large).
Decision: Accept (poster)