A Two-Phase Exact Algorithm for MAX-SAT and Weighted MAX-SAT Problems

被引：71

作者：

Borchers B. ^{[1
]}

Furman J. ^{[2
]}

机构：

[1] Mathematics Department, New Mexico Tech., Socorro

[2] Department of Mathematical Sciences, Clemson University, Clemson

来源：

Journal of Combinatorial Optimization | 1998年 / 2卷 / 4期

关键词：

Mathematical Modeling; Industrial Mathematic; Integer Programming; Discrete Geometry; Search Tree;

D O I：

10.1023/A:1009725216438

中图分类号：

学科分类号：

摘要：

We describe a two-phase algorithm for MAX-SAT and weighted MAX-SAT problems. In the first phase, we use the GSAT heuristic to find a good solution to the problem. In the second phase, we use an enumeration procedure based on the Davis-Putnam-Loveland algorithm, to find a provably optimal solution. The first heuristic stage improves the performance of the algorithm by obtaining an upper bound on the minimum number of unsatisfied clauses that can be used in pruning branches of the search tree. We compare our algorithm with an integer programming branch-and-cut algorithm. Our implementation of the two-phase algorithm is faster than the integer programming approach on many problems. However, the integer programming approach is more effective than the two-phase algorithm on some classes of problems, including MAX-2-SAT problems.

引用

页码：299 / 306

页数：7

共 20 条

[1]

Blair, C.E., Jeroslow, R.G., Lowe, J.K., Some results and experiments in programming techniques for propositional logic (1986) Computers and Operations Research, 13 (5), pp. 633-645

[2]

Cheriyan, J., Cunningham, W.H., Tunçel, L., Wang, Y., A linear programming and rounding approach to max 2-sat (1996) Cliques, Coloring, and Satisfiability, 26, pp. 395-414. , D.S. Johnson and M.A. Trick (Eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS

[3]

Davis, M., Putnam, H., A computing procedure for quantification theory (1960) Journal of the Association for Computing Machinery, 7, pp. 201-215

[4]

Garey, M.R., Johnson, D.S., (1979) Computers and Intractability: A Guide to the Theory of NP-Completeness, , W. H. Freeman and Company: New York

[5]

Goemans, M.X., Williamson, D.P., Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming (1995) Journal of the ACM, 42, pp. 1115-1145

[6]

Hansen, P., Jaumard, B., Algorithms for the maximum satisfiability problem (1990) Computing, 44, pp. 279-303

[7]

Harche, F., Thompson, G.L., The column subtraction algorithm, an exact method for solving weighted set covering packing and partitioning problems (1990) Computers and Operations Research, 21, pp. 689-705

[8]

Hooker, J.N., Resolution vs. cutting plane solution of inference problems: Some computational experience (1988) Operations Research Letters, 7 (1), pp. 1-7

[9]

Hooker, J.N., Fedjki, C., Branch-and-cut solution of inference problems in propositional logic (1990) Annals of Mathematics and Artificial Intelligence, 1, pp. 123-139

[10]

Jeroslow, R.E., Wang, J., Solving propositional satisfiability problems (1990) Annals of Mathematics and AI, 1, pp. 167-187

← 1 2 →