Description
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.
Goals
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 “libnvblas.so” 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] https://github.com/coin-or/Csdp - A C implementation of the predictor-corrector version of the primal-dual barrier method of Helmberg at al. [*C].
Gain
Scholarships are available for AU/NZ university students who wish to do an honours research year of study at the Australian National University.
https://www.anu.edu.au/study/scholarships/find-a-scholarship/co-lab-honours-grant
Keywords
Boolean Satisfiability, GPGPU, Semidefinite Programming