Study of Lower Bound Functions for MAX-2-SAT

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 19

Constraint Satisfaction and Satisfiability

Recently, several lower bound functions are proposed for solving the MAX-2-SAT problem optimally in a branch-and-bound algorithm. These lower bounds improve significantly the performance of these algorithms. Based on the study of these lower bound functions, we propose a new, linear-time lower bound function. We show that the new lower bound function is admissible and it is consistently and substantially better than other known lower bound functions. The result of this study is a high-performance implementation of an exact algorithm for MAX-2-SAT which outperforms any implementation of the same class.