Abstract
Recently, Linear Programming (LP)-based relaxations have been shown promising in boosting the performance of exact MAX-SAT solvers. We compare Semidefinite Programming (SDP) based relaxations with LP relaxations for MAX-2-SAT. We will show how SDP relaxations are surprisingly powerful, providing much tighter bounds than LP relaxations, across different constrainedness regions. SDP relaxations can also be computed very efficiently, thus quickly providing tight lower and upper bounds on the optimal solution. We also show the effectiveness of SDP relaxations in providing heuristic guidance for iterative variable setting, significantly more accurate than the guidance based on LP relaxations. SDP allows us to set up to around 80% of the variables without degrading the optimal solution, while setting a single variable based on the LP relaxation generally degrades the global optimal solution in the overconstrained area. Our results therefore show that SDP relaxations may further boost exact MAX-SAT solvers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Hooker, J.N., Fedjiki, C.: Branch-and-cut solution of inference problems in propositional logic. Annals of Math. and Artificial Intelligence 1 (1990)
Warners, J.: Nonlinear approaches to satisfiability problems. PhD thesis, Technische Universiteit Eindhoven (1999)
Xing, Z., Zhang, W.: Maxsolver: An efficient exact algorithm for (weighted) maximum satisfiability. Artificial Intelligence 164(1-2), 47–80 (2005)
Joy, S., Mitchell, J., Borchers, B.: A branch and cut algorithm for MAX-SAT and weighted MAX-SAT. Satisfiability Problem: Theory and Applications 35, 519–536 (1997)
Alizadeh, F.: Interior point methods in semidefinite programming with applications to combinatorial optimization. SIAM Journal on Optimization 5(1), 13–51 (1995)
Goemans, M., Rendl, F.: Combinatorial Optimization. In: Wolkowicz, H., Saigal, R., Vandenberghe, L. (eds.) Handbook of Semidefinite Programming, pp. 343–360. Kluwer, Dordrecht (2000)
Grötschel, M., Lovász, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization. John Wiley & Sons, Chichester (1988)
Goemans, M., Williamson, D.: Improved Approximation Algorithms for Maximum Cut and Satisfiability Problems Using Semidefinite Programming. Journal of the ACM 42(6), 1115–1145 (1995)
Hochbaum, D.S.: (Editor) Approximation algorithms for NP-Hard problems. PWS Publishing Company (1997)
Feige, U., Goemans, M.: Approximating the value of two prover proof systems, with applications to max2sat and max dicut. In: Proceedings of the 3rd Israel Symposium on Theory of Computing and Systems (1995)
Garey, M., Johnson, D.: Computers and Intractibility. Freeman, New York (1979)
Chvátal, V., Reed, B.: Mike gets some (the odds are on his side). In: 33th Annual Symposium of Foundations of Computer Science, pp. 620–627 (1992)
Lewin, M., Livnat, D., Zwick, U.: Improved rounding techniques for the MAX 2-SAT and MAX DI-CUT problems. In: Cook, W.J., Schulz, A.S. (eds.) IPCO 2002. LNCS, vol. 2337, pp. 67–82. Springer, Heidelberg (2002)
Anjos, M.: Semidefinite optimization approaches for satisfiability and maximum-satisfiability problems. Journal on Satisfiability, Boolean Modeling and Computation 1, 1–47 (2005)
de Klerk, E., van Maaren, H.: On semidefinite programming relaxation of 2+p-sat. Annals of Math. and Artificial Intelligence 37 (2003)
Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)
Selman, B.: Mwff - a program for generating random MAX k-SAT instances (1993)
Borchers, B.: A C Library for Semidefinite Programming. Optimization Methods and Software 11(1), 613–623 (1999), http://www.nmt.edu/~borchers/csdp.html
Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gomes, C.P., van Hoeve, WJ., Leahu, L. (2006). The Power of Semidefinite Programming Relaxations for MAX-SAT. In: Beck, J.C., Smith, B.M. (eds) Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems. CPAIOR 2006. Lecture Notes in Computer Science, vol 3990. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11757375_10
Download citation
DOI: https://doi.org/10.1007/11757375_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34306-6
Online ISBN: 978-3-540-34307-3
eBook Packages: Computer ScienceComputer Science (R0)