SOLVING THE WEIGHTED MAX-2-SAT PROBLEM WITH ITERATED TABU SEARCH

Given a CNF formula in which each clause is of length at most two and has an associated positive weight, the weighted Max-2-SAT problem asks to find a truth assignment to the Boolean variables that maximizes the total weight of the satisfied clauses. We develop an iterated tabu search (ITS) algorithm for solving this problem. We report computational results on Max-2-SAT instances of size up to 3000 variables and provide comparisons of ITS to state-of-the-art heuristic methods from the literature, which demonstrate the competitiveness of our approach.