Goal-Aware Neural SAT Solver

TL;DR

This paper introduces QuerySAT, a neural SAT solver with a query mechanism that improves problem-solving by allowing multiple solution trials and feedback, outperforming baseline models on various SAT tasks.

Contribution

The paper proposes a novel query mechanism for neural networks applied to SAT solving, enabling iterative problem-solving and feedback integration to enhance performance.

Findings

QuerySAT outperforms neural baseline on SAT tasks

Unsupervised loss function enables rich problem information extraction

Query mechanism improves neural network problem-solving capabilities

Abstract

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.