A new bounding procedure and an improved exact algorithm for the Max-2-SAT problem

Given a CNF (conjunctive normal form) Boolean expression with clauses of size at most two, the Max-2-SAT problem asks to find a truth assignment to the Boolean variables that makes true the maximum number of clauses. In this paper, we describe an innovative upper bound computation procedure which is centered around the use of equations and inequalities that are satisfied by all solutions to the problem. The procedure is incorporated in a branch-and-bound algorithm for Max-2-SAT. An initial solution to the problem is provided by an iterated tabu search heuristic. We present computational experience on the Max-2-SAT benchmark instances from the Max-SAT Evaluation 2007. The results show that the developed branch-and-bound algorithm is very competitive with the best previously reported techniques.