[3H1-OS-9a] OS-9

10:15 AM - 10:30 AM JST(1:15 AM - 1:30 AM UTC)

[3H1-OS-9a-06] Construction of a Solver Based on Continuous-Time Dynamical Systems for Making Unsatisfiable Boolean Formulas Satisfiable

〇Yuto Yamaguchi¹, Nozomi Akashi¹, Akihiro Yamamoto¹ (1. Graduate School of Informatics, Kyoto University)

Keywords:

Satisfiability problem,Dynamical system,Continuous optimization problem,Analog computing

実社会の多くの割り当て問題はブール充足可能性(SAT)問題として定式化可能である．しかし，定式化されたSATの論理式が充足解の存在しない充足不能となるケースが多く発生することが考えられる．実用上は，充足不能な例においても充足可能とする制約の修正を求めることが重要である．しかし，充足不能な例において，修正の手掛かりとなる最大充足数を求める問題はSATの充足解構築より困難という課題がある．そこで本研究は，SATの充足解を多項式時間で構築するとされる連続時間力学系(CTDS)ソルバーに基づき，SATの制約修正と解構築を同時に行う手法を提案する．提案手法では，SATの変数と制約を連続緩和することで勾配降下法を適用し，連続時間力学系として変数と制約の最適化を行う．ランダム3-SAT問題に対する実験の結果，本手法は従来のCTDSソルバーとは異なり，充足不能な論理式に対し，単一の実行過程において制約を修正し，修正後の論理式に対する充足解を構築することが確認された．連続時間力学系は物理実装が可能であるため，本結果は，SATの制約修正に対する，アナログ計算も可能な新しい道筋を提示するものである．