I’m looking for a talented PostDoc to join the DQBF project: https://github.com/Sat-DQBF. The candidate will work on the development of DQBF solvers.

The last few decades have seen tremendous progress in the development of SAT solvers. However, it has also become clear that they are approaching their limits and are unable to scale to problems that are ill-suited to SAT-based encodings. DQBF (Dependency Quantified Boolean Formulas) is a generalization of the standard QBF that allows them to succinctly encode many hard problems arising in hardware verification, circuit designs and software synthesis.

The main goal of this project is to build a DQBF solver that scales well in applications. The project involves collaborators such as Friedrich Slivovsky (University of Liverpool) and Jie-Hong Roland Jiang (National Taiwan University).

The position is fully funded by UKRI EPSRC for the duration of 3 years. The ideal starting date is as soon as possible, but it is negotiable.

If you are interested or have any question, please contact me at tonytan@liverpool.ac.uk or Friedrich Slivovsky at F.Slivovsky@liverpool.ac.uk. We will be happy to answers any question.

Tony Tan
University of Liverpool