Gensat: A navigational approach

GenSAT is a family of local hill-climbing procedures for solving propositional satisfiability problems. We restate it as a navigational search process performed on an N-dimensional cube by a fictitious agent with limited lookahead. Several members of the GenSAT family have been introduced whose efficiency varies from the best in average for randomly generated prob-lems to a complete failure on the realistic, specially constrained problems, hence raising the interesting question of understanding the essence of their different performance. In this paper, we show how we use our navigational approach td investigate this issue. We introduce new algorithms that sharply focus on spe-cific combinations of properties of efficient GenSAT variants, and which help to identify the relevance of the algorithm features to the efficiency of local search. In particular, we argue for the reasons of higher ef-fectiveness of HSAT compared to the original GSAT. We also derive fast approximating procedures based on variable weights that can provide good switching points for a mixed search policy. Our conclusions are validated by empirical evidence obtained from the ap-plication of several GenSAT variants to random 3SAT problem instances and to simple navigational prob-lems