SATにおける高度な制約伝播と並列マルチエージェントプラニング

SATアルゴリズムに関しては、all-different制約のSAT符号化に関する研究を進めた。all-different制約をSAT符号化する際、通常、任意の2変数間にdifferent制約が存在するものとして符号化することが一般的だが、その場合、符号化後の問題が対称構造をもつことになり、特にUNSATな問題例に対してSATアルゴリズムの性能が著しく劣化することが分かっている。そこで本研究では、順序付けされた補助変数を利用することにより対称構造を排除できる新しい符号化方法を考案した。実験で評価した結果、新しい符号化法に基づくSATアルゴリズムは、相転移領域付近のUNSATな問題例に対して従来の符号化法に基づくSATアルゴリズムよりも効率的に動作することが分かった。一方,並列マルチエージェントプランニングに関しては、協調経路発見問題において、ある固定した最大経路長をもつプランが存在するか否かをSATアルゴリズムで判定し、これを、最大経路長を変えながら最適解を求めるという方法を提案した。また、SAT問題として記述する際に、2つの符号化法を提案した。一つはall-different符号化法とよばれ、その基本アイデアは、あるエージェントがある時刻において取り得る可能な状態を値域とする変数を導入するというものである。一方、もう一つの符号化法はinverse符号化法とよばれ、ある状態のある時刻においてそれを占める可能なエージェントを値域とする変数を導入するというものである。実験で評価した結果、両方の符号化法とも、SATPLANやSASEのような汎用プランナーよりもサイズおよび速度の面で優れていることが分かった。

SATアルゴリズムに関しては、all-different制約のSAT符号化に関する研究を進めた。all-different制約をSAT符号化する際、通常、任意の2変数間にdifferent制約が存在するものとして符号化することが一般的だが、その場合、符号化後の問題が対称構造をもつことになり、特にUNSATな問題例に対してSATアルゴリズムの性能が著しく劣化することが分かっている。そこで本研究では、順序付けされた補助変数を利用することにより対称構造を排除できる新しい符号化方法を考案した。実験で評価した結果、新しい符号化法に基づくSATアルゴリズムは、相転移領域付近のUNSATな問題例に対して従来の符号化法に基づくSATアルゴリズムよりも効率的に動作することが分かった。一方,並列マルチエージェントプランニングに関しては、協調経路発見問題において、ある固定した最大経路長をもつプランが存在するか否かをSATアルゴリズムで判定し、これを、最大経路長を変えながら最適解を求めるという方法を提案した。また、SAT問題として記述する際に、2つの符号化法を提案した。一つはall-different符号化法とよばれ、その基本アイデアは、あるエージェントがある時刻において取り得る可能な状態を値域とする変数を導入するというものである。一方、もう一つの符号化法はinverse符号化法とよばれ、ある状態のある時刻においてそれを占める可能なエージェントを値域とする変数を導入するというものである。実験で評価した結果、両方の符号化法とも、SATPLANやSASEのような汎用プランナーよりもサイズおよび速度の面で優れていることが分かった。