Skip to main content
SpringerLink
Log in

An improved semidefinite programming relaxation for the satisfiability problem

  • Published:
Mathematical Programming Submit manuscript

Abstract.

The satisfiability (SAT) problem is a central problem in mathematical logic, computing theory, and artificial intelligence. An instance of SAT is specified by a set of boolean variables and a propositional formula in conjunctive normal form. Given such an instance, the SAT problem asks whether there is a truth assignment to the variables such that the formula is satisfied. It is well known that SAT is in general NP-complete, although several important special cases can be solved in polynomial time. Semidefinite programming (SDP) refers to the class of optimization problems where a linear function of a matrix variable X is maximized (or minimized) subject to linear constraints on the elements of X and the additional constraint that X be positive semidefinite. We are interested in the application of SDP to satisfiability problems, and in particular in how SDP can be used to detect unsatisfiability. In this paper we introduce a new SDP relaxation for the satisfiability problem. This SDP relaxation arises from the recently introduced paradigm of “higher liftings” for constructing semidefinite programming relaxations of discrete optimization problems. To derive the SDP relaxation, we first formulate SAT as an optimization problem involving matrices. Relaxing this formulation yields an SDP which significantly improves on the previous relaxations in the literature. The important characteristics of the SDP relaxation are its ability to prove that a given SAT formula is unsatisfiable independently of the lengths of the clauses in the formula, its potential to yield truth assignments satisfying the SAT instance if a feasible matrix of sufficiently low rank is computed, and the fact that it is more amenable to practical computation than previous SDPs arising from higher liftings. We present theoretical and computational results that support these claims.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Anjos, M.F.: New Convex Relaxations for the Maximum Cut and VLSI Layout Problems. PhD thesis, University of Waterloo, 2001, Published online at http://etd.uwaterloo.ca/etd/manjos2001.pdf

  2. Anjos, M.F., Wolkowicz, H.: Geometry of semidefinite max-cut relaxations via matrix ranks. J. Comb. Optim. 6 (3), 237–270 (2002)

    Article  MATH  Google Scholar 

  3. Anjos, M.F., Wolkowicz, H.: Semidefinite programming for discrete optimization and matrix completion problems. Discr. App. Math. 123 (1–2), 513–577 (2002)

    Google Scholar 

  4. Anjos, M.F., Wolkowicz, H.: Strengthened semidefinite relaxations via a second lifting for the max-cut problem. Discr. App. Math. 119 (1–2), 79–106 (2002)

    Google Scholar 

  5. Balas, E., Ceria, S., Cornuéjols, G.: A lift-and-project cutting plane algorithm for mixed 0–1 programs. Math. Programming 58 (3, Ser. A), 295–324 (1993)

  6. Bauschke, H.H. Kruk, S.G.: The method of reflection-projection for convex feasibility problems with an obtuse cone. Technical report, Oakland University, Rochester MI, U.S.A., February 2002

  7. Benson, S.J., Ye, Y., Zhang, X.: Solving large-scale sparse semidefinite programs for combinatorial optimization. SIAM J. Optim. 10 (2), 443–461 (electronic), (2000)

    Article  MATH  Google Scholar 

  8. Bienstock, D., Zuckerberg, M.: Subset algebra lift operators for 0-1 integer programming. Technical Report CORC 2002-01, Columbia University, July 2002

  9. Burer, S.: Semidefinite programming in the space of partial positive semidefinite matrices. Technical report, Department of Management Sciences, University of Iowa, May 2002

  10. Conforti, M., Cornuéjols, G.: A class of logic problems solvable by linear programming. J. Assoc. Comput. Mach. 42 (5), 1107–1113 (1995)

    MATH  Google Scholar 

  11. de Klerk, E., van Maaren, H.: On semidefinite programming relaxations of (2+p)-SAT. Ann. Math. Artificial Intelligence 37 (3), 285–305 (2003)

    Article  MATH  Google Scholar 

  12. de Klerk, E., van Maaren, H., Warners, J.P.: Relaxations of the satisfiability problem using semidefinite programming. J. Automat. Reason. 24 (1–2), 37–65 (2000)

    Google Scholar 

  13. Ferris, M., Mesnier, M., Moré, J.: NEOS and Condor: Solving optimization problems over the Internet. ACM Trans. Math. Softw. 26 (1), 1–18 (2000)

    Google Scholar 

  14. Fukuda, M., Kojima, M., Murota, K., Nakata, K.: Exploiting sparsity in semidefinite programming via matrix completion I: General framework. SIAM J. Optim., 11 3 (01), 647–674 (electronic), (2000)

    Google Scholar 

  15. Goemans, M.X., Williamson, D.P.: New approximation algorithms for the maximum satisfiability problem. SIAM J. Disc. Math. 7 (4), 656–666 (1994)

    Google Scholar 

  16. 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)

    MATH  Google Scholar 

  17. Grigoriev, D., Hirsch, E.A., Pasechnik, D.V.: Complexity of semialgebraic proofs. Moscow Math. J. 2 (4), 647–679 (2002)

    MATH  Google Scholar 

  18. Gu, J.: Global optimization for satisfiability (SAT) problem. IEEE Trans. on Know. and Data Eng. 6 (3), 361–381 (1994)

    Google Scholar 

  19. Gu, J., Purdom, P.W., Franco, J., Wah, B.W.: Algorithms for the satisfiability (SAT) problem: a survey. In: Satisfiability problem: theory and applications (Piscataway, NJ, 1996), Amer. Math. Soc., Providence, RI, 1997, pp. 19–151

  20. Halperin, E., Zwick, U.: Approximation algorithms for MAX 4-SAT and rounding procedures for semidefinite programs. J. Algorithms 40 (2), 184–211 (2001)

    Article  MATH  Google Scholar 

  21. Helmberg, C.: A cutting plane algorithm for large scale semidefinite relaxations. Technical Report ZR-01-26, Konrad-Zuse-Zentrum Berlin, October 2001. To appear in the Padberg Festschrift “The Sharpest Cut”, SIAM

  22. Helmberg, C., Kiwiel, K.C.: A spectral bundle method with bounds. Math. Program. 93 (2, Ser. A), 173–194 (2002)

  23. Helmberg, C., Rendl, F.: A spectral bundle method for semidefinite programming. SIAM J. Optim. 10 (3), 673–696 (electronic), (2000)

    Article  MATH  Google Scholar 

  24. Henrion, D., Lasserre, J.B.: Gloptipoly - global optimization over polynomials with matlab and sedumi. Technical report, LAAS-CNRS, Toulouse, France, 2002

  25. Karloff, H., Zwick, U.: A 7/8-approximation algorithm for MAX 3SAT? In: Proc. of 38th FOCS, 1997, pp. 406–415

  26. Kočvara, M., Stingl, M.: PENNON - a generalized augmented lagrangian method for semidefinite programming. Technical Report 286, Institute of Applied Mathematics, University of Erlangen, 2001

  27. Kočvara, M., Stingl, M.: PENNON - a code for convex nonlinear and semidefinite programming. Technical Report 290, Institute of Applied Mathematics, University of Erlangen, 2002

  28. Lasserre, J.B.: Optimality conditions and LMI relaxations for 0-1 programs. Technical report, LAAS-CNRS, Toulouse, France, 2000

  29. Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11 (3), 796–817 (electronic), (2000/01)

    Article  MATH  Google Scholar 

  30. Lasserre, J.B.: An explicit equivalent positive semidefinite program for nonlinear 0-1 programs. SIAM J. Optim. 12 (3), 756–769 (electronic), (2002)

    Article  MATH  Google Scholar 

  31. Laurent, M.: Semidefinite relaxations for max-cut. In: M. Grötschel, (ed.), The Sharpest Cut, Festschrift in Honor of M. Padberg’s 60th Birthday. SIAM, to appear

  32. Lovász, L.: On the Shannon capacity of a graph. IEEE Trans. Inform. Theory 25 (1), 1–7 (1979)

    Google Scholar 

  33. Lovász, L., Schrijver, A.: Cones of matrices and set-functions and 0-1 optimization. SIAM J. Optim. 1 (2), 166–190 (1991)

    Google Scholar 

  34. Nakata, K., Fujisawa, K., Fukuda, M., Kojima, M., Murota, K.: Exploiting sparsity in semidefinite programming via matrix completion II: Implementation and numerical results. Math. Prog. 95, 303–327 (2003)

    Article  Google Scholar 

  35. Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Programming 96 (2, Ser. B), 293–320 (2003)

  36. Sherali, H.D., Adams, W.P.: A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM J. Disc. Math. 3 (3), 411–430 (1990)

    MATH  Google Scholar 

  37. Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim. Methods Softw. 11/12 (1–4), 625–653 (1999)

  38. Toh, K.C., Todd, M.J., Tütüncü, R.H.: SDPT3 – a MATLAB software package for semidefinite programming, version 1. 3. Optim. Methods Softw. 11/12 (1–4), 545–581 (1999)

  39. van Maaren, H.: Elliptic approximations of propositional formulae. Discrete Appl. Math. 96/97, 223–244 (1999)

    Google Scholar 

  40. Warners, J.P., van Maaren, H.: A two-phase algorithm for solving a class of hard satisfiability problems. Oper. Res. Lett. 23 (3–5), 81–88 (1998)

    Google Scholar 

  41. Wolkowicz, H., Saigal, R., vandenberghe, L., editors.: Handbook of semidefinite programming. Kluwer Academic Publishers, Boston, MA, 2000

  42. Zwick, U.: Outward rotations: a tool for rounding solutions of semidefinite programming relaxations, with applications to MAX CUT and other problems. In: Proceedings of 31st STOC, 1999, pp. 679–687

Download references

Author information

Authors and Affiliations

  1. Electrical and Computer Engineering, University of Waterloo, Waterloo, Ontario, N2L 3G1, Canada

    Miguel F. Anjos

Authors
  1. Miguel F. Anjos
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Miguel F. Anjos.

Additional information

Mathematics Subject Classification (2000): 20E28, 20G40, 20C20

Rights and permissions

Reprints and permissions

About this article

Cite this article

Anjos, M. An improved semidefinite programming relaxation for the satisfiability problem. Math. Program. 102, 589–608 (2005). https://doi.org/10.1007/s10107-003-0495-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10107-003-0495-2

Keywords

Search

Navigation