NeuroSAT, A Graph Neural Network Based Predictor for SAT Problem

In theoretical research and practical applications, boolean satisfiability is the most studied combinatorial optimization problem. In the last few years, enormous progress has been made on practical SAT solvers despite exponential runtime algorithms in software and hardware verification, challenging algebraic problems and many more.

On the other hand, machine learning and deep neural networks are opening new doors to solving data validation problems, risk management, pattern recognition, and almost every problem in the business sector day by day. We still do not know what we can do with artificial neural networks. As a result, many researchers try to understand the extent to which Artificial Intelligence(AI) can understand the propositional logic of boolean satisfiability problems.

This study will explore a Graph Neural Network (GNN) based SAT solver named “NeuroSAT.” Moreover, we will look for the answers that whether its architecture can perform a discrete search on its own after end-to-end training with minimal supervision or not and what contribution it makes to the SAT community.