This paper discusses the well-known nondeterministic polynomial time (NP) complete combinatorial and decision problems: the Boolean satisfiability (SAT) and the maximum satisfiability (Max-SAT = k-SAT) set of clauses of some literals (k variables) that can be set to true or false.
It is well known that local search algorithms are the most suitable techniques to solve hard SAT instances, since no known polynomial algorithm for these problems exists. However, local search algorithms are incomplete satisfaction search methods, which means that they cannot tell us there is no solution for a given SAT instance when such a solution doesn’t exist.
Zhang proposes a heuristic technique, called backbone-guided search, that improves the performance of the well-known local search algorithm WalkSAT, in solving large SAT instances. It allows the algorithm to reach a high quality local minimum, not very far from an optimal solution. Many experiments have been conducted to show the performance of the backbone heuristic with the WalkSAT local search algorithm to solve SAT instances. I think the author should compare his WalkSAT backbone with Tabu search, Ant techniques, and genetic algorithms, used successfully to solve hard SAT instances, to see if his approach is better than these techniques. In fact, WalkSAT is a relatively old technique to solve large SAT instances. I encourage the author to try to see how we can integrate his backbone heuristic with other optimization techniques.
The paper is well written and well structured. It is relatively easy to understand, even for a nonspecialist. I enjoyed reading this paper, and appreciate the efforts of the author to explain his ideas.