Learning a SAT Solver from Single-Bit Supervision https://arxiv.org/abs/1802.03685 graph convolution っぽいモデルでSAT問題のSAT/UNSATの予測を学習。

SATな場合には変数のembeddingがクラスタになっていて、一方に真を他方に偽を割り当てるような割り当てを試すと、大体正しい解になってる。 同じモデルで別のデータで学習した場合、変数のembeddingから unsat core の情報を復元できた。

ただ、メッセージパッシングの段数の多さの割に、学習しやすくする工夫が layer nomalization くらいしか入ってなくて、これだけで本当に学習できるのかという気はする……

TensorFlow実装: https://github.com/dselsam/neurosat/