The restart strategy can improve the effectiveness of SAT solvers for satisfiable problems. In 2002, we proposed the so-called
random jump strategy, which outperformed the restart strategy in most experiments. One weakness shared by both the restart
strategy and the random jump strategy is the ineffectiveness for unsatisfiable problems: A job which can be finished by a
SAT solver in one day cannot not be finished in a couple of days if either strategy is used by the same SAT solver. In this
paper, we propose a simple and effective technique which makes the random jump strategy as effective as the original SAT solvers.
The technique works as follows: When we jump from the current position to another position, we remember the skipped search
space in a simple data structure called “guiding path”. If the current search runs out of search space before running out
of the allotted time, the search can be recharged with one of the saved guiding paths and continues. Because the overhead
of saving and loading guiding paths is very small, the SAT solvers is as effective as before for unsatisfiable problems when
using the proposed technique.