充足可能性問題(Propositional Satisfiability Problem, SAT問題)とは、二値変数からなる論理式に対して、その式を充足する変数割り当ての有無を証明する問題である。その性質は古典的なNP完全問題として知られており、充足解の求解を多項式時間以内に終わらせることが困難であると信じられている。問題の形式はConjunctive Normal Form (CNF, 乗法標準形)であり、clauseと呼ばれる論理式が論理積で連結されたものである。SAT問題の生成方法は様々あり、その中でも、現実世界のアプリケーションから生成された問題はアプリケーション問題と呼ばれ、一般的に変数間の依存関係が強く、構造的(structured)な問題であることが知られている。近年の研究成果によって、このアプリケーションから派生したSAT問題を解くソルバ(SATソルバ)の性能が飛躍的に向上し、現実世界の問題を扱える水準に達した。SATソルバは二分木に対するbacktrack探索を行い、conflictが生じた時に新たなclauseを学習するclause学習アルゴリズムが備わっている。また、SATソルバの並列化も進められており、近年は各ワーカーが競争的かつ強力的に探索を行うportfolio戦略が主流となっている。

SATソルバは値を割り振る変数の選択によって、しばしば解の存在しない、また枝狩りを促進する役に立つclauseも学習できないような不毛な探索空間に陥ることがある。そのような空間に陥ると、backtrackだけでは脱却が困難になり、同一空間を長い時間探索することになる。それを防止するために、探索を最初からやり直すrestartが近年のSATソルバに備わっている。一方で、様々な探索空間を場当たり的に探索するだけでは効率的に解を発見することが難しく、互いに関連の深い変数群に対する集中的な探索も必要であると考えられる。両者を適切に切り替える必要があるが、一般的に不毛な探索空間に停滞しているかどうかを検知することは困難である。

この問題に対して、本研究では探索空間の切り替えを積極的に行い、探索に多様性を持たせることを考える。ただし、単純にそれまで探索対象に選ばれていなかった変数を選択するような、無作為な方法による探索空間の転換ではなく、アプリケーション問題に内在する構造を利用した転換が重要である。単純な構造を持つ問題の場合は、たとえ変数が比較的多くても短い処理時間で解を発見できることが多いが、複雑な構造を持つ問題の場合、局所的な構造が絡み合っており、特定の構造のみに対する探索を行っていては解を効率的に発見できないと考えられる。そのような一般的に解くのが困難な問題に対して、問題に内在する局所的な構造を可能な限り探索するために、探索に多様性をもたらすことが重要であると考える。本研究では、問題の構造を利用して、探索初期(入り口)における値を割り振る変数の順番を積極的に変更し、様々な空間への探索を促すことで不毛な探索空間への陥りを防ぎつつ、集中的に探索する変数を切り替え、探索に多様性を与えることを目的とする統合的手法structure-based entry-variable diversionを提案する。

その実現方法の一つとして、restart直前の探索状況から問題の構造を考慮して重要な変数群を見つけ出し、restart後にそれらを優先的に値を割り振ることで探索空間の切り替えを効果的に行うCounter Implication Restart (CIR)を提案し、解くのが困難な問題に対して高速な処理を実現した。そして、探索に多様性を持たせることは逐次のSATソルバのみならず、各ワーカーが可能な限り異なる探索を行う必要があるportfolio型の並列SATソルバにおいても重要な役割を持ち、CIRは同様に高い効果を示した。さらに、より並列数の高い大規模環境において、各ワーカー間で探索空間の重複が顕著になる可能性が高いため、より強力な多様性を実現するblock branchingの提案を行う。block branchingは変数間の強い関係を示すbinary clauseに着目し、それらから互いに関係の深い変数をまとめ、各ワーカーに集中的に探索を行わせる。それによって、問題に内在する局所的な構造を一斉に調べることが期待でき、全体として多様な空間にわたる探索が可能となる。block branchingは解くのが困難な問題に対して有効性を示した。本研究の全ての提案手法は特定のSATソルバの実装に依存せず、近年の多くのSATソルバに適用が可能であり、探索効率を向上させることが可能である。

本論文は「SATソルバにおける効率的な探索の多様化を実現する統合的手法 (A Unified Approach for SAT Solvers to Achieve Efficient Diversification)」と題し、SAT (SATisfiability problem, 充足可能性問題)ソルバ の高速化を目的とし、問題の構造を利用し探索に多様性を持たせるための統一的枠組みを提案、逐次および並列ソルバへの実装実験による検証を行うもので、全八章から構成される。本研究におけるSATソルバの対象は、現実世界の問題から導出される「アプリケーション問題」で、数十万から数百万変数からなるConjunctive Normal Form (CNF, 乗法標準形)を想定している。

