A Two-Phase Exact Algorithm for MAX-SAT and Weighted MAX-SAT Problems
Tóm tắt
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.
Tài liệu tham khảo
C.E. Blair, R.G. Jeroslow, and J.K. Lowe, “Some results and experiments in programming techniques for propositional logic,” Computers and Operations Research, vol. 13, no.5, pp. 633–645, 1986.
J. Cheriyan, W.H. Cunningham, L. Tuncçl, and Y. Wang, “A linear programming and rounding approach to max 2–sat,” in Cliques, Coloring, and Satisfiability, D.S. Johnson and M.A. Trick (Eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, 1996, vol. 26, pp. 395–414.
M. Davis and H. Putnam, “A computing procedure for quantification theory,” Journal of The Association for Computing Machinery, vol. 7, pp. 201–215, 1960.
M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman and Company: New York, 1979.
M.X. Goemans and D.P. Williamson, “Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming,” Journal of the ACM, vol. 42, pp. 1115–1145, 1995.
P. Hansen and B. Jaumard, “Algorithms for the maximum satisfiability problem,” Computing, vol. 44, pp. 279–303, 1990.
F. Harche and G.L. Thompson, “The column subtraction algorithm, an exact method for solving weighted set covering packing and partitioning problems,” Computers and Operations Research, vol. 21, pp. 689–705, 1990.
J.N. Hooker, “Resolution vs. cutting plane solution of inference problems: Some computational experience,” Operations Research Letters, vol. 7, no.1, pp. 1–7, 1988.
J.N. Hooker and C. Fedjki, “Branch-and-cut solution of inference problems in propositional logic,” Annals of Mathematics and Artificial Intelligence, vol. 1, pp. 123–139, 1990.
R.E. Jeroslow and J. Wang, “Solving propositional satisfiability problems,” Annals of Mathematics and AI, vol. 1, pp. 167–187, 1990.
Y. Jiang, H. Kautz, and B. Selman, “Solving problems with hard and soft constraints using a stochastic algorithm for MAX-SAT,” presented at the First International Joint Workshop on Artificial Intelligence and Operations Research, Timberline, OR, 1995.
S. Joy, J.E. Mitchell, and B. Borchers, “A branch-and-cut algorithm for MAX-SAT and weighted MAX-SAT,” in Proceedings of the DIMACS Workshop on Satisfiability: Theory and Applications, 1996, to appear.
D. Loveland, Automated Theorem-Proving: A Logical Basis, North Holland: New York, 1978.
G.L. Nemhauser, M.W.P. Savelsbergh, and G.C. Sigismondi, “MINTO, a Mixed INTeger Optimizer,” Operations Research Letters, vol. 15, no.1, pp. 47–58, 1994.
C.H. Papadimitriou and M. Yannakakis, “Optimization, approximation, and complexity classes,” Journal of Computers and System Sciences, vol. 43, pp. 425–440, 1991.
M.G.C. Resende and T.A. Feo, “A GRASP for satisfiability,” in Cliques, Coloring, and Satisfiability, D.S. Johnson and M.A. Trick (Eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, 1996, vol. 26, pp. 499–520.
J.A. Robinson, “A machine-oriented logic based on the resolution principle,” Journals of The Association for Computing Machinery, vol. 12, no.1, pp. 23–41, 1965.
B. Selman and H.A. Kautz, “An empirical study of greedy local search for satisfiability testing,” in Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI-93), Washington, DC, 1993, pp. 46–51.
B. Selman, H. Levesque, and D. Mitchell, “A new method for solving hard satisfiability problems,” in Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), San Jose, CA, 1992, pp. 440–446.
R.J. Wallace and E.C. Freuder, “Comparitive studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems,” in Cliques, Coloring, and Satisfiability, D.S. Johnson and M.A. Trick (Eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, AMS, 1996, vol. 26, pp. 587–615.