AsymSAT: Accelerating SAT Solving with Asymmetric Graph-based Model Prediction

Abstract

The Boolean satisfiability problem (SAT) is the foundational problem in electronic design automation (EDA). Recent efforts have explored the use of graph neural networks (GNNs) in SAT solving.However, for a subset of symmetric SAT problems, we unveil that the current GNN-based end-to-end SAT solvers are bound to yield incorrect outcomes as they are unable to break symmetry in variable assignments, while symmetric structure is prevalent in logic circuits such as miter circuits for equivalence checking and cryptographic circuits with XOR gates. In response, we introduce AsymSAT, an innovative GNN architecture coupled with recurrent neural networks (RNNs) to produce asymmetric models. Moreover, we bring up a method to integrate machine-learning-based SAT assignment prediction with classic SAT solvers and demonstrate its advantage on non-trivial SAT instances including logic equivalence checking and cryptographic analysis with an average of 75.45% speed-up.

Zhiyuan Yan

Ph.D. student in Microelectronics Thrust

My research interests include hardware formal verification, AI for EDA and Boolean Satisfiability Problem.