On Formula Embeddings in Neural-Guided SAT Solving

Abstract

Branching heuristics determine the performance of search-based SAT solvers. We note that recently, Neural Machine Learning approaches have been proposed to learn such heuristics from data. The first step in learning a branching heuristic is a transformation from the space of Boolean formulas to a vector space. We note that there is no canonical transformation: techniques such as message-passing networks and LSTMs have been proposed to embed formulas into R^n. We build a novel dataset of an approximate optimal heuristic and compare the estimation performance of models with different embedding methods. We show that for performant models, embedding methods need to represent the structural invariances of Boolean formulas: similar to CNNs and spatially local data such as images.