A GRASP for Satisfiability

Mauricio G.C. Resende and Thomas A. Feo

Extended version of paper in Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, David S. Johnson and Michael A. Trick ,Eds., DIMACS Series on Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, vol. 26, pp. 499-520, 1996


A greedy randomized adaptive search procedure (GRASP) is a randomized heuristic that has been shown to quickly produce good quality solutions for a wide variety of combinatorial optimization problems. In this paper, we describe a Grasp for the satisfiability (SAT) problem.  This algorithm can be also directly applied to both the weighted and unweighted versions of the maximum satisfiability (MAX-SAT) problem.  We review basic concepts of Grasp:  construction and local search algorithms.  The implementation of Grasp for the SAT problem is described in detail.  Computational experience on a large set of test problems is presented.

PostScript file of full paper
Go back
Mauricio G.C. Resende's Home Page
Last modified: 28 June 2002

Copyright Notice