Solving Dynamic 3-SAT Formula: An Empirical Study

The SAT problem is a well-known NP-complete problem and has an immense range of applications including information security. Many SAT problems are always dynamically changing and we might solve them from a fresh start point or based on previous solutions. That is, the restarting strategy and the resuming strategy. In this paper, both basic strategies for solving dynamic 3-SAT formulas are compared and discussed. For experimental comparisons, a framework that transfers an existing 3-SAT formula generating algorithm to a dynamic SAT formula generating algorithm is given. The experiments and analysis show these two basic strategies have their advantages according to the changing severity of specific dynamic SAT formulas. Interestingly, when the SAT formula does not dramatically change, a weak SAT solver with the resuming strategy might have better performance than a recent solver with the restating strategy. Considering many state-of-the-art SAT solvers do not facilitate the previous solutions, we argue that it is very significant to pay more attention to SAT solvers with the resuming strategy.