Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems
Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence. Constraint Satisfaction Problems. Pages 290-294.
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.
@inproceedings{ijcai1993p41,
title = {Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems},
author = {Selman, Bart and Kautz, Henry A.},
booktitle = {Proceedings of the Thirteenth International Joint Conference on
Artificial Intelligence, {IJCAI-93}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Ruzena Bajcsy},
pages = {290--294},
year = {1993},
note = {Constraint Satisfaction Problems},
url = {https://ijcai.org/proceedings/1993/41},
}
TY - CPAPER TI - Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems AU - Selman, Bart AU - Kautz, Henry A. T2 - Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, IJCAI-93 PB - International Joint Conferences on Artificial Intelligence PY - 1993 SP - 290 EP - 294 UR - https://ijcai.org/proceedings/1993/41 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
