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. The resolution hardness numbers give for 𝑚=1,2,…m=1,2,… the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. We achieve this by a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for formulas and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.

An open access version of the paper is available as a technical report