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.

翻译：SATNet是一个不同的制约解析器, 具有自定义的反向调整算法, 可以用作深层学习系统中的一个层。 这是一个很有希望的建议, 可以弥合深层次的学习和逻辑推理。 事实上, SATNet 成功地应用到学习复杂的逻辑拼图的规则, 例如数独, 仅从输入作为图像的输入和输出对方中学习。 在本文中, 我们展示了如何通过利用特定但未知的逻辑谜题或更一般的逻辑公式的目标规则的对称来改进对SATNet的学习。 我们介绍了SymSATNet, 这是SATNet的一个变体, 将目标规则的给定的对称转换成SATNet参数参数的参数, 并且要求参数应具有某种特定的参数形式来保证条件。 这一要求极大地减少了用足够对称法来学习规则的参数数量, 使SymSATNet的参数学习比SATNet的参数要容易得多。 我们还描述了一种自动发现目标规则的对称技术, 也就是SymSATNet的对Symetromas 和对SySAT 的模型进行基础实验。