I attended the Satisfiability: Theory, Practice, and Beyond workshop at Berkeley.

This was a great experience, gave me a chance to listen to talks from prominent people in the SAT and optimisation community about how they see the field is progressing. There was a particular focus on certified algorithms and high-level representations, the latter is of course a major focus of my research as well.

I gave a talk on Conjure, and covered the exciting research directions that are enabled by having a high-level representation of a problem.

(I also had a chance to spend some time with my old friends Onur and Özge Coşkunseda whilst I was near San Franciso, which was brilliant. They introduced me to some of their friends who work in cutting edge Biochemistry applications, potential collaborators for the future…)

Following is the abstract of the talk.

Abstract:

Modelling and encoding choices matter significantly when solving a problem using Constraint Programming, SAT or SMT. The solving time for the same problem can vary from a few seconds to several days depending on the model being used. In this talk I will explain one approach to remedy this problem: abstract modelling. We capture a precise problem specification that is free of adhoc modelling choices and refine this problem specification to low level models automatically using Conjure. Abstract modelling also allows other model optimisation opportunities like automated symmetry breaking, structured local search, automated streamlining and more.

The talk was recorded and is available on Youtube.