制約充足問題 (CSP) は,与えられた制約を満たす解を探索する問題である.CSP には産学問わず様々な応用があり,人工知能分野などにおける重要な研究課題となっている.本研究では,SATソルバーを用いた高性能な CSP を解くシステムを実現するために,制約のMDD表現とSAT符号化を用いた方法を研究開発した.結果として,国際競技会における入賞とシステムの高速化に成功した.また応用研究として生物学における細胞内で起こる遺伝子の相互作用のネットワークの数理モデルであるオートマタネットワークの定常状態の計算にSAT型解法を応用した.さらにハミルトン閉路問題のSAT型解法の提案も行った.
|