On EDA-Driven Learning for SAT Solving
DescriptionWe present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem. Unlike existing solutions trained on random SAT instances with relatively weak supervision, we propose applying the knowledge of the well-developed electronic design automation (EDA) field for SAT solving. Specifically, we first resort to logic synthesis algorithms to pre-process SAT instances into optimized and-inverter graphs. Next, we regard the distribution of SAT solutions being a product of conditional Bernoulli distributions. We approximate SAT solving procedure with a conditional generative model, leveraging a novel directed acyclic graph neural network (DAGNN) with two polarity prototypes for conditional SAT modeling.
TimeTuesday, July 11th3:40pm - 3:55pm PDT
Location3004, 3rd Floor