Variable Selection with PageRank for SAT Solvers

Abstract

How to choose decision variables often determines the performance of SAT solvers. In state-of-the-art SAT solvers, Variable State Independent Decaying Sum (VSIDS) has been used as a standard technique in the decision process. In this study, we analyze the VSIDS from the point of view of PageRank and propose a technique for improving the VSIDS. While the VSIDS focuses on local search spaces, the PageRank values are based on the relative importance from a global point of view. From this fact, we utilize the PageRank values for controlling the VSIDS and improve the performances of representative SAT solvers, MiniSAT and Glucose.