GenSATis a family of local hill-climbing procedures for solving propositional satisfiability problems.We restate it as a navigational search process performed on an N-dimensionalcube by a fictitious agent with limited lookahead. Several membersof the GenSAT family have been introduced whoseefficiency varies from the best in averagefor randomlygenerated problemsto a completefailure on the realistic, specially constrained problems, hence raising the interesting questionof understandingthe essenceof their different performance. In this paper, weshowhowweuse our navigational approachtd investigate this issue. We introduce newalgorithms that sharply focus on specific combinationsof properties of efficient GenSAT variants, and whichhelp to identify the relevance of the algorithmfeatures to the efficiencyof local search. In particular, weargue for the reasons of higher effectiveness of HSATcomparedto the original GSAT. Wealso derive fast approximating procedures based on variable weights tha...
Yury V. Smirnov, Manuela M. Veloso