Combining local search and backtracking techniques for constraint satisfaction

Backtracking techniques are well-known traditional methods for solving many constraint satisfaction problems (CSPs), including the satisfiability (SAT) problem in the propositional logic. In recent years, it has been reported that local search techniques are very effective in solving some large-scale instances of the SAT problem. In this research, we combine the backtracking and local search techniques into a single method for solving SAT and CSPs. When setting a parameter of the method to either of its two extreme values, we obtain the ordinary backtracking procedure or the local search procedure. For some problems, if the parameter takes values in the middle of the two extremes, the new method is much more effective than either backtracking or local search. We tested the method with classical problems like the n-Queens and random SAT instances, as well as some difficult problems from finite mathematics. In particular, using the new method, we solved four open problems in design theory.