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 autoated symmetry breaking, structured local search, automated streamlining and more.