Goal-Aware Neural SAT Solver
This work addresses the limitation of neural networks in problem-solving tasks like Boolean Satisfiability, offering a method to enhance performance through iterative feedback, though it is incremental in its application to a specific domain.
The authors tackled the problem of neural networks relying solely on input values by proposing a query mechanism that allows networks to make solution trials and receive loss feedback at runtime, demonstrating this approach with QuerySAT, a neural SAT solver that outperforms neural baselines on various SAT tasks.
Modern neural networks obtain information about the problem and calculate the output solely from the input values. We argue that it is not always optimal, and the network's performance can be significantly improved by augmenting it with a query mechanism that allows the network at run time to make several solution trials and get feedback on the loss value on each trial. To demonstrate the capabilities of the query mechanism, we formulate an unsupervised (not depending on labels) loss function for Boolean Satisfiability Problem (SAT) and theoretically show that it allows the network to extract rich information about the problem. We then propose a neural SAT solver with a query mechanism called QuerySAT and show that it outperforms the neural baseline on a wide range of SAT tasks.