Domain-independent extensions to GSAT: solving large structured satisfiability problems

GSAT is a randomized local search procedure for solving propositional satisfiability problems (Selman et al. 1992). GSAT can solve hard, randomly generated problems that are an order of magnitude larger than those that can be handled by more traditional approaches such as the Davis-Putnam procedure. GSAT also efficiently solves encodings of graph coloring problems, N-queens, and Boolean induction. However, GSAT does not perform as well on handcrafted encodings of blocks-world planning problems and formulas with a high degree of asymmetry. We present three strategies that dramatically improve GSAT's performance on such formulas. These strategies, in effect, manage to uncover hidden structure in the formula under considerations, thereby significantly extending the applicability of the GSAT algorithm.