An Incremental Branch-and-Bound Method for the Satisfiability Problem
Hachemi Bennaceur, Idir Gouachi, Gérard Plateau
INFORMS Journal on Computing · 1998 · Volume 10 · Issue 3
Abstract
The satisfiability problem is to check whether a set of clauses in propositional logic is satisfiable. If it is satisfiable, the incremental satisfiability problem is then to check whether satisfiability remains given additional clauses. This paper deals with an incremental branch-and-bound method which solves exactly both problems. This method includes flexible Lagrangean relaxations, metaheuristics, and judicious jumping back. This leads to an efficient implementation which compares favorably with the classical Davis-Putnam-Loveland procedure and its incremental version designed by Hooker. Numerous computational results are detailed.
Keywords
Satisfiability problem, branch and bound, integer programming
Enable JavaScript for citation tools and additional paper interactions.