Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
This work addresses the challenge of encoding selection in constraint satisfaction and optimization, which is incremental but improves performance for SAT-based solvers.
The paper tackles the problem of selecting effective SAT encodings for pseudo-Boolean and linear integer constraints by using a supervised machine learning approach, achieving good results on unseen problem classes and outperforming AutoFolio with a new feature set.
Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-Boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.