alldifferent（x₁,...,x_n） 制約は，制約プログラミン
グにおける代表的なグローバル制約の一つである．この制約は，与えられた変
数 x_i が互いに異なる値を取ることを意味する．alldifferent 制
約は，グラフ彩色問題や時間割問題など様々な問題に現れる．本発表では，
alldifferent 制約の SAT 符号化について，順序符号化法と直接符号化法をチャ
ネリング制約を用いて融合した手法について述べる．考案した SAT 符号化の
評価として，Knuth のThe Art of Computer Programming でも取り上げられて
いるクイーングラフ彩色問題を用いた実験結果を示す．