LEARNING TO SOLVE CIRCUIT-SAT: AN UNSUPERVISED DIFFERENTIABLE APPROACH
Recent efforts to combine Representation Learning with Formal Methods, commonly known as Neuro-Symbolic Methods, have given rise to a new trend of applying rich neural architectures to solve classical combinatorial optimization problems. In this paper, we propose a neural framework that can learn to solve the Circuit Satisfiability problem. Our framework is built upon two fundamental contributions: a rich embedding architecture that encodes the problem structure, and an end-to-end differentiable training procedure that mimics Reinforcement Learning and trains the model directly toward solving the SAT problem. The experimental results show the superior out-of-sample generalization performance of our framework compared to the recently developed NeuroSAT method.
The paper makes a nice contribution to solving Circuit-SAT problem from a Neuro-Symbolic approach, particularly, 1) a novel DAG embedding with a forward layer and a reverse layer that captures the structural information of a circuit-sat input. 2) Compared with Selsam et al.'s work of Neuro-SAT, the proposed model in this paper, DG-DAGRNN, directly produces an assignment of variables, and the method is unsupervised and end-to-end differentiable. 3) Empirical experiments on random k-SAT and random graph k-coloring instances that support the authors' claim on better generalization ability.
The paper is lucid and well written, I would support its acceptance at ICLR. Though I have a few comments and questions for the authors to consider.
- In figure 1 (a), what are x11, x12, etc?
- When comparing the two approaches of Neuro-Symbolic methods, besides the angles of optimality and training cost, it is worth to mention that the first one that based on classical algorithms always has a correctness guarantee, while the second one (learning the entire solution from scratch) usually does not.
- Section 4.1, as a pure decision problem, solving SAT means that giving a yes/no answer (i.e., a classification); while for practical purposes, solving SAT means that producing a model (i.e., a witness) of the formula if it is SAT. This can be misleading for some readers when the authors mentioning "solving SAT", and it would be clear if the authors could make a distinction when using such terms.
- Section 4.1, "without requiring to see the actual SAT solutions during training", again, what is the meaning of "solutions" is not very clear at this point. Readers may realize the experiments in the paper only train with satisfiable formulae from the afterward description, so the "solutions" indicates the assignments of variables. But it would be better to make it clear.
- Section 4.1/The Evaluator Network, "one can show also show that min() < S_min() <= S_max() < max()", what is the ordering relation (i.e., < and <=) here? It is a bit confusing if a forall quantifier for inputs (a_1, ... a_n) is required here.
- Section 4.1/The Evaluator Network, how does the temperature affect the results of R_G? It would be helpful to show their dynamics.
- Section 4.1/Optimization, "if the input circuit is UNSAT, one can show that the maximum achievable values for S_\theta is 0.5", it would be better to provide a brief description of how it is guaranteed. Also, this seems to be suggesting the DG-SAGRNN solver has no false positives, i.e., it will never produce a satisfiable result for unsatisfiable formulae? This would be interesting toward some semi-correctness if the answer is yes.
- Section 5.1, are the testing data all satisfiable formulae? If yes, then the figure 2 shows there is a number of satisfiable formulae but both the models cannot produce correct results -- is that a correct understanding of figure 2? If not, then what is the ground truth?
- I would love to see more experiments on SAT instances with a moderate number of variables but from real-world applications. It would be interesting to see how the model utilizes the rich structural information of instances from real applications (instead of randomly generated formulae).
- The training time and testing time(per instance) are not reported in the experiments.