[4F3-OS-8b] AIと制約プログラミング(2/2)

[4F3-OS-8b-02] 決定的並列SATソルバー構築のための汎用フレームワークの検討

〇吹上 翼¹、帯津 勇斗¹、鍋島 英知²、盧 暁南² (1. 山梨大学工学部コンピュータ理工学科、2. 山梨大学大学院総合研究部)

キーワード：決定的並列SATソルバー、ポートフォリオ型並列SATソルバー、汎用フレームワーク

マルチコア CPU の普及により並列 SAT ソルバーの開発が進められているが，その多くは非決定的である．また， ManySAT や ManyGlucose のような既存の決定的並列 SAT ソルバーは１種類の逐次ソルバーのみを並列化している．本研究では，まず決定的な並列 SAT ソルバーのための汎用フレームワークを作成するとともに，複数の逐次ソルバーを導入する．次にスレッドごとにソルバーを選択し，複数の逐次ソルバーを並列化した際に発生する待ち時間を削減するための方法を検討した．