Accerlating Constraint Solving in Symbolic Execution by CNN

Boolean satisfiability (SAT) is one of the most well-known NP-complete problems and has been extensively studied. State-of-the-art solvers exist and have found a wide range of applications. However, they still do not scale well to formulas with hundreds of variables for uniform 3-SAT problems. To tackle this scalability challenge, we introduce CNNSAT, a fast and accurate statistical decision procedure for SAT based on convolutional neural networks. CNNSAT’s effectiveness is due to a precise and compact representation of Boolean formulas. On both real and synthetic formulas, CNNSAT is highly accurate and orders of magnitude faster than the state-of-the-art solvers in predicting satisfiability.

We also extend CNNSAT to predict the satisfiability of constraints in symbolic execution, which accelerates the constraint solving in symbolic execution, because most unsatisfiable constraints are skipped.