第一章「はじめに」では、本論文がターゲットとする「アプリケーション問題」とよばれる一群の問題、たとえば、プランニング、モデル検査、回路設計、ソフトウェア検証といった現実の問題から導出される問題について、その「良い性質」、すなわち、変数間の依存関係が強く構造的であるという性質を利用することにより、探索の高速化が期待できること、そして SATソルバにおける「探索の多様性」の重要性について紹介している。

第二章「SAT 問題とSATソルバ」では、SAT問題や SATソルバに関する基本概念を説明し、現行の殆どのSATソルバで利用されている基本的なアルゴリズムである Davis-Putnam-Logemann-Loveland (DPLL)、およびConflict Driven Clause Learning (CDCL) について説明したうえで、現在、並列SATソルバの主流である Portfolio 法について概説している。

第三章「関連研究」では、本論文の着眼点となった、逐次ソルバにおけるDecision heuristics と Restartに関する手法、および並列SATソルバに採用されている手法について、その手法が適用されたSATソルバと共に紹介し、系譜をたどっている。

第四章「SAT ソルバの内部動作の可視化と解析」では、SATソルバの理解と探索挙動の観察を目的として開発を行ったSATソルバの内部動作可視化ツールを紹介し、いくつかの特徴的な観測結果を示している。この可視化ツールにより、特定の変数に対し偏った探索のみを行うため有効な学習が行えない状態に陥ることがしばしば見受けられることや、implication graphの中に「入次数」が多いノードが出現しやすい問題が存在することが観察され、次章以降の提案の端緒を開いている。

第五章「問題の構造に基づく入り口変数の転換を行う統合的手法」では、探索に多様性を与えるためのフレームワークとして、探索の初期に値を割り振る変数(探索の入り口として選ぶ変数)の順番を、問題の構造を利用することで効果的に変更するstructure-based entry-variable diversionを提案している。これは、探索の対象となる変数に変化をつけることで探索に多様性を与えることを目的として、探索開始時、および restart 時の変数の優先度づけを変更するための枠組みで、本研究では二種類の問題構造について、この枠組みの適用を行っている。

第六章「Counter Implication Restart の提案」(以後、CIRと記す)は、一つ目の適用であり、変数間の値割り当て関係を有向グラフとして表したimplication graphを問題の構造として利用している。restart直前の implication graphを走査し、「入次数の多いノード」すなわちそれまでの探索で比較的重要視されていなかった変数に優先度を付加することで、過去の探索を考慮した上で新たな空間への探索を行っている。本論文ではCIRを逐次SATソルバに実装を行い単体性能を評価、処理時間のかかる「難しい問題」に対して、CIRの有効性を確認している。また、ワーカー毎に異なる探索を行わせるportfolio型の並列SATソルバにも実装を行い、小規模並列SAT ソルバにおける有効性も確認している。

第七章「大規模並列SAT ソルバ向けのdiversification の提案」では、二つ目の適応となるblock branchingの提案を行っている。ここでは、与えられたCNFのbinary clauseを問題の構造として着目、これらのclauseから互いに関連の深い変数から成るブロックを抽出し、各ブロックをportfolio型並列ソルバの各ワーカーに割り当て、ワーカーは割り当てられたブロックの変数に優先度を付加することで、全ワーカーが互いに関連の深い変数を優先して探索しつつ、全体としては、それぞれが可能な限り異なる空間の探索を行うことをめざしている。block branchingはワーカー数の多い大規模並列環境において効果的なdiversificationを図ることができる手法であり、計算機実験の結果から並列環境における有効性を確認している。

第八章「まとめ」では、本論文の研究成果をまとめている。

以上を要するに、本論文は SAT ソルバの効率化のため、問題の持つ構造を利用し多様性を導出する統一的な手法を提案し、その効果についてさまざまな角度から評価を行った。本提案による多様性の実現は、超並列計算機における離散探索問題の並列化手法としてさらなる応用展開が期待される。また、提案手法の一つである CIR は、発表後1年という短期間のうちに複数の並列SAT ソルバに採用されたことが確認されており、これは本提案手法が、単に性能面で優れているのみならず、他手法との親和性も高く実用的であることを示している。このように、本研究は 逐次および並列SATソルバの高効率化に貢献し、短期間のうちにその研究成果が波及し、創造的実践の観点からも価値が大きいと認められる。

よって本論文は博士(情報理工学)の学位請求論文として合格と認められる。