Improving exact algorithms for MAX-2-SAT

被引:0
作者
Haiou Shen
Hantao Zhang
机构
[1] The University of Iowa,Computer Science Department
来源
Annals of Mathematics and Artificial Intelligence | 2005年 / 44卷
关键词
propositional satisfiability; maximum satisfiability; exact algorithms;
D O I
暂无
中图分类号
学科分类号
摘要
We study three new techniques that will speed up the branch-and-bound algorithm for the MAX-2-SAT problem: The first technique is a group of new lower bound functions for the algorithm and we show that these functions are admissible and consistently better than other known 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 no matter what is the clause-to-variable ratio and that the new variable ordering performs much better when the clause-to-variable ratio is less than 2. A direct outcome 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. We also show that our implementation is a feasible and effective tool to solve large instances of the Max-Cut problem in graph theory.
引用
收藏
页码:419 / 436
页数:17
相关论文
共 29 条
  • [1] Aspvall B.(1979)A linear-time algorithm for testing the truth of certain quantified Boolean formulas Information Processing Letters 8 121-123
  • [2] Plass M.F.(1999)A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems Journal of Combinatorial Optimization 2 299-306
  • [3] Tarjan R.E.(2002)A deterministic (2−2/( Theoretical Computer Science 289 69-83
  • [4] Borchers B.(1962)+1)) Communications of the Association for Computing Machinery 7 394-397
  • [5] Furman J.(1960) algorithm for Mat. Kutato Int. Kozl. 5 17-61
  • [6] Dantsin E.(2003)-SAT based on local search Discrete Applied Mathematics 130 139-155
  • [7] Goerdt A.(1990)A machine program for theorem-proving Computing 44 279-303
  • [8] Hirsch E.A.(2000)On the evolution of random graphs Journal of Automated Reasoning 24 397-420
  • [9] Kannan R.(1999)Worst-case upper bounds for MAX-2-SAT with application to MAX-CUT Journal of Algorithms 31 335-354
  • [10] Kleinberg J.(2000)Algorithms for the maximum satisfiability problem Journal of Algorithms 36 63-88