@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00220600, author = {小菅, 脩司 and 宋, 剛秀 and 田村, 直之 and 番原, 睦則}, book = {第84回全国大会講演論文集}, issue = {1}, month = {Feb}, note = {alldifferent(x1,...,xn) 制約は,制約プログラミングにおける代表的なグローバル制約の一つである.この制約は,与えられた変数 xi が互いに異なる値を取ることを意味する.alldifferent 制約は,グラフ彩色問題や時間割問題など様々な問題に現れる.本発表では,alldifferent 制約の SAT 符号化について,順序符号化法と直接符号化法をチャネリング制約を用いて融合した手法について述べる.考案した SAT 符号化の評価として,Knuth のThe Art of Computer Programming でも取り上げられているクイーングラフ彩色問題を用いた実験結果を示す.}, pages = {267--268}, publisher = {情報処理学会}, title = {チャネリング制約を用いた alldifferent 制約の SAT 符号化}, volume = {2022}, year = {2022} }