The Department of Computer Science at Lund University invites applications for a PhD position in computer science focused on SAT solving and combinatorial optimization.
The PhD student will be working in the research group of Jakob Nordström, which is currently in transition from KTH to a combined location at Lund University and the University of Copenhagen on either side of the Oresund bridge.
Much of the activities of the research group revolve around the themes of efficient algorithms for satisfiability in propositional logic (SAT solving) and lower bounds on the efficiency of methods for reasoning about SAT (proof complexity). On the practical side, one problem of interest is to gain a better understanding of, and improve, the performance of current state-of-the-art SAT solvers based on conflict-driven clause learning (CDCL). We are even more interested in exploring new algebraic or geometric techniques (such as Groebner bases or pseudo-Boolean solving) that could potentially yield exponential improvements over CDCL. We also believe that there should be ample room for technology transfer with related areas such as SMT solving, constraint programming (CP), and/or mixed integer linear programming (MIP), and so the research project will likely involve such areas.
This is a four-year full-time employed position, but PhD positions usually (though not necessarily) include 20% teaching, in which case they are prolonged for one more year. The expected starting date is September 2020, although this is to some extent negotiable. The position is fully funded and comes with a competitive salary.
The application deadline is February 10, 2020. See http://www.csc.kth.se/~jakobn/openings/PhD-SAT-LTH-200210.php for the full announcement with more information and instructions how to apply. Informal enquiries are welcome and may be sent to jakob.nordstrom@cs.lth.se or jn@di.ku.dk .
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************