Recent efforts to combine Representation Learning with Formal Methods, commonly known as the 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. Recent advances in neural network models for discrete structures have given rise to a new field in Representation Learning known as the Neuro-Symbolic methods. Generally speaking, these methods aim at marrying the classical symbolic techniques in Formal Methods and Computer Science to Deep Learning in order to benefit both disciplines. One of the most exciting outcomes of this marriage is the emergence of neural models for learning how to solve the classical combinatorial optimization problems in Computer Science. The key observation behind many of these models is that in practice, for a given class of combinatorial problems in a specific domain, the problem instances are typically drawn from a certain (unknown) distribution. Therefore if a sufficient number of problem instances are available, then in principle, Statistical Learning should be able to extract the common structures among these instances and produce meta-algorithms (or models) that would, in theory, outperform the carefully hand-crafted algorithms.There have been two main approaches to realize this idea in practice. In the first group of methods, the general template of the solver algorithm (which is typically the greedy strategy) is directly imported from the classical heuristic search algorithm, and the Deep Learning component is only tasked to learn the optimal heuristics within this template. In combination with Reinforcement Learning, such strategy has been shown to be quite effective for various NP-complete problems -e.g. BID16 . Nevertheless, the resulted model is bounded by the greedy strategy, which is sub-optimal in general. The alternative is to go one step further and let Deep Learning figure out the entire solution structure from scratch. This approach is quite attractive as it allows the model not only learn the optimal (implicit) decision heuristics but also the optimal search strategies beyond the greedy strategy. However, this comes at a price: training such models can be quite challenging! To do so, a typical candidate is Reinforcement Learning (Policy Gradient, in specific), but such techniques are usually sample inefficient -e.g. BID4 . As an alternative method for training, more recently BID24 have proposed using the latent representations learned for the binary classification of the Satisfiability (SAT) problem to actually produce a neural SAT solver model. Even though using such proxy for learning a SAT solver is an interesting observation and provides us with an end-to-end differentiable architecture, the model is not directly trained toward solving a SAT problem (unlike Reinforcement Learning). As we will see later in this paper, that can indeed result in poor generalization and sub-optimal models.In this paper, we propose a neural Circuit-SAT solver framework that effectively belongs to the second class above; that is, it learns the entire solution structure from scratch. More importantly, to train such model, we propose a training strategy that, unlike the typical Policy Gradient, is differentiable end-toend, yet it trains the model directly toward the end goal (similar to Policy Gradient). Furthermore, our proposed training strategy enjoys an Explore-Exploit mechanism for better optimization even though it is not exactly a Reinforcement Learning approach.The other aspect of building neural models for solving combinatorial optimization problems is how the problem instance should be represented by the model. Using classical architectures like RNNs or LSTMs completely ignores the inherent structure present in the problem instances. For this very reason, there has been recently a strong push to employ structure-aware architectures such as different variations of neural graph embedding. Most neural graph embedding methodologies are based on the idea of synchronously propagating local information on an underlying (undirected) graph that represents the problem structure. The intuition behind using local information propagation for embedding comes from the fact that many original combinatorial optimization algorithms can actually be seen propagating information. In our case, since we are dealing with Boolean circuits and circuit are Directed Acyclic Graphs (DAG), we would need an embedding architecture that take into account the special architecture of DAGs (i.e. the topological order of the nodes). In particular, we note that in many DAG-structured problems (such as circuits, computational graphs, query DAGs, etc.), the information is propagated sequentially rather than synchronously, hence a justification to have sequential propagation for the embedding as well. To this end, we propose a rich embedding architecture that implements such propagation mechanism for DAGs. As we see in this paper, our proposed architecture is capable of harnessing the structural information in the input circuits. To summarize, our contributions in this work are three-fold:(a ) We propose a general, rich graph embedding architecture that implements sequential propagation for DAG-structured data. ( b) We adapt our proposed architecture to design a neural Circuit-SAT solver which is capable of harnessing structural signals in the input circuits to learn a SAT solver. (c) We propose a training strategy for our architecture that is end-to-end differentiable, yet similar to Reinforcement Learning techniques, it directly trains our model toward solving the SAT problem with an Explore-Exploit mechanism.The experimental results show the superior performance of our framework especially in terms of generalizing to new problem domains compared to the baseline. In this paper, we proposed a neural framework for efficiently learning a Circuit-SAT solver. Our methodology relies on two fundamental contributions: (1) a rich DAG-embedding architecture that implements the sequential propagation mechanism on DAG-structured data and is capable of learning useful representations for the input circuits, and (2) an efficient training procedure that trains the DAGembedding architecture directly toward solving the SAT problem without requiring SAT/UNSAT labels in general. Our proposed training strategy is fully differentiable end-to-end and at the same time enjoys many features of Reinforcement Learning such as an Explore-Exploit mechanism and direct training toward the end goal.As our experiments showed, the proposed embedding architecture is able to harness structural information in the input DAG distribution and as a result solve the test SAT cases in a fewer number of iterations compared to the baseline. This would also allow us to inject domain-specific heuristics into the circuit structure of the input data to obtain better models for that specific domain. Moreover, our direct training procedure as opposed to the indirect, classification-based method in NeuroSAT enables our model to generalize better to out-of-sample test cases, as demonstrated by the experiments. This superior generalization got even more expressed as we transferred the trained models to a complete new domain (i.e. graph coloring). Furthermore, we argued that not only does direct training give us superior out-of-sample generalization, but it is also essential for the problem domains where we cannot enforce the strict training regime where SAT and UNSAT cases come in pairs with almost identical structures, as proposed by BID24 .Future efforts in this direction would include closely examining the SAT solver algorithm learned by our framework to see if any high-level knowledge and insight can be extracted to further aide the classical SAT solvers. Needless to say, this type of neural models have a long way to go in order to compete with industrial SAT solvers; nevertheless, these preliminary results are promising enough to motivate the community to pursue this direction.
We propose a neural framework that can learn to solve the Circuit Satisfiability problem from (unlabeled) circuit instances.
{"src": "scitldr-AIC_train", "paper_id": "BJxgz2R9t7"}