Search space structures of local search algorithms for SAT.

摘要

SAT problems are NP-Complete, which are not expected to be solved efficiently. Hence, the classic systematic search algorithms may encounter some hard instances that cannot be solved in reasonable time. However, local search algorithms may show their surprising efficiency on some of those SAT instances that are hard for classic ones. Local search procedures for SAT have become popular since the early 90's and several efficient solvers based on local search procedures have been proposed. The GSAT family and the WalkSAT family are two popular series of them. They use simple heuristics but can solve SAT instances on even thousands of variables. However, the search mechanism underlying them is still not well understood. Moreover, because of the lack of general theoretical tools for the analysis of local search algorithms, many researchers still analyze them empirically.;To understand the local search mechanism more deeply, we empirically analyzed the structure of the search spaces of local search algorithms. A search space basically represents all the possible states and moves of a local search procedure. Our research focuses on the coverage of traps and the convergence speed on search spaces. Traps consist of assignments that local search procedures should avoid. A local search procedure associated with search space graphs containing fewer traps has less chance to get stuck in traps. The convergence speed measures how fast a algorithm converges to the sinks. The solutions are a part of those sinks. Therefore, a faster convergence speed is desired. On the other hand, the convergence speed is directly affected by the average out-degree of states in search spaces. We empirically confirm the expected correlations among the coverage of traps, the average out-degree and algorithm performance through our study.