@InProceedings{selman+1992,
  author       = {Selman, Bart and Levesque, Hector and Mitchell, David},
  title        = {A new method for solving hard satisfiability problems},
  booktitle    = {Proceedings of the Tenth National Conference on Artificial
                  Intelligence},
  year         = 1992,
  series       = {AAAI'92},
  pages        = {440–446},
  publisher    = {AAAI Press},
  isbn         = 0262510634,
  abstract     = {We introduce a greedy local search procedure called GSAT for
                  solving propositional satisfiability problems. Our
                  experiments show that this procedure can be used to 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 or
                  resolution. We also show that GSAT can solve structured
                  satisfiability problems quickly. In particular, we solve
                  encodings of graph coloring problems, N-queens, and Boolean
                  induction. General application strategies and limitations of
                  the approach are also discussed.GSAT is best viewed as a
                  model-finding procedure. Its good performance suggests that
                  it may be advantageous to reformulate reasoning tasks that
                  have traditionally been viewed as theorem-proving problems as
                  model-finding tasks.},
  numpages     = 7,
  location     = {San Jose, California},
  url          = {https://dl.acm.org/doi/10.5555/1867135.1867203}
}