2019 Fiscal Year Annual Research Report
A fast Boolean satisfiability problem solver by shortening the proof
| Project/Area Number |
17K00300
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 充足可能性判定（SAT）問題 / SATソルバー / 圧縮節 |
|---|
| Outline of Annual Research Achievements |
令和元年度は主に以下の2つの研究課題に関して取り組んだ．それぞれの実績概要を示す．
1. 探索の無駄を低減するヒューリスティクスの検討：決定的並列SATソルバーにおける学習節交換時の待ち時間を抑制するため，コードブロックの実行回数に基づく実行時間の推定手法を考案し，これまでのリテラルアクセス回数ベースの手法よりも大きく待ち時間を削減することに成功した．評価実験の結果，64CPUコアからなる多数コア環境において非決定的なソルバーの求解数を超える場合があることを確認した．さらなる待ち時間の削減に向けて，決定的な挙動の担保を考慮せずに求解中に動的に交換間隔を調整する手法について検討を行った．その結果，待ち時間は若干削減できるものの求解数に大きな変化は見られないことから，現状の待ち時間削減手法が十分に効率的であることを確認した．
2. 拡張融合法のための実用的な適用条件の検討：これまで与えられたSAT問題の求解中に拡張融合法によって証明を短縮する手法の検討について進めてきたが，これとは大きく異なるアプローチで証明を短縮する手法について検討した．SAT問題は通常，機械的に生成されるため規則的な構造を多数内包している．そこで規則的に並んだ節群をあらかじめ圧縮しておき，圧縮した節を展開せずに直接推論に利用する手法について検討し，実装ならびに評価を行った．評価実験の結果，１千万節を超える巨大な問題においてメモリ使用量の削減によって求解数の向上が達成できることを確認した．現時点ではまだ証明の高速化や短縮は達成できていないが，今後この手法を拡張し，圧縮節を学習する手法を検討することで証明を短縮し高速化を図る予定である．またこの手法はポートフォリオ型の並列SATソルバーにおいてメモリ使用量を大幅に削減する効果が期待できるため，並列ソルバーへの適用もすすめる予定である．
|
