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相比具有竞争力。我们讨论了实例特征对选择最优编码任务的相对重要性，并比较了机器学习方法的多种变体。