位取り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的なSAT符号化

DOI HANDLE オープンアクセス

書誌事項

タイトル別名
  • A Compact and Efficient SAT Encoding of Finite CSP based on a Numeral System of Integers

この論文をさがす

抄録

This paper proposes a new SAT encoding method, named compact order encoding, which encodes arithmetic constraints used in Constraint Satisfaction Problems on finite integer domains. The basic idea of the compact order encoding is the use of a numeral system of some base B ≥ 2 to represent integer variables, and each digit of variables is encoded by using the order encoding. It is equivalent the log encoding when B = 2, and it is equivalent to the order encoding when B is larger than the domain size of integer variables. Therefore, it can be seen as a generalization of the log and order encodings. We confirmed that the compact order encoding is applicable to wide range of problems from small-scale (where domain size of variables is less than 102) to large-scale (where domain size of variables is about 107), and shows better performance than log encoding, order encoding, and existing constraint solvers through experimental comparisons on Open- Shop Scheduling and Graph Coloring which are typical constraint satisfaction problems. From those results, although further comprehensive experiments will be necessary for selecting base B, it can be said that the compact order encoding is one of the effective SAT encodings at the current moment applicable to wide range of problems in various scales.

収録刊行物

関連プロジェクト

もっと見る

詳細情報 詳細情報について

問題の指摘

ページトップへ