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.

翻译：许多约束满足和优化问题可以通过将其编码为布尔可满足性问题（SAT）的实例来有效求解。然而，即使是约束的最简单类型，文献中也存在多种编码方式，其性能差异很大，而为给定问题实例选择合适的编码并非易事。我们探讨了使用监督机器学习方法为伪布尔和线性约束选择编码的问题。我们证明了，使用一组标准的约束问题特征可以有效地选择编码；然而，使用专门为伪布尔和线性约束设计的新特征集时，我们获得了更好的性能。事实上，在为未见问题类别选择编码时，我们取得了良好的结果。在使用相同特征集时，我们的结果与AutoFolio相比具有竞争力。我们讨论了实例特征在最佳编码选择任务中的相对重要性，并比较了机器学习方法的几种变体。