Faster exact solutions for Max2Sat

Abstract

Given a boolean 2CNF formula F, the Max2Sat problem is that of finding the maximum number of clauses satisfiable simultaneously. In the corresponding decision version, we are given an additional parameter k and the question is whether we can simultaneously satisfy at least k clauses. This problem is NP-complete. We improve on known upper bounds on the worst case running time of Max2Sat, implying also new upper bounds for Maximum Cut. In particular, we give experimental results, indicating the practical relevance of our algorithms.