A small amount of practical experience with SAT, SMT or CSP solvers (or
any tool that uses them, such as most verification systems) will show
that there is significant variation in run-time even between relatively
similar problems. This naturally leads to a whole range of questions;
What is difficulty? Where does it come from? What is the relation
between theoretical measures (such as proof complexity) and practical
ones (such as run-time)? Can we recognise difficulty and identify it
with parts of the problem? Can we predict the difficulty of a problem
in less time than it takes to solve it? In this talk we will present an
abstract satisfaction view on difficulty; using the mathematics of
abstract interpretation to understand satisfiability problems. This is
a work-in-progress talk so all are welcome to attend and participate.