[Job-offers-cs] Postdoc positions in SAT solving at KTH Royal Institute of Technology

[Pekka Orponen]

-------- Forwarded Message --------
Subject: [DMANET] Postdoc positions in SAT solving at KTH Royal 
Institute of Technology
Date: Sun, 23 Dec 2018 10:59:58 +0000
From: Jakob Nordström <jakobn at kth.se>
To: dmanet at zpr.uni-koeln.de <dmanet at zpr.uni-koeln.de>

The TCS Group at KTH Royal Institute of Technology invites applications 
for postdoc positions in computer science focused on algorithms for 
solving the Boolean satisfiability problem (SAT) very efficiently for 
large classes of instances, and on analyzing and understanding such 
algorithms.

KTH Royal Institute of Technology is the leading technical university in 
Sweden. The Theoretical Computer Science Group at KTH (www.kth.se/tcs) 
offers a strong research environment spanning a wide range of research 
topics such as complexity theory and approximation algorithms, computer 
and network security, cryptography, formal methods and natural language 
processing. We have one of Europe's most prominent groups in algorithms 
and complexity theory, and the research conducted here has attracted 
numerous international awards and grants in recent years.

The postdoctoral researchers will be working in the research group of 
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.

A more detailed description of the project can be found at 
www.csc.kth.se/~jakobn/project-proofcplx. The group currently consists 
of 4 postdoctoral researchers and 4 PhD students (in addition to the 
PI). There are also several other professors, postdocs, and PhD students 
in the TCS Group working on other aspects of algorithms and 
computational complexity, and so this is a unique opportunity to explore 
new connections between theoretical and practical areas of computer 
science within a vibrant and growing research environment.

Within the overall framework sketched above, the postdocs will be 
expected and encouraged to contribute to and influence the research 
agenda. Taking part in teaching graduate seminar courses is encouraged 
but not required. Travel funding is included, and the group also 
receives short-term and long-term visitors on a regular basis.

These postdoc positions are full-time employed positions for one year 
with a possible (and expected) one-year extension. The expected starting 
date is in August-September 2019, although this is to some extent 
negotiable.

The application deadline is February 4, 2019. See 
http://www.csc.kth.se/~jakobn/openings/J-2018-3178-Eng.php for the full 
announcement with more information and instructions how to apply. 
Informal enquiries are welcome and may be sent to jakobn at kth.se .