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 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 — in particular, solvers using conflict-driven clause learning (CDCL). We are even more interested in exploring new techniques that hold out the theoretical possibility of exponential improvements over CDCL, but seem hard to implement efficiently in practice, e.g., algebraic methods such as Groebner bases or geometric methods such as pseudo-Boolean solving.

The application deadline is March 31, 2017. See the postdoc and PhD, respectively, for full announcements with more information and instructions how to apply. Informal enquiries are welcome and may be sent to .

Please note that these are additional announcements on top of earlier announcements D-2016-0833 and D-2016-0872 due to additional research funding. Candidates who already applied for these positions should not apply again — all applicants for the announcements are evaluated in parallel.

Jakob Nordström, Associate Professor
KTH Royal Institute of Technology
Phone: +46 8 790 69 19 (office), +46 70 742 21 98 (cell)