Tomáš Peitl and Stefan Szeider won the Best Paper Award at the main track of CP’2020, the 26th International Conference on Principles and Practice of Constraint Programming, for their paper: “Finding the Hardest Formulas for Resolution”.

Congratulations!

In the paper, a  resolution-based method (CDCL SAT solver) is used to find the hardest formulas for resolution, which constitutes a self reference as greatly illustrated by MC Escher in his lithograph “Drawing Hands (1948).

Abstract: A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof.

Peter Norvig (Google Inc.) will give the Vienna Gödel Lecture 2015.

March 26, 2015, 17:30
Vienna University of Technology, Lecture Hall 7
1040 Vienna, Gußhausstraße 27-29, ground floor

The lecture will be moderated by Stefan Szeider.

More information can be found here.