Research and Development of a New SAT Solving Technologies for Constraint Satisfaction Problems

点击翻译按钮获取中文摘要

本研究の目的は，制約充足問題に対する新しいSAT解法技術を研究開発し，さらに開発したシステムを実用的な問題に応用し，既存技術では解けなかった問題の解決を目指すとともに研究開発した技術を評価することである．研究遂行のため(WG1) SAT符号化手法の研究開発，(WG2) SAT型制約ソルバーの研究開発，(WG3) 応用・評価の3つの研究開発テーマを設定し，研究開発を分担して進めている．(WG1)では，研究代表者らが考案した順序符号化を用いて整数係数を持つ線形制約をSAT符号化した場合に，どのような変数順序で符号化アルゴリズムを実行すると良いかについて実験を行い，結果を評価した．また，接頭和を用いた符号化法，剰余記数法を用いた符号化法，MDDを用いた符号化法について検討を進めた．(WG2)では，ベースとなるSAT型制約ソルバーFun-sCOPで2022年XCSP3競技会 (http://xcsp.org/competitions/)に参加し，Main CSPトラックで準優勝という結果を得た．(WG3)では，システム生物学の分野で用いられている非同期多値ネットワークの解析を行うためのSAT型手法を考案し，そのシステムを開発した(雑誌論文1)．具体的には，非同期オートマタネットワークとして表現されている遺伝子ネットワークについて，そのアトラクターをSATソルバーを利用して発見することにより，元の遺伝子ネットワークの定性的な分析を可能にした．次に，複数の車種からなる車を製造する場合に，全体の平均燃費がCAFE規制値を満たす範囲内で総販売予想金額を最大にする組み合わせを探索するための手法を考案し，ASPソルバーを用いたシステムを開発した(雑誌論文2)．さらに，グラフの支配集合や独立集合をSAT型手法で効率良く求める方法について研究を行い結果を学会で発表した．