G-93-25
Tabu Search and a Quadratic Relaxation for the Satisfiability Problem
, , and BibTeX reference
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.
Published August 1993 , 18 pages