A new method for solving hard satisfiability problems Export

@misc{citeulike:3384922, 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.}, author = {Selman, Bart and Levesque, Hector and Mitchell, David}, citeulike-article-id = {3384922}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4724}, keywords = {algorithm}, pages = {440--446}, posted-at = {2008-10-08 02:41:15}, priority = {2}, title = {A new method for solving hard satisfiability problems}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4724}, year = {1992} }

TY - ELEC ID - citeulike:3384922 L3 - citeulike-article-id:3384922 N2 - 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. EP - 446 TI - A new method for solving hard satisfiability problems SP - 440 KW - algorithm AU - Selman, Bart AU - Levesque, Hector AU - Mitchell, David PY - 1992/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4724 ER -