Postdoc and PhD positions in SAT solving at KTH Royal Institute of Technology
The Theory Group at KTH Royal Institute of Technology is looking for postdocs and PhD students in SAT solving.
The positions are within the research group led by Jakob Nordstrom. Much of the activities of this 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, and/or mixed integer linear programming, and so excellent researchers in these areas are also warmly welcome to apply.
The application deadline is January 21, 2018. See the postdoc and the PhD opening webpage, respectively, for full announcements with more information and instructions how to apply. Informal enquiries are welcome and may be sent to jakobn@kth.se .
Jakob Nordström, Associate Professor
KTH Royal Institute of Technology
Phone: +46 8 790 69 19 (office), +46 70 742 21 98 (cell)
http://www.csc.kth.se/~jakobn/
