書誌事項
- タイトル別名
-
- 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.
収録刊行物
-
- コンピュータ ソフトウェア
-
コンピュータ ソフトウェア 30 (1), 1_211-1_230, 2013
日本ソフトウェア科学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390282679713328384
-
- NII論文ID
- 130004549312
-
- NII書誌ID
- AN10075819
-
- HANDLE
- 20.500.14094/90002834
-
- ISSN
- 02896540
-
- 本文言語コード
- ja
-
- データソース種別
-
- JaLC
- IRDB
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可