Efficient branch-and-bound algorithms for weighted MAX-2-SAT

• 成果类型: Article
• 署名作者: Ibaraki, Toshihide; Imamichi, Takashi; Koga, Yuichi; Nagamochi, Hiroshi; Nonobe, Koji; Yagiura, Mutsunori
• 署名单位: Nagoya University; Kwansei Gakuin University; Kyoto University; Hosei University
• 刊物名称: MATHEMATICAL PROGRAMMING
• ISSN/ISSBN: 0025-5610
• DOI: 10.1007/s10107-009-0285-6
• 发表日期: 2011
• 页码: 297-343
• 关键词: max-sat; time algorithm; tabu search; satisfiability; optimization; heuristics

摘要

MAX-2-SAT is one of the representative combinatorial problems and is known to be NP-hard. Given a set of m clauses on n propositional variables, where each clause contains at most two literals and is weighted by a positive real, MAX-2-SAT asks to find a truth assignment that maximizes the total weight of satisfied clauses. In this paper, we propose branch-and-bound exact algorithms for MAX-2-SAT utilizing three kinds of lower bounds. All lower bounds are based on a directed graph that represents conflicts among clauses, and two of them use a set covering representation of MAX-2-SAT. Computational comparisons on benchmark instances disclose that these algorithms are highly effective in reducing the number of search tree nodes as well as the computation time.