A new method for solving hard satisfiability problems

TLDR

GSAT is best viewed as a model‑finding procedure. The authors introduce GSAT, a greedy local search procedure for propositional satisfiability, and discuss its general application strategies and limitations. GSAT is a greedy local search procedure that solves propositional satisfiability problems, applied to encodings of graph coloring, N‑queens, and Boolean induction. Experiments show GSAT solves hard, randomly generated satisfiability problems an order of magnitude larger than those handled by traditional methods, quickly solves structured problems, and its good performance suggests reformulating theorem‑proving tasks as model‑finding tasks.

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.