Satisfaction can be Relaxing

Revisit, review, and evaluate semi-definite programming (SDP) relaxations of the Boolean SAT problem.

Picture of Charles Gretton

12 Jun 2023


co-supervised with Josh Milthorpe.

Some years ago M, Anjos [*A] characterised and evaluated semi-definite programming (SDP) relaxations of the Boolean SAT problem. His empirical work was interesting and somewhat promising, but did not obviously impact the course of fashionable decsion procedures for the SAT problem. There are related works that consider optimisation problems that can be posed about formulae in Boolean logic [*B]. Since Anjos’ study early this century there have been enormous advances in heterogeneous computing, and particular GPGPU libraries and hardware. On that basis, we expect revising the SDP characterisation of SAT will be timely, and yield some interesting results compared to serial and incremental systematic searches that make use of systematic lookahead and CDCL-style backtracking search procedures. 


This project suggest exploring the use of existing implementations of an SDP solution procedure, and swap out the BLAS and LAPACK libraries with their CUDA/GPGPU counterparts. For example, using “” for the BLAS implementation. The target  problem corpus will be “hard” random UNSAT problems in the 3-SAT family, with upwards of 700 Boolean variables.

Background Literature

[*A] Anjos, M. An improved semidefinite programming relaxation for the satisfiability problem. Math. Program. 102, 589–608 (2005).

[*B] Carla P. Gomes, Willem-Jan van Hoeve, and Lucian Leahu. The Power of Semidefinite Programming Relaxations for MAX-SAT. In Proc. Conference: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Third International Conference, CPAIOR 2006, Cork, Ireland, May 31 - June 2, 2006.

[*C] Helmberg C., Rendl F., Vanderbei R.J., Wolkowicz H.: An interior-point method for semidefinite programming. SIAM J. Optim. 6, 342–361 (1996)

[#A] - A C implementation of the predictor-corrector version of the primal-dual barrier method of Helmberg at al. [*C].


Scholarships are available for AU/NZ university students who wish to do an honours research year of study at the Australian National University.


Boolean Satisfiability, GPGPU, Semidefinite Programming

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times