Groupe d’études et de recherche en analyse des décisions

G-93-25

Tabu Search and a Quadratic Relaxation for the Satisfiability Problem

, et

We propose a new branch-and-bound algorithm for the Satisfiability problem (SAT). A relaxation as well as a decomposition scheme are defined by using polynomial instances, i.e., 2-satisfiability and Horn satisfiability. A specialized Tabu Search type heuristic is included to speed up the search for a solution (if there is one). Experimental results are reported as well as computational comparisons with some of the most efficient algorithms of the literature.

, 18 pages