Learning Symmetric Rules with SATNet
Authors: Sangho Lim
Eun-Gyeol Oh
Hongseok Yang
Venue: NeurIPS 2022 Accept (2022)
Keywords: group equivariance
deep learning
MAXSAT
SATNet

Abstract: SATNet is a differentiable constraint solver with a custom backpropagation algorithm, which can be used as a layer in a deep-learning system. It is a promising proposal for bridging deep learning and logical reasoning. In fact, SATNet has been successfully applied to learn, among others, the rules of a complex logical puzzle, such as Sudoku, just from input and output pairs where inputs are given as images. In this paper, we show how to improve the learning of SATNet by exploiting symmetries in the target rules of a given but unknown logical puzzle or more generally a logical formula. We present SymSATNet, a variant of SATNet that translates the given symmetries of the target rules to a condition on the parameters of SATNet and requires that the parameters should have a particular parametric form that guarantees the condition. The requirement dramatically reduces the number of parameters to learn for the rules with enough symmetries, and makes the parameter learning of SymSATNet much easier than that of SATNet. We also describe a technique for automatically discovering symmetries of the target rules from examples. Our experiments with Sudoku and Rubik's cube show the substantial improvement of SymSATNet over the baseline SATNet.

Learning Symmetric Rules with SATNet
Sangho Lim" School of Computing KAIST
Eun-Gyeol Oh"
Graduate School of Information Security KAIST
Daejeon, South Korea 1im. sangekaist........ kr
Daejeon, South Korea eun-gyeol oh@kaist. ac. kr
Hongseok Yang
School of Computing and Kim Jaechul Graduate School AL, KAIST Discrete Mathematics Group, Institute for Basic Science (IBS)
Daejeon, South Korea
hongseok yangkkaisnnnaaaaaaa.mkmm ac.kr
Abstract
SATNet is a diffcrentiable constraint solver with custom backpropagation algo- rithm, which can be used as layer deep-learning system. It is a promising proposal for bridging deep learning and logical reasoning. In fact, SATNet has been successfully applied to learn, among others, the rules of a complex logical puzzle, such Sudoku, just from input and output pairs where inputs are given as images. In this paper, we show how to improve the learning of SATNet by exploiting symmetries in the target rules of given but unknown logical puzzle or more generally a logical formula. We present SymSATNee,, a variant SAT- Net that translates the given symmetries of the target rules to condition the parameters of SATNet and requires that the parameters should have particular parametric form that guarantees the condition. The requirement dramatically re- duces the number of parameters to learn for the rules with enough symmetries, and makes the parameter learning of SymSATNet much easier than that of SATNet. We also describe technique for automatically discovering symmetries of the target rules from examples. Our experiments with Sudoku and Rubik's 's cube show the substantial improvement of SymSATNet over the baseline SATNet.
Introduction
Bringing the ability of reasoning to the deep-learning systems has been the aim of a large amount of recent research efforts 28
26 23 One notable outcome of these endeavours SATNet (26). a differentiable constraint solver with an efficient custom backpropagation algorithm. SATNet can be used as a component of deep-learning system and make the system capable of learning and reasoning about sophisticated logical rules. Its potential has been demonstrated successfully with the tasks of learning the rules of complex logical puzzles, such as Sudoku, just from input-output examples where the inputs are given as images.
We show how to improve the rule (or constraint) learning of SATNet, when the target rules have permutation symmetries. By having symmetries, we mean the solutions of the rules are closed under the permutations of those symmetries. For example, in Sudoku, if completed 9 Sudoku board is solution, permuting the numbers to 9 in the board, the first three rows, or the last three columns always gives rise another solution. Thus, these permutations are symmetries of Sudoku.
These authors contributed equally to this work.
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

