Home / Computer science / GWSAT
Citation
Selman and Kautz (1993):
@InProceedings{selman+1993,
author = {Selman, Bart and Kautz, Henry},
title = {Domain-independent extensions to {GSAT}},
booktitle = {Proceedings of the 13th International Joint Conference on
Artifical Intelligence - Volume 1},
year = 1993,
series = {IJCAI'93},
pages = {290-295},
address = {San Francisco, CA, USA},
publisher = {Morgan Kaufmann Publishers Inc.},
subtitle = {Solving large structured satisfiability problems},
abstract = {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.},
numpages = 6,
location = {Chambery, France}
}