We propose GVE(Glue Variables Elimination), an algorithm that organically combines neural networks with a deterministic solver to solve SAT(Boolean satisfiability problem) in the filed of linguistics. It gives full play to their respective advantages by following steps: (a) applying a graph learning algorithm to learn the structure of the CNF formula; (b) finding the glue variables of the problem; (c) determining their values; (d) simplifying the original formula; (e) using a deterministic solver to solve the simplified problem. We use SATCOMP 2003-2019 benchmarks as the test data sets, and compare our model with the SAT solver CADICAL that has performed well in SATCOMP 2019 as well as the neural network model PDP proposed in recent years. GVE model shows good performance. As the complexity of the problem increases, the solution time can be about 20%-95% quicker than the deterministic solver, while at the same time around 72% more accurate than PDP model.
Ziwei Zhang, Beijing University of Posts and Telecommunications, China
Yang Zhang, Beijing University of Posts and Telecommunications, China
This paper is part of the ACL2021 Conference Proceedings (View)
View / Download the full paper in a new tab/window