Learning to Solve Circuit-SAT: An Unsupervised Differentiable Approach
Abstract
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.
Cite
Text
Amizadeh et al. "Learning to Solve Circuit-SAT: An Unsupervised Differentiable Approach." International Conference on Learning Representations, 2019.Markdown
[Amizadeh et al. "Learning to Solve Circuit-SAT: An Unsupervised Differentiable Approach." International Conference on Learning Representations, 2019.](https://mlanthology.org/iclr/2019/amizadeh2019iclr-learning/)BibTeX
@inproceedings{amizadeh2019iclr-learning,
title = {{Learning to Solve Circuit-SAT: An Unsupervised Differentiable Approach}},
author = {Amizadeh, Saeed and Matusevych, Sergiy and Weimer, Markus},
booktitle = {International Conference on Learning Representations},
year = {2019},
url = {https://mlanthology.org/iclr/2019/amizadeh2019iclr-learning/}
}