Improving Exact Algorithms for MAX-2-SAT

We study three new techniques which will speed up the branch-and-bound algorithm for the MAX-2-SAT problem: The first technique is a new lower bound function for the algorithm and we show that the new lower bound function is consistently better than other lower bound functions. The other two techniques are based on the strongly connected components of the implication graph of a 2CNF formula: One uses the graph to simplify the formula and the other uses the graph to design a new variable ordering. The experiments show that the simplification can reduce the size of the input substantially when used in preprocessing and that the new variable ordering performs much better when the clause-to-variable ratio is less than 2. The result of this research is a high-performance implementation of an exact algorithm for MAX-2-SAT which outperforms any implementation we know about in the same category. It also shows that our MAX-2-SAT implementation is a feasible and effective tool to solve large...

• Type: Conference
• Year: 2004
• Where: AMAI
• Authors: Haiou Shen, Hantao Zhang
• Keywords: AMAI 2004, Artificial Intelligence, Branch-and-bound Algorithm, Implication Graph, Lower Bound Functions