2015 Fiscal Year Research-status Report
| Project/Area Number |
26330248
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 充足可能性判定(SAT)問題 / SATソルバー / 動的簡単化 |
|---|
| Outline of Annual Research Achievements |
平成27年度は主に以下の3つの研究課題に関して取り組んだ．それぞれの実績概要を示す．
1. 頑健なヒューリスティクスの開発：学習節の評価尺度の1つであるリテラルブロック距離(LBD)は，充足不能な問題の求解性能向上に大きく寄与した尺度であり，高速SATソルバーの多くで利用されている．この尺度は産業応用問題において特に有用であるが，リテラルブロックの大きさが小さくなる問題においては，LBDに基づくリスタート戦略が不安定になることがある．そこで，求解中にリテラルブロックの大きさに基づいて適切なリスタート戦略を選択する手法を考案・実装した．過去3年の競技会の問題群において評価したところ，求解数が大きく向上することを確認した．
2. 軽量動的簡単化手法の拡張：単位伝播処理から抽出したバイナリ節から基数制約を求解中に抽出し，問題の簡単化に利用する手法を考案・実装した．基数制約のSAT符号化にはいくつもの種類があり，それを構文的または意味的に自動検出する手法も提案されているが，提案手法は求解中に意味的抽出を行う点と基数制約を簡単化に利用する点が新しい．評価実験の結果，一定の性能向上が得られることを確認した．
3. 拡張融合法に基づく次世代SATソルバーの検討：拡張融合法により証明の短縮が図れるケースを検討し，その単純な場合として，あるリテラルを含意する別のリテラル群が頻出する場合に，そのリテラル群に別名を与える手法を考案した．含意関係は単位伝播処理から高速に抽出可能であり，また頻度は近似計数手法を用いることでメモリ使用量を抑えることが可能である．現状では性能向上を達成できていないが，拡張融合法を実現するための要素技術として利用できると考えられる．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で示した3テーマのうち，「1. 頑健なヒューリスティクスの開発」に関しては大きな性能向上を達成しており，期待以上の成果がえられているといえる．本手法を実装したSATソルバーは，SAT Race 2015 競技会において28ソルバー中7位であった．また「2. 軽量動的簡単化手法の拡張」で示した基数制約に基づく簡単化手法も，その効果は大きいとはいえないものの安定した性能改善を示している．
次に「3. 拡張融合法に基づく次世代SATソルバーの検討」では，拡張融合法が証明短縮につながるための一定の適用条件を示したものの，その検出コストを抑えるため実装においては単純なケースに限定しており，現状では性能向上を達成できていない．しかし頻出リテラル群の省メモリな計数方法などの要素技術は実現できており，今後条件を一般化した検出手法を検討する予定である．よって本テーマの進捗はおおむね順調であるといえる．
一方，H27年度に予定していた「4. 明示的な探索空間分割機構を備えた並列SATソルバーの実現」については，既存技術の調査結果から，先読み型SATソルバーの先読み技術を利用した問題分割手法の実現と並列動的簡単化の検討を進めている段階であり，予定よりも遅れているといえる．
以上より，テーマ1に関しては計画以上に進展しており，テーマ2,3はおおむね順調，テーマ4は遅れているため，総合的におおむね順調と判断した．
|
| Strategy for Future Research Activity |
平成28年度は以下の課題に取り組む．
1. 拡張融合法の適用条件の一般化：H27年度に検討した拡張融合法の適用条件は証明短縮につながる条件を示しているものの，その検出にはコストがかかる．コストを低減するために適用条件に制限を加えると，証明短縮の機会を失う可能性があり，そのトレードオフが肝要となる．適用条件に対する制約と証明短縮の効果のバランスを取りながら性能向上を図る．
2. 明示的な探索空間分割機構を備えた並列SATソルバーの実現：探索空間分割型並列SATソルバーでは，いくつかの命題変数の真偽値を仮定することで探索空間の分割を図る．しかし，数百万変数からなる問題のごく一部の変数を仮定するだけでは探索空間の重複を避けることは困難である．本研究では，明示的に探索空間を分割するため，各ソルバーが獲得する学習節に着目し，ソルバー間で多数の学習節が共有可能な場合は探索空間には重複があるといえるため，それを抑制するために問題の再分割や探索戦略へのバイアスを付加する手法について検討を進める．
3. 並列SATソルバーにおける軽量動的簡単化手法の検討：探索空間分割型の並列SATソルバーでは，各ソルバープロセスが解く部分問題はそれぞれ異なる前提に基づくため，あるプロセスの単位伝播から抽出されるバイナリ節を他プロセスでの簡単化に直接利用することはできない．一方，ポートフォリオ型の並列SATソルバーであれば，各ソルバープロセスは同一の問題を解くため，ソルバー間でバイナリ節を共有でき，バイナリ節に基づく動的簡単化を強化できる可能性がある．そこでまずはポートフォリオ型における並列動的簡単化の検討を進める．
|
