Abstract: | Several local search algorithms for propositional satisfiability have recently been proposed which are able to solve hard random problems beyond the range of conventional backtracking procedures. in this paper, we explore the impact of focusing search in these procedures on the "unsatisfied variables"; that is, those variables will appear in clauses which are not yet satisfied. For random problems, we show that such a focus reduces the sensitivity of these procedures to their input parameters. We also observe a simple scaling law in performance. for non-random problems, we show that whilst this focus can improve performance, many problems remain difficult. We speculate that such problems will remain hard for local search unless constraint propagation techniques can be combined with hill-climbing.
|