Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: This paper introduces SymSATNet, a modified version of SATNet that can find and exploit symmetries of a learnable logical formula.
Exploiting symmetries reduces the number of parameters and the complexity of the learning problem, which leads to faster training and better generalization.
Symmetries can either be specified a priori to integrate domain knowledge, or inferred from data with a novel 'SymFind' algorithm.

On 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.

For 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$. 
Finally, the formula $C$ is projected onto the space of $G$-equivariant matrices (with the discovered symmetry group $G$) as a warmstart for training SymSATNet.

Empirically, 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.
In 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.
Finally, 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.
Finally, 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.
strengths_and_weaknesses: #### Originality
The 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.

#### Quality
Overall 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.

Current weaknesses in quality:
- Related work:
	- 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.
- Experiments:
	- 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.
	- 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.
	- It would be great if the authors included also the train loss curves in the appendix for all experiments.
	- 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.


#### Clarity
Overall, the paper is well-written, with a clear presentation.
On a small note, it might be useful to add line numbers to the algorithm box. 
Also, 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.

#### Significance
The 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.

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.
- 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.
- 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?
- See also questions raised in Strengths and Weaknesses.

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).
2) 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.

If discussions of these remaining unclear limitations are added to the paper, I am willingly to increase the rating of the paper.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: 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:
1. 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;
2. 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.


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.

**Strengths**:
- 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.
- 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.
SymFind 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. 
- Noisy SAT solving results are interesting as a bonus.

**Weaknesses**:
- 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? 
Performance 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? 
- 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. 
- 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.

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?
2. Is it possible for SymFind to propose incorrect symmetries? What will happen if this is the case empirically, or in the worst case?
3. How does the SymSATNet model (and, for that matter, SATNet) perform with respect to a symbolic Sat solver on these domains?
4. How does SymFind perform with respect to existing symmetry-breaking techniques for SAT solving?
5. How does SymSATNet, the baseline SATNet, and the automatic symmetry finding problem scale with the number of constraints/propositions to be solved?

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.
review_title: null

final_score: rating: 8: Strong Accept: Technically strong paper, with novel ideas, excellent impact on at least one area, or high-to-excellent impact on multiple areas, with excellent evaluation, resources, and reproducibility, and no unaddressed ethical considerations.
review_content: 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. 
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. 

Below are some suggestions for the authors to further improve the paper:
* 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. 
*  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. 
* 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. 
* 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
rules having symmetries, we mean that the solution set of those rules is closed under the transformations of those symmetries."
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?
* 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?
* 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? 
* 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.

Some I can think of:
* The approach can only handle permutation symmetries, not all symmetries.
* The approach only works with SATNet.
review_title: null

Meta-review: metareview: This paper describes a refinement of SATNet that incorporates or finds symmetries in constrain satisfaction problems.  Experiments are given on Rubik's cube and Sudoku both of which exhibit significant symmetries (rotations and reflections of the cube and permutations of some rows and columns in Sudoku).  We have three reviews which are uniformly positive.  One weakness expressed is that the experiments seem toyish.  I also have that concern.  I would have to have see experiments on larger SAT problems before being convinced that there is something useful here.  But has the reviews are positive I will recommend acceptance.
confidence: Less certain
Decision: Accept