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을 개선하는 방법을 제안한다. 본 논문이 제안하는 SATNet의 변형 모델인 SymSATNet은 논리 규칙이 가지는 대칭성을 SATNet의 매개변수가 가져야할 조건으로 치환하고 이 조건을 만족하는 특정 매개변수 형식을 가진다. SymSATNet은 이 매개변수 형식을 이용해 충분한 대칭성을 가지는 문제를 학습할 때 학습해야할 매개변수의 수를 크게 줄여서 SATNet보다 효과적으로 학습한다. 또한 본 논문에서는 예시로부터 논리 문제의 규칙이 가지는 대칭성을 자동으로 발견하는 알고리즘을 소개한다. 실험에서는 스도쿠와 루빅스 큐브를 이용한 문제를 통해 SymSATNet의 개선된 학습 능력을 시험한다.
