×

zbMATH — the first resource for mathematics

Sums of squares based approximation algorithms for MAX-SAT. (English) Zbl 1152.68058
Summary: We investigate the Semidefinite Programming based sums of squares (SOS) decomposition method, designed for global optimization of polynomials, in the context of the (Maximum) Satisfiability problem. To be specific, we examine the potential of this theory for providing tests for unsatisfiability and providing MAX-SAT upper bounds. We compare the SOS approach with existing upper bound and rounding techniques for the MAX-2-SAT case of M. X. Goemans and D. P. Williamson [“Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming”, J. Assoc. Comput. Mach. 42, No. 6, 1115–1145 (1995; Zbl 0885.68088)] and U. Feige and M. X. Goemans [“Approximating the value of two prover proof systems, with applications to MAX2SAT and MAXDICUT”, in: Proceedings of the Third Israel Symposium on Theory of Computing and Systems. 182–189 (1995)] and the MAX-3-SAT case of H. Karloff and U. Zwick [“A 7/8-approximation algorithm for MAX 3SAT?”, in: Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, Miami Beach, FL, USA, IEEE Press, New York (1997)], which are based on Semidefinite Programming as well. We prove that for each of these algorithms there is an SOS-based counterpart which provides upper bounds at least as tight, but observably tighter in particular cases. Also, we propose a new randomized rounding technique based on the optimal solution of the SOS Semidefinite Program (SDP) which we experimentally compare with the appropriate existing rounding techniques. Further we investigate the implications to the decision variant SAT and compare experimental results with those yielded from the higher lifting approach of M. F. Anjos [“On semidefinite programming relaxations for the satisfiability problem”, Math. Methods Oper. Res. 60, No. 3, 349–367 (2004; Zbl 1087.90056); “An improved semidefinite programming relaxation for the satisfiability problem”, Math. Program. 102A, No. 3, 589–608 (2005; Zbl 1059.90117); “Semidefinite optimization approaches for satisfiability and maximum-satisfiability problems”, J. Satisf. Boolean Model. Comput. 1, No. 1, 1–47 (2006; Zbl 1194.90064)].
We give some impression of the fraction of the so-called unit constraints in the various SDP relaxations. From a mathematical viewpoint these constraints should be easily dealt within an algorithmic setting, but seem hard to be avoided as extra constraints in an SDP setting. Finally, we briefly indicate whether this work could have implications in finding counterexamples to uncovered cases in Hilbert’s Positivstellensatz.

MSC:
68W25 Approximation algorithms
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
90C22 Semidefinite programming
Software:
COL; CSDP; MAX-2-SAT; SDPA; SeDuMi
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Anjos, M.F., On semidefinite programming relaxations for the satisfiability problem, Math. methods oper. res., 60, 3, 349-367, (2004) · Zbl 1087.90056
[2] Anjos, M.F., An improved semidefinite programming relaxation for the satisfiability problem, Math. programming, 102, 3, 589-608, (2005) · Zbl 1059.90117
[3] Anjos, M.F., Semidefinite optimization approaches for satisfiability and maximum-satisfiability problems, J. satisfiability Boolean modeling comput., 1, 1-47, (2005) · Zbl 1194.90064
[4] Benson, S.J.; Ye, Y.; Zhang, X., Solving large-scale sparse semidefinite programs for combinatorial optimization, SIAM J. optim., 10, 2, 443-461, (2000) · Zbl 0997.90059
[5] Blekherman, G., There are significantly more nonnegative polynomials than sums of squares, Israel J. math., 153, 355, (2005) · Zbl 1139.14044
[6] B. Borchers, CSDP: a C library for semidefinite programming, Technical Report, New Mexico Tech, 1997. · Zbl 0973.90524
[7] Borchers, B.; Furman, J., A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems, J. combin. optim., 2, 4, 299-306, (1999) · Zbl 0954.90026
[8] E. de Klerk, Aspects of Semidefinite Programming: Interior Point Algorithms and Selected Applications, Applied Optimization Series, vol. 65, Kluwer Academic Publishers, Dordrecht, 2002. · Zbl 0991.90098
[9] E. de Klerk, J.P. Warners, Semidefinite programming relaxations for MAX 2-SAT and 3-SAT: computational perspectives, in: P.M. Pardalos, A. Migdalas, R.E. Burkard (Eds.), Combinatorial and Global Optimization, Series on Applied Optimization, vol. 14, World Scientific Publishers, Singapore, 2002. · Zbl 1029.90053
[10] Feige, U.; Goemans, M.X., Approximating the value of two prover proof systems, with applications to MAX2SAT and MAXDICUT, (), 182-189
[11] K. Fujisawa, M. Kojima, K. Nakata, M. Yamashita, SDPA (Semidefinite Programming Algorithm): user’s manual, Research Reports on Information Sciences, Series B: Operations Research B 308, Department of Information Sciences, Tokyo Institute of Technology, Oh-Okayama, Meguro-ku, Tokyo, Japan, 2002.
[12] Goemans, M.X.; Williamson, D.P., Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. assoc. comput. Mach., 42, 6, 1115-1145, (1995) · Zbl 0885.68088
[13] HĂ…stad, J., Some optimal inapproximability results, J. assoc. comput. Mach., 48, 798-859, (2001) · Zbl 1127.68405
[14] Karloff, H.; Zwick, U., A 7/8-approximation algorithm for MAX 3SAT?, ()
[15] Knuth, D.E., The art of computer programming, vol. 2: seminumerical algorithms, (1969), Addison-Wesley Reading, MA · Zbl 0191.18001
[16] Lewin, M.; Livnat, D.; Zwick, U., Improved rounding techniques for the MAX-2-SAT and MAX-DI-CUT problems, (), 67-82 · Zbl 1049.90535
[17] Parrilo, P.A., Semidefinite programming relaxations for semialgebraic problems, Math. programming ser. B, 96, 2, 293-320, (2003) · Zbl 1043.14018
[18] Putinar, M., Positive polynomials on compact semi-algebraic sets, Indiana univ. math. J., 42, 3, (1993) · Zbl 0796.12002
[19] Sturm, J.F., Using sedumi 1.02, a MATLAB toolbox for optimization over symmetric cones, Optim. methods software, 11-12, 625-653, (1999) · Zbl 0973.90526
[20] Zwick, U., Computer assisted proof of optimal approximability results, (), 496-505 · Zbl 1093.68640
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.