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.