A New Method for Solving Hard Satisfiability Problems

A New Method for Solving Hard Satisfiability Problems : GSAT : 

A New Method for Solving Hard Satisfiability Problems : GSAT Bart Selmon Hector Levesque David Mitchel 1992

Abstract : 

Abstract GSAT is a greedy local search procedure to solve propositional satisfiabilty problems. GSAT is used to solve hard , randomly generated problems of large size. GSAT performance is much better than the traditional approaches like Davis-putnam(DP) procedure or resolution.

Introduction : 

Introduction The first NP-hard problem was Propositional Satisfiability (or) SAT. [cook 1971] Though SAT is originally formulated as a Decision problem, there are two closely related search problems: 1. Model-finding 2. Theorem-proving GSAT is a Model-finding procedure.

The GSAT procedure : 

The GSAT procedure

Experimental Results : 

Experimental Results GSAT tested on different classes of formulas: Random formulas Graph coloring encodings N-queens encodings

Hard random formulas : 

Hard random formulas Random instances of CNF formulas are often used in evaluating satisfiability procedures. Some care has to be taken in sampling formulas. Formulas are generated in 2 ways: Uniform Distribution and fixed-clause length model. The hardest formulas lie around the region where there is 50% chance of randomly generated formula being satisfiable.

Hard random formulas contd… : 

Hard random formulas contd… Let N: Number of Variables, K: Literals for each clause L: Number of Clauses. The difficulty of formulas depends on ratio between N & L. For 3-CNF formulas (K=3) , L apprx.Equl to 4.3N Unsatisfiable formulas are of little interest because GSAT return in time proportional to (MAX-FLIPS * MAX-TRIES). So DP is used to select satisfiable formulas to use as test cases.

Comparision of results with DP procedure : 

Comparision of results with DP procedure

Graph coloring : 

Graph coloring Consider problem of coloring with K-colors of a Graph with V-vertices such that no two adjacent vertices have same color. Each node take any 1 of K-possible colors & must have atleast one color. Consider of the hardest instance discussed on Graph coloring.[Johnson et al 1991]

Graph coloring cotnd. : 

Graph coloring cotnd. For 125 vertex Graph: Encoding allows for 18 colors consists of 89,288 clauses & 2,250 Variables. Encoding allows for 17 colors consists of 83,272 clauses & 2,125 Variables. GSAT managed to find 18-coloring in apprx. 5 hours, but DP can not. GSAT didn’t find 17-coloring directly.

N-queens : 

N-queens One has to place N-queens on N X N chess board such that no queens attacks each other. By using standard backtracking technique solution is quite hard. But recent paper[Minton et al 1990] show one can generate solutions by starting with a random placement of queens(one in each row) in polynomial time.

N-queens contd… : 

N-queens contd… Use one variable for each of the N^2 squares on the chess board. A variable is true, when a queen is on the corresponding square.

N-queens contd… : 

N-queens contd…

Limitations : 

Limitations The following conjunction of clauses shows that GSAT can misled: (1 V ~2 V 3) ^ (1 V ~3 V 4) ^ (1 V ~4 V ~2) ^ (1 V 5 V 2) ^ (1 V ~5 V 2) ^ (~1 V ~6 V 7) ^ (~1 V ~7 V 8) ^ ……….^(~1 V ~98 V 99) ^ (~1 V ~99 V 6). GSAT is incomplete.

Applications : 

Applications Reformulate tasks that are traditionally been viewed as theorem-proving as model-finding ones. ex: formulation of planing as a model-finding task. [Kautz and selman 1992] Another potential application for GSAT is vivid representations.

Conclusions : 

Conclusions This method is simple & effective. It outperforms the DP procedure by an order of magnitude on hard random formulas. Although GSAT works well in many cases it is not complete. Here we can get some approximate solution which can be refined iteratively. So, model-finding has clear advantage over theorem-proving.

Slide 17: 

Thank You