2019 IJCAI-JAIR Best Paper Prize

Marijn Heule (now at Carnegie Mellon University, USA), Matti Järvisalo (Constraint Reasoning and Optimization Group at University of Helsinki, Finland), Florian Lonsing (now at Stanford University, USA), Martina Seidl and Armin Biere (Johannes Kepler University, Austria) have been awarded the for their paper "Clause Elimination for SAT and QSAT", which appeared in volume 53 (2015) of , a leading journal in the general field of AI research.

The paper was chosen as the recipient of this prestigious award from the set of all papers published at JAIR in the preceding five calender years. The award was announced during the opening ceremony of the leading AI conference IJCAI 2019,  on August 13 in Macau, China. An invited award talk was delivered on the same day at IJCAI 2019 by Järvisalo. "In his 2019 IJCAI-JAIR Best Paper Prize talk, Matti Järvisalo nicely emphasises the enormous impact of automated reasoning in AI and beyond ... and shines a bright light on one of AI's largest intellectual and commercial successes to date.", , Chair of the 2019 IJCAI-JAIR Best Paper Prize Selection Committee.

As noted in the award citation, the paper describes fundamental and practical results on a range of clause elimination procedures as preprocessing and simplification techniques for SAT and QBF solvers. Since its publication, the techniques described therein have been demonstrated to have profound impact on the efficiency of state-of-the-art SAT and QBF solvers. The work is elegant and extends beautifully some well-established theoretical concepts. In addition, the paper gives new emphasis and impulse to pre- and in-processing techniques - an emphasis that resonates beyond the two key problems, SAT and QBF, covered by the authors.

Further information:

 (in German)