Learning SAT Encodings for Constraint Satisfaction Problems

Constraint programming addresses many interesting and challenging problems in
our world, including recent applications to contexts as diverse as allocating
refugee relief funds, short-term mine planning and hardware circuit design.

Users define their problems in high-level modelling languages which include
descriptive global constraints. One of the most effective ways to solve
constraint satisfaction problems (CSPs) is by translating them into instances
of the Boolean Satisfiability Problem (SAT). For some global constraints in
CSPs there exist many algorithms which encode the constraint into SAT;
choosing an appropriate SAT encoding can alter the ultimate solving time
dramatically.

We investigate the problem of selecting the best SAT encoding for
pseudo-Boolean and linear integer constraints. Many machine learning
techniques are explored, applied and evaluated to aid this selection. The
result is a significant improvement in performance compared to the default
choice and to the single best choice from a training set. The approach is
successful even for previously unseen problem classes and it greatly
outperforms a sophisticated general algorithm selection and configuration
tool.

This work provides a thorough empirical study and detailed analysis of each
stage in the machine learning process as applied to choosing SAT encodings.
It does this in three phases: firstly by using generic CSP instance features
to select an encoding per constraint type for each instance, then by
introducing new features which focus on the constraint types in question, and
finally by learning to select encodings for individual constraints.

We find that even generic instance features can produce good predictions, but
that the specialised features introduced give more robust performance
especially when predicting for unseen problem classes. Training to predict
per constraint shows potential and leads to better performance for some
problem classes, but per-instance selection is still competitive across the
corpus of problems as a whole.