Our improvement is a variant of SATNet, called SymSATNet, which abbreviates symmetry-awe awwre SATNet. SymSATNet assumes that some symmetries of the target rules are given a priori although the rules themselves are unknown. It then translates these symmetries into condition on the parameter matrix C' E RR**" of SATNet (or our minor generalisation), and requires that the parameters have a particular parametric form that guarantees the condition. Concretely, the translated condition says that the matrix C' regarded as a linear map should be equivariant with respect to the group G determined by the given symmetries, and the requirement is that C' should be linear combination of elements in a basis for the space of G-equivariant symmetric matrices. The coefficients of this linear combination the parameters of our SymSATNet, and their number is often substantially smaller than that of the parameters of SATNet For Sudoku, the former is 18, while the latter is 7292 or k- . 729 for some k E N at best. The reduced number of parameters implies that SymSATNet has to tackle easier learning problem than SATNet, and has a potential to learn faster and generalise better than SATNet.
Who provides symmetries for SymSATNer? The default answer is domain experts, but a better alternative is possible. We present an automatic algorithm to discover symmetries. Our algorithm based on empirical observation that symmetries emerge in the parameter matrix C' of SATNet in the early phase of training, as clusters of similar entries. Our algorithm takes a snapshot of C' at some training epoch of SATNet, and finds group G' such that (i) specific entries of C' share similar values by G-equivariance condition, and (ii) the number of SymSATNet parameters under G is minimised.
We empirically evaluate SymSATNet and our symmetry symmetry-discoveriiee discovering algorithm with Sudoku and a problem related Rubik's 's cube. For both problems, our algorithm discovered nontrivial symmetries, and SymSATNe with manually specified or automatically found symmetries outperformed the baseline SATNet in learning the rules, in terms of both efficiency and generalisation.
Related work There have been multiple studies on discovering symmetries present in conjunctive normal form (CNF) formulas in order to reduce the search space of satisfiability (SAT) solvers. Crawford (7] proved that the symmetry-detectee
problem is equivalent to the graph isomorphism problem, and showed how to reduce the complexity of pigeonhole problems using symmetries.
Crawford et al. [8] proposed bymmetry-breaking predicates (SBPs), and Aloul et al. [ developed SBPs with more efficient constructions. For automatic symmetry detection, Darga et al.
presented
a method that improves the partition refinement procedure introduced by McKay [19 20 and Darga al. [0] proposed algorithm that achieve efficiency by exploiting the sparsity of symmetries. In contrast to these global and static methods, Benhamou et al. [4] and Devriendt et al. [12 handled local symmetries that dynamically arise during search. The use of symmetries also appears in NeuroSAT [22). which learns how to solve SAT problems from examples. NeuroSAT AT solves a given SAT formula by message passing over a graph constructed from the formula, and in so doing, its learnable solver can exploit symmetries in the formulas. All of these techniques use symmetries to help solve given formulas, whereas our approach uses symmetries to help learn such formulas. Another difference is that those techniques find hard symmetries of given formulas, whereas our approach discovers soft or approximate symmetries in a given SATNet parameter matrix. In the context of deep learning, Basu et al. 3 and Dehmamy et al. [11 described algorithms that find and exploit symmetries via group decompositions and Lie algebra convolutions. But these techniques are not designed to find symmetries in logical formulas.
Our work is related to the studies on learning logical rules from examples using gradients. Yang et al. (28) proposed neural logic programming, an end-to-end differentiable system which learns first- order logical rules, Evans and Grefenstette [14] proposed a differentiable inductive logic programming system which is robust to noise of training data, and Cingillioglu and Russo (5) introduced an RNN- based model learn logical reasoning tasks end-to-end. Want et al. 25 26 presented SATNet using the mixing method, and Topan et al. (23) further improved SATNet by solving the symbol grounding problem, a key challenge of SATNet. Our work extends these lines of work by proposing how to discover and exploit symmetries from examples when learning logical rules with SATNet.
'SATNet assumes that C' is of the form ST for some S E mm for m < n, so that the number of parameters is < n²? But often it is still substantially larger than the number of parameters of SymSATNet.
2

---

2 Background
We review SATNet, the formalisation of symmetries using groups, and equivariant maps. For natural number n, let [n] = (1,....7) n), and for a matrix M, let Mi be the ji, entry of M.
2.1 SATNet
A good starting point for learning about SATNet is to look at its origin, the mixing method 22 which an efficient algorithm for solving semidefinite programming problems with diagonal constraints. Let n. k E N and C' be a real-valued symmetric matrix in R"**, The mixing method aims at solving the following optimisation problem:
argmin (C, VTV) subject to ||0:|| = for E [rd]
(I)
VERkxn
where Us is the i-th column of the matrix V, and ||x]|| is L2 norm of Us The mixing method solves (T) by coordinate descent, where each column v; of V is repeatedly updated follows: Ii 4 EjE(n),j4 C2 and 64 +
To:ll -Tol] This always finds a fixed point of the equations. In fact, it
2:
is shown that almost surely this fixed point attains global optimum of the optimisation problem.
An example of the above optimisation problem most relevant to us continuous relaxation of MAXSAT, MAXSAT is problem of finding truth assignments to n boolean variables bi....,by b, assumes m clauses of those variables, Fi,..... Fm. where Fe is the disjunction of some variables with or without negation: F3 b, V V bi V -bip+1 V...-b. -bp... Then, MAXSAT asks for truth assignment on the variables that maximises the number of true clauses F; under the assignment. The rules of many problems, including Sudoku, can be expressed as an instance of MAXSAT.
To apply the mixing method to MAXSAT, introduce relaxed vectors U1,...., On R that encode the boolean variables, and construct the matrix 5 E R2 that encodes the m clauses of MAXSAT: the (E. entry of S has if I' contains by: and -1 if F/ includes -by; and 0 if neither of these cases holds. Then, the problem in [I is formed with C = - S, and solved by the mixing method.
SATNet is a variant of the mixing method where some of the columns of V are fixed and the optimisation is over the rest of the columns columns?PConcrees Concretely, it assumes that the column indices in [r] are split into two disjoint sets, I and O (i.c., IUO = [n] and Ino = (). The inputs of SATNet are the columns v2 of V with i I, and the outputs are the rest of the columns (i.c.. the v, 's with O). The symmetric matrix is the parameter of SATNet. Given the input vectors, SATNet repeatedly executes the coordinate descent updates on each output column, until it converges.
One important feature of SATNet is that has a custom algorithm for backpropagation. Let Vz be the matrix of the input columns to SATNet, and Vo be that of the output columns computed by SATNet on the input V/2 under the parameter C. Assume that / is a loss of the output Vo. In this context, SATNet provides formulas and algorithms for computing the derivatives 01 and 01/0C.
We recall the formulas for the derivatives. Let 01 < 02 <... < o10) be the sorting of the indices in O. Assume that SATNet was run until convergence, so that the output columns in Vo are the fixed &u point of the coordinate descent updates: for all E O. go Eje(a, Co, and v, || The formulas for 01/ Vz and 01/0C at (Vz, Vo, C') are defined in terms of the next quantities:
C² ggo0x|o)
Pe PE Olk
U R
W E R Olkxn?
They have the following definitions: for i,j [[0]] p.g E [k], and m,dr [n].
(C")
0
i=
U (P((D' + C*) s0 T))²
al
T
Cocos
if
Vvec(Vo)
(D')s=
A1loo:11
ifi=j
0
if r = 0; and 8 0;
ifi
Vp
if r o and # 0,
W(--))k-p (r-1)nts
(J+
Un, vo,) Jm.
if if + j.
V
if + o and 0;
P P(111)+pp (1-13449
10
if r + og and 8 + 0z-
"The original SATNet assumes that C' has the form S S for some m x n matrix S. We drop this assumption and adjust the forward and backward computations of SATNet accordingly. The main steps of derivations of the formulas for the forward and backward computations from the work on SATNet (26).
3

---

Here @ is the Kronecker product, is Moore-Penrose inverse (also known as pseudo inverse), and vec Vo) is the vector obtained by stacking the columns of Vo. Let CO. E R R|o|x|z| be obtained by restricting C' to the indices (o.t) with E O and E I. Then,
(Co,z @ lt). SATNet computes the above derivative formulas efficiently by iterative algorithms.
01/0 vee(C) = --,
(2)
2.2 Symmetries and equivariant maps
By symmetries set X, we mean group G that acts on X. The acting here refers to a function from G x X' to X, called group action, such that (i) e and (ii) (g g') = g (g' x) for all g, g' E G and
x = x for the unit e E G and any x E X, X, where o is the group operator of G.
We use symmetries of permutations on finite set. The set X' in our case is R*x", |the space of the matrix V in (I). and G is a subgroup of the group S, of all permutations on [n]. The group action g V is then defined by permuting the columns of V by g: for all i, E [n)] (o V)i.j = VG) This group action can be expressed compactly with the n X n permutation matrix Pa-1 where (Pg-)),, [(=ا- and g V = VPg- g-1 for the indicator function 1I. Throughout the paper, we often equate each element y of with its permutation matrix Pg. and view G itself as the group of permutation matrices Po for g E G with the standard matrix multiplication.
One important reason for considering symmetries is to study maps that preserve these symmetries. called equivariant maps. Let G' be group that acts on sets X' and y.
x)==)))-) = (f(x)) for all E G and x E X. is G-invariant or invariant if f(g - x) = [(x) for all g E G and æ E X.
Definition 2.1. A function X + y is G-equivariant equivariant if f(g xx)
The forms of equivariant maps have been studied extensively in the work on equivariant neural networks and group representation theory C representation theorems for different G's describe the matrix form of f. We use permutation groups defined inductively by the following three operations.
18 27 In particular, when f is linear, various
Definition 2.2. Let G and I be permutation groups on (p) and [g). with each group element viewed as a p X p or q q permutation matrix. The direct sum G @ H1 the direct product G @ H, and the wreath product H G are the following groups of (p+ q) x (p + or pq x pg permutation matrices with matrix multiplication as their composition:
Go H = [g + h: G, h H);
G H = we Gg
H G= (wr(h, g g G, G H²).
Here g @ h is the block diagonal matrix with p x p matrix g as its upper-left corner and q x q matrix h the lower-right corner, g h is the Kronecker product of two matrices g and h, and wr(h, g) is the pq x pg permutation matrix defined by wr(h, () i, E' E [p] and j.j E [g].
( for all
The next theorem specifies the representation of G-equivariant linear maps for an inductively- constructed G, by describing a basis of those linear maps. For a permutation group on [m], let E(G) = M E mm Mg = gM, Vg E G), the vector space of G-equivariant linear maps, where each g E G is regarded as a permutation matrix. See Appendix B for the proof of Theorem 2.3
Theorem 2.3. Let G, H be permutation groups on [p] and [g). and B(G), B(H) be some bases of E(G) and 8 (H), respectively. Then, the following sets form bares G @ H. G & H. and H G:
B(G + H) = (A 0,, O, + B A B(G), B B(H))
100x(x+00))
(HH):
B(GHH) = (A AE BE
B(H[G) = (A & 10 AE A., = 0 for E [p] and O', EOHH)))) U (To B: B()), 0E
Here Om is an everywhere-zero matrix in mm and 1RXS, I are the matrices defined by (1xxs)iJ = (is,,,EEs), (1R)s = (i=jjiem) whose shapes are defined by the context in which they are used. Here, 10xip+09: 1 ( E ((++a)x(+*)) 1o'x0" Rixq, Io E RPxP Also, (GG) (l(()) g E G} :i [p]) (i.e. the set of G-orbits), and p O (p

---

3 Symmetry-aware SATNet
In this section, we present SymSATNet, which abbreviates symmelry-aware SATNet. This variant is designed to operate when symmetries of a learning task are known a priori (via an algorithm or domain expert). The proofs of the theorem and the lemma in the section are in Appendix C
SymSATNeet solves the optimisation problem of SATNet, but under the following assumptions:
Assumption 3.1. The optimisation objective (C, VTV) in ( map on V g* is invariant under a permutation group G, whose action is of type in Section 2.2 (i.e., each g E G acts as permutation the columns of V).
Continuing our convention, we denote P. by g. One immediate consequence of Assumption 3.1 (C, V) = (C, (g (g v) = (C, (V for all g E G and V E R The next theorem re- re-phrases this property of the optimisation objective as equivariance of C: Theorem 3.2. Let C be a symmetric n. X n matrix. Then,
(C, (C,V = (V.
for all V E Bx and G C as a linear map on R is G-equivariant, that is, Cg gC for all g E G. Furthermore, if k = n, the converse also holds.
This theorem lets incorporate the symmetries into the objective of SATNet, and leaves the handling of the diagonal constraints of SATNet. The next lemma says that those constraints require no special treatment, though, since they already preserved by the action of any g G.
Lemma 3.3. Let V E &x* and E G. Every column of V has the L2-norm if and only if every column of Vg- has the Lz-norm 1.
Recall E(G) = {M EMERY Raxn; Mg gM, Vy E G} is the vector space of G-equivariant matrices.
Let E(G), be the subset of EG) containing only symmetric matrices. When G is a permutation group constructed by direct sum, direct product, and wreath product, we can generate a basis orthogonal basis of {()), by applying the Gram Schhidt orthogonalisation to {B + B" B E B(G)). Let
B(G) of E(G) automatically using Theorem 2.3 Then, can convert B(G)
B(G).- [Bi,... ..... Ba} be such an orthogonal basis of E(G)..
SymSATNNtt SATNet where the matrix C' in the optimisation objective has the form:
C=
8 B
for some scalars 01.....6e. R. Note that by this condition on the form of C, SymSATNet has
only d parameters o...... ls, instead of n x m for some m in the original formulation of SATNet. When the learning target has enough symmetries, d is usually far smaller than n² or even n, and this reduction brings speed-up and improved generalisation.
The forward computation of SymSATNet is precisely that of SATNet, the repeated coordinate-wise updates until convergence, and the backward computation is the one of SATNet extended (by the chain rule) with step backpropagating the derivatives 01/0C' 0C to each 01/00, o, for a E [d]
We summarise SymSATNet below using the usual notation of SATNet (I, O, Vz, Vo, and V):
The input is Vz, the matrix of the input columns of V.
The parameters are (f)...., Oa) E Rd. They define the matrix C' by
The forward computation solves the following optimisation problem using coordinate
descent, and returns Vo. the matrix of the output columns of V:
argmin (C, VV)
subject to || = for o O.
VoERA [o)
* The backward computation computes 01/0Vz and 01/00 by 2 and the chain rule:
01/00,- = (a1/0 veo veo = - U W veef B.).
(5)
PSymSATNetis is implemented based the SATNet code (26) available under the MIT License.
5

---

4 Discovery of Symmetries
One obstacle for using SymSATNeet is that the user has to specify symmetries. We now discuss how to alleviate this issue by presenting an algorithm for discovering candidate symmetries automatically,
The goal of our algorithm, denoted by SYMFIND, is find a permutation group G that captures the symmetries of an unknown learning target and is expressible by the following grammar: G ::= Im Zm Sm G G G @ G GIG for m N. The Im denotes the trivial group containing only the identity permutation on [m]] and Zm denotes the group of cyclic permutations on [m]. each of which maps E [m]] to (i + n) mod m for some n. The S. is the group of all the permutations on [m]. The last three cases are direct sum, direct product, and wreath product (see Definition 2.2). They describe three ways of decomposing a group G into smaller parts. Having such decomposition of G brings the benefit to recursively and efficiently compute a basis of G-equivariant linear maps.
The design of MYMFIND is based our empirical observation that softened version of symmetries often emerges in the parameter matrix C' of the original SATNet during training. Even in the early part of training. many entries of C' share similar values, and there is a large-enough group G with Cg = gC for all g E G. which intuitively means that G captures symmetries of C. Furthermore, we observed, such G often consists of symmetries of the learning target. This observation suggests an algorithm that takes C' as input and finds such G expressible in our grammar or its slight extension.
The input of SYMFIND is a matrix M E Rm As previously explained, when SYMFIND is called at the top level, it receives as input the pa- rameter of SATNet learnt by fixed number
Algorithm 1 SYMFIND with a threshold À >>> 0
1: Input: M E RR Output: (G,o)
2: if pri(grp(SS m, idm), M) - M[I S À then
of training steps. However, subsequent recursive calls to SYMFIND may have input M different
3: return (Sm,idm)
4: end if
from C. Then, SYMFIND returns a group G in our grammar and a permutation a on [m]. together defining a permutation group [m]:
5: A < {[Im,
6: if pri(grp(Zm, idm), M) - MII S À then
M)
7: A AU {Zem, idm)}
8: end if
SYMFIND(MM) = (G, = o = GGG).
(",,''+ + SUMFIND(M): 10: A - ((G'
9: (G',o')
11: for every divisor p of m do
where is the composition of permutations.
12: (G", o"" t- (M.
When G is decomposed into, say G @ G2, the specifies which indices in [m]] get permuted
13: A A+ o")}
14: end for
by G1 and G2- Once top-level SYMFIND re- turns (G.o), construct ((grp(G, )). as in Section with a minor adjustment with o
15: (G,o) & argmin dim dim(E(grp(G, o)))
16: return (G,o)
Algorithm| I describes SYMFIND, where id,. is the identity permutation on [m]. ||-||> is the Frobenius norm, dim(V) is the dimension of a vector space V, and the Reynolds operator prj projects matrix M E Rm orthogonally to the subspace of G-equivariant m m matrices:
pri M)
Σ 9Mg gEG
so that pr .)- - MlF computes the 1,2 distance between the matrix M and the space EG)).
In the lines 2-4, the algorithm first checks whether S, models symmetries of the input M accurately. If so, the algorithm returns (Sm, idm). Otherwise, assumes that an appropriate group for M's symmetries is one of the remaining cases in the grammar, and constructs a list A of candidates intially containing the trivial group (Im; idm). In the lines 6-8, the algorithm adds a pair (Zm; idm) to A if it approximates M's symmetries well. In the lines 9-10, the algorithm calls the subroutine SUMFIND which finds grp ,o) with G' = ① G² that approximates M's symmetries well. In the lines 11-14, the algorithm calls the other subroutine PRODFIND for every divisor p of m. For each p. PRODFIND finds grp(G" o²) with G" GH & GK (or G/ 2 GT)) that approximates M's symmetries well, where GK[ and G are permutation groups on [p] and [m/p]. Finally, in the line 15, our SYMFIND picks a pair (G,a) from the candidates A with the strongest level of symmetries in the sense that the basis of grp(G, (BGG,,))equee -qquivariant matrices has the fewest elements.
We construct B(grp(G, [oooT :B E B(G)), which is orthogonal basis for E(grp(G,

---

The subroutine SUMFIND clusters entries of M as blocks since block-shaped clusters commonly arise matrices equivariant with respect a direct sum of groups. The other subroutine PRODFIND uses technique [4 to exploit typical pattern of Kronecker product of matrices, and detects the presence of the pattern in . by applying SVD a reshaped version of M. Each subroutine may call SYMFIND recursively. See Appendix D for the details.
5 Experimental Results
We experimentally evaluated ATmSATNet and the SYMFIND algorithm on the tasks of learning rules of two problems, Sudoku and the completion problem of Rubik's cube. The original SATNet was used baseline, and both ground-truth and iilomatically-disovveeee symmetries were used for SymSATNet. For SYMFIND, we also tested its ability to recover known symmetries given randomly generated equivariant matrices. We observed significant improvement of SymSATNet over SATNet in various learning tasks, and also the promising results and limitation of SYMFIND.
Sudoku problem In Sudoku, we are asked to fill the empty cells of 9 x board such that every row, every column, and each of nine 3 x 3 blocks have all numbers the encoding of a full number assignment for the board where the (i. k--th entry of A is 1 if the (i,j)-th cell of the board contains k. In SATNet, we flatten A to the assignment on the n = 93 boolean variables, and relax each variable into R* resulting V E IR* kin in the objective of SATNet.
1.0
9. Let A E 1) 9999X9 be
0.6
Text
0.2
SATNet
SymSATNet
SymSATNct Auto
00
Epoch
(a) Sudoku
The rules of Sudoku have symmetries formalised by G = (Sg S3) @ (S3 S3) @ Sg. Each of two S3 1S refers solution-preserving permutations for rows and columns in Sudoku. The last Sg refers to permutations of the assigned numbers 1- in each cell. See Appendix [F] for more infor- mation about the symmetry group for Sudoku.
0.6
Test Accuracy
0.2
SATNet-Pain SATNut-300a.x
SymrAA Net SymdAA NetsAuto
0.0
0
20
60
80
100
To learn the rules of Sudoku using SymSATNet, we constructed a basis B(G),, as explained in Sec- tion has 18 elements, which means that Sym- SATNet has 18 parameters to learn.
Epoch
(b) Rubik's cube
Figure I: Test accuracies over training epochs.
We used 9K training and IK test ex- amples generated by the Sudoku gen- erator (21). Each example is a pair (Vz, Vo) where the input Vi assigns 31- 42 cells (out of 81 cells) and the output Vo specifies the remaining cells. Sym- SATNet was compared with SATNet- Plain without auxiliary variables, and SATNet-300aux with 300 auxiliary vari- ables. We used binary cross entropy loss and Adam optimizer [16), with the learn- ing rate 7 2 10 for SATNet-Plain and SATNet-300aux as the original work and 1 = 4 10 for SymSATNet. We measured test accuracy, the rate of the sooeee Sudoku instances by the forward computations. We reported the average over 10 runs with 95% confidence interval.
Table 1: Best test accuracies during 100 epochs and aver- age train times (10 sec). Additional times for automatic symmetry detection also reported after
MODEL
SUDOKU
CUBE
Acc. TIME
Acc.
TIME
SATNET-PLANE
88.1%
48.0
55.7%
1.8
11.8%
=0.17
20.7%
=0.01
SATNET- 330AUXX
97.9%
90.3
56.5%
14.0
10.3%
10.68
10.9%
10.12
SYMSATNET
99.2%
25.6
66.9%
1.1
+0.2%
+0.14
11.2%
-0.00
SYMSATNET-AUTO
99.5% %
22.7
68.1 %
3.4
+0.14
40.66
10.2%
..2.8%
+0.35
10.19
The results are in Figure and Table T (SymSATNNetAAute refers to variant of SymSATNe that
uses SYMFIND as subroutine to find symmetries automatically, and will be described later this
section.) Our SymSATNet outperformed SATNet-Plaie and SATNet-300aux. On average, its 100
7

---

epochs finished 2-4x faster in terms of wall clock than two alternatives. due to the reduced number of itteatiinn and avoidance of matrix operations. See Appendix for the efficiency of SymSATNet. Despite the speed up, the best test accuracy of SymSATNet 29) was significantly better than SATNet-Plain (88.1)) and slightly better than SATNet-300aux (97.9%).
Completion problem of Rubik's 's cube The Rubik's cube is composed of 6 faces, each of which has 9 facelets. We considered a constraint satisfaction problem where we are asked to complete the missing facelets of the Rubik's 's cube such that the resulting cube is solvable; by moving the cube, we can make all facelets in each face have the same colour, and no same colours appear in two faces. Let A E {0. 1] 1]6x9x6 be a colour assignment of Rubik's ' cube where the (i,j, k)-th entry has and only if the j-th facelet of the i-th face has colour k. We formulate the optimisation objective of
SATNet for Rubik's cube using the relaxation of A to V E R for 71 = 6 x 9 x 6.
This problem has symmetries formalised by G = Rs4 & Ra on [n]. Here R54 and Re are permutation groups on [54] and [6), each of which captures the allowed moves of facelets, and the rotations of the whole cube. If colour assignment A is solvable, so is the transformation of A by any permutations in G. See Appendix For more information about the symmetries of this problem.
We generated a basis B(G), in three steps. We first created B R54) and ((Re) using the generators of each group [5]. Next, we combined them using Theorem 2.3 to get B(G), which converted to symmetric orthogonal basis (()), > via Gram-Schmidt. The final result has 48 basis elements.
We used dataset of 9K training and IK test examples generated by randomly applying moves to the solution of the cube, Each example is a pair (Vz, Vo) where V7 assigns colours to facelets except for two corner facelets, two edge facelets, and one center facelet, and Vo specifies the colours of those five missing facelets. In the test examples, only Vzz is used. We trained SymSATNet, SATNet- Plainn, and 3A0Nx for 100 epochs, under the same configuration as in the Sudoku case.
The results appear in Figure D and Table I On average. the 100-epoch training of SymSATNet completed faster in the wall-clock time than those of SATNet-Plain and SATNet-300aux. Also, it achieved better test accuracies (66.9%) than these alternatives (55. 7% and 56.5%). Note that unlike Sudoku, the test accuracy of SATNet-300aux was only marginally better than that of SATNet- which indicates that both suffered from the overfitting issue. Note also the sharp increase in the training time of SATNet-300aux. These two indicate that adding auxiliary variables is not so effective for the completion problem for Rubik's cube, while exploiting symmetries is still useful.
Automatic discovery of symmetries To test the effectiveness of SYMFIND, we tested whether S SYMFIND could find proper symmetries in Sudoku and Rubik's s cube. We applied SYMFIND to the parameter C' of SATNet-Plain in T-th training epoch, where T = 10 for Sudoku and = 20 for Rubik's s cube. For Sudoku, SYMFIND always recovered the full symmetries with G = (Sg SSa) ? (Sy 7 S3) @ Sg in our 10 trials. For Rubik's cube, the group of full symmetries
grp(G. for G= S3x @ (Sy1 S8x @ (11)) (S2 S3). SYMFIND recovered all the parts except Sy S22 Instead of this, the algorithm found S12 & S2 or S3 @ Sg. or S @ Sq in our 10 trials. We manually observed that the entries of C' in the corresponding part were difficult to be clustered, violating the assumption of SYMFIND. This illustrates the fundamental limitation of SYMFIND.
To account for the limitation of SYMFIND, we refined the group G of detected symmetries to a subgroup in an additional validation step, before training SymSATNet with those symmetries. In the validation step, we checked the usefulness of each part G; of the expression of G' in our grammar. Concretely, we rewrote only with the part G; concern, where all the other parts of G were masked by the trivial groups Ig. After projecting C' with the masked groups using Reynolds operator, we measured the improvement of accuracy of SATNet over validation examples. Finally, we assembled only the parts G, that led to sufficient improvement. For example, if G (Zz (Zz&S,) @5, is discovered by SYMFIND, we consider the parts G = Zz. G2 = S1, and G3 = Sz. Then, we construct three masked groups G = (Zg @ I4) @ Iz. G² (Ig S.) @ Iz. and G = (Is @ Ia) @ Sz, and measure the accuracy of SATNet with C' projected by each G² over validation examples. If G and G¹2 show accuracy improvements greater than threshold, we combine G1 and G3 to form G'= (Z, @ I4) @ Sz. which is then used to train SYmSATNet.
We used 8K training, IK validation, and 1K test examples to train SymS ATNet with symmetries found by SYMFIND and the validation step. We denote these runs by SymSATNNt-Auto. We took a group G discovered by SYMFIND in T'-th training epoch (with the same T above) and constructed
8

---

its subgroup G' via the validation step. SymSATNet was then trained after being initialised by the projection of C with G'. The other configurations are the same as before.
As shown in Figure and Table 1 Rubik's is cube (68.1%) better than even SymSATNeet During the 10 trials with Sudoku, SymSATNet- Auto was always given the full symmetries in Sudoku. For Rubik's 's cube, when SymSATNNet-
performed the best for Sudoku (99.5%) and
was given correct subgroups (e.g. ((Sg 1 S3) @ (S3 l Sg) @ (Z4 @ I&)) @ (S2 Sa), ((S2 2 Sa) @ (S3 2 (Sp I S4)) @ (Is & Ia)) @ (S2 ())). then it performed even better than SymSATNet In two of the 10 trials, slightly incorrect symmetries were exploited, but it outperformed SATNet- and EATNet-300aur These results show the partial symmetries of subgroups derived by the validation step are still useful, even when they are slightly inaccurate.
Robustness to noise We tested robustness of SymSATNet and SymSATNet-Auto noise-corrupted datasets. We generated noisy Su- doku and Rubik's cube datasets where each train- ing example is corrupted with noise; it alters the value of random cell or the colour of random facelet to a random value other than the origi- nal. We used noisy datasets with 0-3 corrupted instances to measure the test accuracy, and tried 10 runs for each dataset to report the average and 95% confidence interval. All the other setups are the same as before. Figure 2 shows the results. In both problems, SymSATNet was the most ro- bust, showing remarkably consistent accuracies. SymSATNet-Auto showed comparable robustness to ZATNet-300aux in noisy Sudoku, but outper- formed the two basclines in noisy Rubik's 's cube.
noise by
Test Accuracy
0.9
0.8
SATNet-Plain
SymSATNue
SATMet- -000ax
SymSATNet--uut
Number of Corruption
(a) Sudoku
0.7
0.6
0.5
0.4
0.3
0.2
S4TNet-3000
SATNet Plain
SymSATNet Auto
SymSATNet
Next, to show the robustness of SYMFIND, we applied it to restore permutation groups G from noise-corrupted G-equivariant symmetric matrices M. We picked (G,, o,) for E [4] where Ii, 02.
Number of Corruption
(b) Rubik's cube
Figure 2: Best test accuracies for noisy Sudoku and Rubik's cube datasets.
0g are random permutations on [15]. [30], [12].
and is the identity permutation on [8]. and
G Zz t 23 + Zo Za + Za, G2 Sg S10,
G3 (S3 1 Sa) + Za. G4=
S2 X S2 X S2.
Then, we generated grp (Gi, o.)) -equivvaaai symmetric matrices M, by projecting random matrices with standard normal entries into the space (grp(GG,, o;)).. Then, Gaussian noises from N N(0, w²) for w = 5 x 10-3 are added to M,'s entries, and the resulting matrix M is given to SYMFIND.
For each (G,, ot). we repeatedly generated Mt and ran SYMFIND on M/ for 1K times, and measured the portion where SYMFIND recovered (G,, o.) ex- actly (full accuracy), and also the portion of cases where SYMFIND returned subgroup of (G,, o;) which is not the trivial group I.m. (partial accuracy). As Table 2 shows, the measured full accuracies were in the range of 60.3 - 93.5%, and the par- tial accuracies were in the range of 79.2 94.3%. These results show the ability of SYMFIND to recover meaningful and sometimes full symmetries.
Table 2: Full accuracies and partial accuracies of SYMFIND for given groups over IK runs.
GROUP
FULL Acc.
PARTIAL Acc.
Di= Za S
76.6%
79.2%
60.3%
79.9%
(Ss Sa) O Z
77.5%
87.0%
S, S, & 93.5%
94.3%
Transfer learning To test the transferability of SymSATNet, we generated Sudoku and Rubik's cube datasets with varying difficulties, where each dataset consisted of 9K training and 1K test examples. For SymSATNet-Auto, we split the 9K training examples into 8K training and 1K validation examples. We used three levels of difficulties for Sudoku and Rubik's 's cube (easy, normal, hard), based on the number of missing cells for Sudoku or missing facelets for Rubik's cube. The input part of Sudoku examples was generated with 21 (easy), or 31 (normal), or 41 masked cells (hard), and the input part of Rubik's cube examples was generated with 3 (easy), or (normal), or 5 missing facelets (hard). For both problems, used the training examples of easy or normal

---

1.0
0.8-
Text accuracy
Accurecy
0.4-
0.2
0.21
SATNet--laai SATNet 300aux
SymSATNet
SATNeE Hain
SymGATNet SymSATNect
SymSATNet Auto
SATNet 300Ouk
20
40
60
80
100
20
40
60
80
160
Epoch
Epoch
(a) Normal Sudoku Hard Sudoku
(b) Normal Rubik's cube + Hard Rubik's cube
1.0
Text Accuracy
0.8-
36 Accurscy
0.6-
0.2
0.2
SymSATNet NymsAANNesstutt
SATNet Paaln
SynSATNet Syn6ATNMet-Auto
SATHee--100auc
0.0
100
20
40
60
80
100
Epoch
Epoch
(c) Easy Sudoku + Hard Sudoku
(d) Easy Rubik's 's cube + Hard Rubik's 's cube
Figure 3: Transfer learning with various difficulties of training and test examples. For both problems, normal and easy examples were used to train, and hard examples were used to test each model.
datasets for training, and the test examples hard datasets for testing. We repeated every task in this experiment five times. Here we report the average test accuracies and 95% confidence interval.
Figure 3 shows the test accuracies throughout 100 epochs in the four types of transfer learning tasks. SymSATNeet achieved the best result in the whole tasks; it succeeded in solving hard problems after learning from easier examples. As Figures Ba and 3c indicate, STmeATNet-AA group symmetries in Sudoku. For Rubik's cube, Figure (3b shows that SymSATNNe-AAur achieved better performance over the baselines by finding partial symmetries. These results show the promise of SymSATNet and SymS ATNe--Auto for learning transferable rules even from easier examples.
exploited the full
Note that for the easy Rubik's cube dataset, SymSATNet-Auu showed poor performance (Figure 3d]. The poor performance comes from the violation of the assumption of SYMFIND; the group sym- metries sometimes did not emerge in SATNet in this case. three out of five trials with the easy Rubik's 's cube dataset, SATNet learnt nothing while producing the 0% test accuracy, and SYMFIND returned the trivial group which equated SymSATNet. two trials, SATNet learnt correct rules, and SYMFIND and the validation step found correct partial symmetries, which led to the improved performance. These results exhibit the fundamental limitation of SymSATNet-AAuto, whose performance strongly depends the original SATNet.
with SATNet-Plain. In the remaining
Conclusion
We presented SymSATNet, that is capable of exploiting symmetries of the rules or constraints to be learnt by SATNet. We also described the SYMFIND algorithm for automatically discovering symmetries from the parameter C of the original SATNet at fixed training epoch, which based on our empirical observation that symmetries emerge during training as duplicated C. Our experimental evaluations with two rule-learning problems related to Sudoku and Rubik's ss cube show the benefit of SymS ATN and the promise and limitation of SYMFIND. Although components of SYMFIND are motivated by the theoretical analysis of the space of equivariant matrices, such as Theorem 2.2, SYMFIND lacks theoretical justification its overall performance. One interesting future direction to fill in this gap by identifying when symmetrics emerge during the training of SATNet and proving probabilistic guarantees on when SYMFIND returns correct group symmetries.
similar entries of
This work was supported by the Engineering Research Center Program through the National Research Foundation Korea (NRF) funded by the Korean Government MSIT (NRF. 201 8R LASA 1059921) and also by the Institute for Basic Science (BS-R029-C1)..
Acknowledgement
10

---

References
[1] Fadi A Aloul, Arathi Ramani, Igor I. Markov, and Karem A Sakallah. Solving difficult instances of boolean satisfiability in the presence of symmetry. /EEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(9):117711137, 2003.
[2] Fadi A Aloul, Karem A Sakallah, and Igor L Markov. Efficient symmetry breaking for boolean satisfiability. IEEE Transactions on Computers, 55(5)-44-555, 2006.
[3] Sourya Basu, Akshayaa Magesh, Harshit Yadav, and Lav Varshney. Group equivariant neural architecture search via group decomposition and reinforcement learning. arXiv e-prints, pages arXiv-2104, 2021.
[4] Belaid Benhamou, Tarek Nabhani, Richard Ostrowski, and Mohamed Réda Saıdi. Dynamic symmetry breaking in the satisfiability problem. In Proceedings of the 16th international conference on Logic for Programming, Artificial intelligence, and Reasoning. LPAR-16, Dakar, Senegal (April 25-may 1, 2010), 2010.
[5] Nuri Cingillioglu and Alessandra Russo. Deeplogic: Towards end-to-end differentiable logical reasoning. In Proceedings of the AAAI 20 Spring Symposium on Combining Machine Learning with Knowledge Engineering (AAAI-MAKE 20/9), 2019.
[6] Taco S. Cohen and Max Welling. Group equivariant convolutional networks. In Proceedings of ICML' 16, pages 2990-2999, 2016.
[7] James Crawford. A theoretical analysis of reasoning by symmetry in first-order logic. In AAAI Workshop Tractable Reasoning, pages 17-22. Citeseer, 1992.
[8] James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry- breaking predicates for search problems. In Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, pages 148-159. Morgan Kaufmann Publishers Inc., 1996.
[9] Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, and Igor L. Markov, Exploiting structure in symmetry detection for CNF. In Proceedings of the 41st Annual Design Automation Conference, pages 530-534. Association for Computing Machinery, 2004.
[10] Paul T Darga, Karem A Sakallah, and Igor L Markov. Faster symmetry discovery using sparsity of symmetries. In 2008 45th ACM/IEEE Design Automation Conference, pages 149-154. IEEE, 2008.
[11] Nima Dehmamy, Robin Walters, Yanchen Liu, Dashun Wang, and Rose Yu. Automatic symmetry discovery with Lie algebra convolutional network. Advances in Neural Information Processing Systems, 34, 2021.
[12] Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe. Symmetric explanation learning: Effective dynamic symmetry handling for SAT. In International Conference Theory and Applications of Satisfiability Testing, pages 83-100. Springer, 2017.
[13] David Dummit and Richard M Foote. Abstract algebra, volume 1999. Prentice Hall Englewood Cliffs, NJ, 1991.
[14] Richard Evans and Edward Grefenstette. Learning explanatory rules from noisy data. J. Artif. Intell. Res., 61:1-64, 2018
[15] Mare Finzi, Max Welling, and Andrew Gordon Wilson. A practical method for constructing equivariant multilayer perceptrons for arbitrary matrix groups. In Proceedings of ICML'21, pages 3318-3328, 2021.
[16] Diederik P. Kingma and Jimmy Ba. Adam: method for stochastic optimization. CoRR, abs/1412.6980. 2015.
[17] Subrata Majumdar, Kalyan Kumar Dey, and Mohd Altab Hossain. Direct product and wreath product transformation semigroups. GANIT: Journal of Bangladesh Mathematical Society, 31:1-7, Apr. 2012.
11

---

[18] Haggai Maron, Heli Ben-Hamu, Nadav Shamir, and Yaron Lipman. Invariant and equivariant graph networks. Proceedings of ICLR'I9, 19, 2019.
[19] Brendan D. McKay, Backtrack programming and the graph isomorphism problem. 1976.
[20] Brendan D. McKay, Practical graph isomorphism. Congressus Numerantium, 30:45-87, 1981.
[21]
Kyubyong Park. Can convolutional neural networks crack sudoku puzzles? httpp:///githbb com Com//Kybyongg/aaa /sudbou sudoku 2018.
[22] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David Dill. Learning SAT solver from single-bit bit supervision. In International Conference on Learning Representations, 2019.
[23] Sever Topan, David Rolnick, and Xujie Si. Techniques for symbol grounding with SATNet. In Advances in Neural Information Processing Systems, volume 34, pages 20733-20744, Curran Associates, Inc., 2021.
[24] Charles F Van Loan and Nikos Pitsianis. Approximation with kronecker products. Linear algebra for large scale and real-time applications, pages 293-314. Springer, 1993.
[25] Po-Wei Wang, Wei-Cheng Chang, and J. Zico Kolter. The mixing method: low-rank coordinate descent for semidefinite programming with diagonal constraints. CoRR, abs/1706.00476, 2018.
[26] Po- Fe-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter. Satnet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. In Proceedings of ICML' 19, pages 6545-6554, 2019.
[27] Renhao Wang, Marjan Albooyeh, and Siamak Ravanbakhsh. Equivariant networks for hierar- chical structures. Proceedings of NewrlPS pages 13806-13817, 2020.
[28] Fan Yang, Zhilin Yang, and William W. Cohen. Differentiable learning of logical rules for knowledge base reasoning. In Proceedings of NeurlPS 17, pages 2017.
12


Reviews:
[{"review_id": "gnw6XyJlLdY", "reviewer": "Reviewer_NN1r", "summary": "The authors build on a differentiable constraint solver (SATNet, Wang et. al 2018) to propose a variant, SymSatNet, which exploits symmetries in the SAT problems in an attempt to improve the speed and accuracy of learning. This paper makes two primary contributions:\n1. SymSatNet, their symmetry-aware formulation of the original SATNet model, which allows the model to exploit known (user-specified) symmetries and therefore constrain the optimization problem;\n2. SymFIND, a method for discovering candidate symmetries based on approximate symmetries in the original SATNet model during training. This algorithm attempts to alleviate the domain-knowledge necessary to specify symmetries in advance in order to exploit the SySatNet formulation.\n\n", "questions": "1. Is it possible to better characterize when the SymFind algorithm should discover a candidate symmetry (eg. based on the training data it has observed?); and how many symmetries it can find with respect to the full ground truth symmetries?\n2. Is it possible for SymFind to propose incorrect symmetries? What will happen if this is the case empirically, or in the worst case?\n3. How does the SymSATNet model (and, for that matter, SATNet) perform with respect to a symbolic Sat solver on these domains?\n4. How does SymFind perform with respect to existing symmetry-breaking techniques for SAT solving?\n5. How does SymSATNet, the baseline SATNet, and the automatic symmetry finding problem scale with the number of constraints/propositions to be solved?\n", "limitations": " My main point here is already largely covered in the sections above, so I will be brief: the authors do discuss empirical limitations of their automatic symmetry finding algorithm. However, I found that their current evaluation, on the Sudoku domain, left me with more questions than answers: when the model discovers only some symmetries, whether it can discover incorrect symmetries, and why we should expect this model to work in general (as well as its scalability as a symmetry finding algorithm.) I do believe this can be addressed, which is why I am hoping to see some empirical or theoretical response from the authors.\n", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Overall summary of comments: I am interested in this paper, which I think presents both compelling empirical evidence for the base formulation of their model, and which presents an interesting algorithm for discovering symmetries in constraint problems as part of training a differentiable constraint solver. However, as I discuss below, in many ways this paper appears preliminary, and I think there is significant room for improvement in its presentation, motivation, and empirical validation. I think this is a promising paper, and it’s unfortunate that the NeurIPS review process doesn’t provide an opportunity for revision. I’ll try to provide broad and specific points for improvement below, and perhaps we can work with the authors as part of the response to effectively provide revised portions of the paper and additional experiments during the rebuttal.\n\n**Strengths**:\n- Empirical demonstration of SymSATNet algorithm is compelling with respect to the SATNet baseline. The basic premise of this formulation is that exploiting symmetries in the constraint solving problem should significantly constrain the search space being implicitly optimized for by the differentiable solver. The authors demonstrate their model on two classically symmetric SAT problems -- Sudoku and Rubik’s cube solving -- and show that their model both improves on test-time accuracy and generally appears to learn more quickly than the original SATNet model.\n- Empirical demonstration of the SymFind (automatic symmetry finding) algorithm is also promising on the Sudoku and Rubik’s cube domains, where the model appears to generally discover useful symmetries comparable to those specified in the base (known symmetries) model.\nSymFind algorithm is original and seems like a potentially novel and interesting method for discovering symmetries in SAT problems that could be of interest both to the original target audience of the SATNet paper (deep-learning practitioners looking to incorporate ‘logic-aware components’ into neural models) and to classical constraint solving problems (as a means for discovering symmetries.) However, I believe this algorithm is presented in quite a preliminary way, as I discuss below, and its presentation, verification, and validation could be improved to convincingly demonstrate what exactly the authors are onto here. \n- Noisy SAT solving results are interesting as a bonus.\n\n**Weaknesses**:\n- SymFind algorithm should either be better theoretically motivated, empirically validated, or both. I think this is the place where author response could yield the greatest differential on this paper, so I am noting it first. The automatic symmetry discovery, in my opinion, is the most interesting part of this paper, and also seems important to the original goals of the SATNet model. I actually think that it is fine that the model sometimes discovers only partial symmetries -- this would seem to be expected in general. However, I was not clear on either the theoretical behavior of this algorithm (is it possible for the model to overpropose symmetries that seemed to exist during training, but actually were not true symmetries in general ? Can the expected behavior be characterized with respect to the training curriculum, eg. the ‘percentage’ of symmetries observed? Could we construct adversarial training curricula for this model?); nor did the evaluation seem sufficiently robust. If the motivation for this approach is purely empirical -- that is, it seems that softened symmetries emerge in the parameter matrix C during training -- then that should be demonstrated using a much larger scale and targeted experiment -- eg. rather than focusing on the Rubik’s cube or Sudoku problems, I would want to see something more like “sampling large numbers of SAT proposition problems with explicit symmetries/permutations, sampling possible assignments, and demonstrating what ‘percentage’ of symmetries this model discovers in general.” Does that make sense? \nPerformance with respect to existing symbolic SAT solvers; and existing symmetry discovery methods? - - - The main evaluation is with respect to SATNet. This is, I think, also a weakness of the original SATNet paper, but seems important. How quickly can off-the-shelf SAT solvers solve the Sudoku and Rubik’s cube domains? Can existing symmetry-discovery algorithms designed for classical SAT problems robustly find symmetries from a similar training regime? \n- Clarity and motivation of presentation. The introduction, in particular, assumes significant base knowledge of the original SATNet paper, and the paper can be quite dense and hard to read without first reading over the original. I think one or more other real-world examples in the introduction could help motivate this paper. A single well-made visualization might also greatly improve the presentation of the ‘symmetries’ problem, and the way in which this model attempts to discover approximate symmetries in the parameter matrix. \n- As a small nit, it seems like the results section presentation of SymFind is out-of-date with respect to the rest of the paper: it uses an older name (SymSatNet-Auto) and references a ‘later’ presentation that in fact was moved before.\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "KZPnLmgfV57", "reviewer": "Reviewer_arDH", "summary": "This paper proposes to incorporate permutation symmetries into the training objective of SATNet. The symmetry constraints reduce the number of parameters, and only requires slight modifications on the backward computation. The experiments show that adding symmetries could improve generalization and computation speeds. Furthermore, the paper also proposes an algorithm that finds symmetries automatically when the prior knowledge is not present. ", "questions": "* Some neural combinatorial models, like NeuroSAT, enforces symmetries by designing specific network architectures. What do you think of the pros and cons of their approach and yours?\n* Would you further explain the difference between SATNet and SATNet-300aux? Why does SATNet-300aux improve a lot more on sudoku not rubik's cube?\n* What is the intuition that SymSATNet-auto performs better than SymSATNet when training and test are i.i.d but worse when they are not? \n* Since I couldn't find a conclusion section, what do you think it's the main limitation of the paper and interesting future direction?", "limitations": "I didn't find a proper section in the paper that addresses the limitation.\n\nSome I can think of:\n* The approach can only handle permutation symmetries, not all symmetries.\n* The approach only works with SATNet. \n", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Overall, this is a joyful reading for me. The paper is well-motivated. Exploiting symmetries is very important in combinatorial and logic reasoning problems. The proposed method is neat and fits nicely into the original framework of SATNet. The experiment results are also very promising. I'd recommend acceptance of this paper. \n\nBelow are some suggestions for the authors to further improve the paper:\n* The proposed method is only able to handle permutation symmetries. There are more complicated symmetries which a permutation matrix is unable to specify. For example, SAT/UNSAT is invariant under transformations like unit propagation, variable elimination. However, the paper uses \"symmetry rules\" throughout, including the title. It would be good to be more careful about the term and explicitly point this out in the paper. \n*  The paper lacks a proper conclusion section, which is a necessary place to summarize the paper, discuss limitations of the study and suggests future directions. \n* Add transfer learning experiments. For combinatorial problems, it's often the case that training and test distributions are not i.i.d. Incorporating symmetries should improve the performance on transfer learning. The last experiment is conducted when test distributions are slightly perturbed from training. It would be good to include the set-up where training and test come from completely different distributions. \n* Writing can definitely be improved. Some sentences are very wordy and long, which decreases the readability of the paper. One example is this sentence from line 27-30: \"By symmetries, we mean transformations of candidate solutions of those rules, and by\nrules having symmetries, we mean that the solution set of those rules is closed under the transformations of those symmetries.\"", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "IK9RPveNn12", "reviewer": "Reviewer_2aBF", "summary": "This paper introduces SymSATNet, a modified version of SATNet that can find and exploit symmetries of a learnable logical formula.\nExploiting symmetries reduces the number of parameters and the complexity of the learning problem, which leads to faster training and better generalization.\nSymmetries can either be specified a priori to integrate domain knowledge, or inferred from data with a novel 'SymFind' algorithm.\n\nOn a technical level, given a group of symmetries $G$ for the learnable formula, SymSATNet initially computes a basis for the vector space of $G$-equivariant linear maps.  It then parametrizes the learnable formula (represented as a matrix $C$) as a linear combination of such basis vectors, thereby ensuring that the learned formula obeys the given symmetries.\n\nFor discovering symmetries from data, the authors first train the standard SatNet for a small number of epochs on the available dataset. The SymFind algorithm is based on the observation that a 'softened' version of the true symmetries often emerges in the learned formula. To convert these 'soft' symmetries into 'hard' symmetries, the SymFind algorithm recursively finds the strongest combination $G$ of symmetry 'atoms' that still closely models the 'soft' symmetries exhibited by learned formula $C$. \nFinally, the formula $C$ is projected onto the space of $G$-equivariant matrices (with the discovered symmetry group $G$) as a warmstart for training SymSATNet.\n\nEmpirically, the authors compare SymSATNet (with ground truth symmetries or symmetries discovered by the SymFind algorithm) to the standard SATNet baseline on a Sudoku and Rubik's cube task. In both problem setups, given a partial assignment of a set of discrete variables, the task is to predict the correct assignment of the remaining variables under a set of problem-specific rules. The SATNet/SymSATNet model maintains a learnable set of rules based upon which the assignment is completed, and this rule set is learned from a dataset of completed assignments.\nIn Sudoku, SymSATNet and SATNet (with auxiliary variables) achieve a close to perfect test accuracy, in Rubik's cube SymSATNet outperforms SATNet. In both experiments, the version of SymSATNet with discovered symmetries achieved similar performance as the one with ground truth symmetries, as it is shown that the discovered symmetries either match or closely resemble the ground truth.\nFinally, the robustness to noisy/mislabeled data (for SymSATNet) and noisy formulas (for SymFind) is examined. In the presence of label noise, SymSATNet (with ground truth symmetries) outperforms the baseline in both problem setups, demonstrating the usefulness of known symmetries to correct for mislabeled data. Discovered symmetries demonstrate improved performance over the baseline in the Rubik's cube experiment, although exhibiting high variance.\nFinally, the SymFind algorithm is shown to have some robustness to noise applied to a dataset of formulas generated from hand-crafted symmetries. This demonstrates the ability to still recover partial and sometimes complete symmetries from corrupted formulas.", "questions": "- The original SATNet is demonstrated to benefit from adding auxiliary variables. Is it also possible to include auxiliary variables in SymSATNet? If so this should also be explored in the experiments, otherwise, this limitation should be discussed.\n- In Sudoku the problem reduces to only learning 18 parameters. While this clearly helps with generalization, I imagine it could also make training in general more difficult, as overparametrization typically allows for smoother training. As an alternative to explicitly parametrizing $C$ in an equivariant basis, have the authors also tried to parametrize the full matrix $C$ and then perform a differentiable projection onto the vector space with the desired symmetry properties on the forward pass? This could potentially result in similar generalization, but smoother training due to the increased number of learnable parameters.\n- In SymSATNet with discovered symmetries, why is the initial SATNet training run stopped at different epochs for the two experiments? I.e. after 10 epochs for Sudoku and after 20 epochs for Rubik's cube. Is this a sensitive hyperparameter?\n- See also questions raised in Strengths and Weaknesses.\n", "limitations": "1) It would be good to include a discussion on the limitations due to potentially non-usable auxiliary variables (in contrast to the original SATNet).\n2) As pointed out in the Clarity section, it is currently not clear what the runtime of the SymFind algorithm is and how it scales. If the runtime of SymFind makes up for a relevant part of the training time of SymSATNet-Auto, a discussion of the runtime limitations (with considerations of scaling with dimensionality) would be necessary in my opinion.\n\nIf discussions of these remaining unclear limitations are added to the paper, I am willingly to increase the rating of the paper.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "#### Originality\nThe authors improve an existing method with the idea of incorporating the use of symmetries. As pointed out by the authors, using equivariances and symmetries in general in deep learning is a known approach, but to the best of my knowledge, this is the first time it is used for learning logical formulas from data. The described algorithm for discovering symmetries also appears to be novel.\n\n#### Quality\nOverall the paper has a good quality, it appears that many considerations were taken into account in the design of the method and the SymFind algorithm. It performs well in the presented set of experiments, speeding up training and improving the generalization capabilities.\n\nCurrent weaknesses in quality:\n- Related work:\n\t- Currently, it is not clear to me if some parts of the SymFind algorithm are inspired by existing works on discovering symmetries. It would be good to add how it conceptually differs from the listed related work.\n- Experiments:\n\t- I find the experiments a bit too toy-ish. The Sudoku experiments seem to be too easy to make a strong point (already one of the baselines achieves an almost perfect test accuracy). While there is a clear performance improvement shown in the Rubik's cube experiment, it is still small-scale even compared to the visual sudoku presented in the original SATNet paper. Perhaps adding a visual component with a learnable neural network backbone in the experiment could make it more convincing.\n\t- Generally, it would be great to have more restarts of the experiments than 3 or 4, as the variance in some of the experiments is relatively large.\n\t- It would be great if the authors included also the train loss curves in the appendix for all experiments.\n\t- The validation step described in the paragraph starting at line 347 seems to be a vital component of the method. It would be good to show its effect in an ablation study in the appendix.\n\n\n#### Clarity\nOverall, the paper is well-written, with a clear presentation.\nOn a small note, it might be useful to add line numbers to the algorithm box. \nAlso, in table 1 I am not sure how the time per epoch was calculated for the SymSATNet-Auto. Does this take the runtime of the SymFind algorithm account? In any case it would be good to report the runtime of the SymFind algorithm separately from the time per epoch, as this is a potential limitation of the method.\n\n#### Significance\nThe presented method is significant in my opinion. SymSATNet allows to incorporate strong prior knowledge into SATNet and should often find applications when the often-used SATNet is currently employed. With the presented SymFind algorithm, the method is also applicable in case of no available prior knowledge of symmetries, which further extends the applicability.\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept