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.
Paru en août 1993 , 18 pages