Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints

要約

多くの制約充足問題と最適化問題は、ブール充足可能性問題 (SAT) のインスタンスとしてエンコードすることで効果的に解決できます。
ただし、最も単純なタイプの制約であっても、パフォーマンスが大きく異なる多くのエンコーディングが文献に記載されており、特定の問題インスタンスに適切なエンコーディングを選択するという問題は簡単ではありません。
教師あり機械学習アプローチを使用して、擬似ブール制約と線形制約のエンコーディングを選択する問題を調査します。
制約問題に対して標準の機能セットを使用してエンコーディングを効果的に選択できることを示します。
ただし、擬似ブール制約と線形制約用に特別に設計された新しい機能セットを使用することで、より優れたパフォーマンスが得られます。
実際、目に見えない問題クラスのエンコーディングを選択すると、良い結果が得られます。
同じ機能セットを使用した場合、結果は AutoFolio と比較して優れています。
最適なエンコーディングを選択するタスクに対するインスタンスの特徴の相対的な重要性について議論し、機械学習手法のいくつかのバリエーションを比較します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google