SAT ソルバー

コンピュータサイエンスと形式手法において、SAT ソルバーはブール値の充足可能性問題を解決することを目的とするコンピュータプログラムです。ブール変数に関する式、たとえば「( xまたはy ) かつ ( xまたはyでない)」を入力すると、 SAT ソルバーは式が充足可能か、充足不可能か、つまり x と y にそのような値が存在しないかを出力します。この場合、 x が真のときに式が充足可能であるため、ソルバーは「充足可能」を返します。 1960 年代に SAT のアルゴリズムが導入されて以来、現代の SAT ソルバーは、効率的に動作するために多数のヒューリスティックとプログラム最適化を伴う複雑なソフトウェア成果物に成長しました。

クック・レビン定理として知られる結果によれば、ブール充足可能性は一般にNP完全問題である。その結果、指数関数的な最悪ケースの複雑さを持つアルゴリズムのみが知られている。それにもかかわらず、2000年代にはSATの効率的でスケーラブルなアルゴリズムが開発され、数万の変数と数百万の制約を含む問題インスタンスを自動的に解決する能力が劇的に進歩することに貢献した。^[1]

SAT ソルバーは、多くの場合、まず式を連言正規形に変換することから始めます。これらは、多くの場合、 DPLL アルゴリズムなどのコア アルゴリズムに基づいていますが、多くの拡張機能と機能が組み込まれています。ほとんどの SAT ソルバーにはタイムアウトが含まれているため、解が見つからない場合でも妥当な時間で終了し、後者の場合は「不明」などの出力が表示されます。多くの場合、SAT ソルバーは答えを提供するだけでなく、式が満たされる場合は例の割り当て ( x、yなどの値) などの詳細情報を提供したり、式が満たされない場合は満たされない節の最小セットを提供したりできます。

最新の SAT ソルバーは、ソフトウェア検証、プログラム分析、制約解決、人工知能、電子設計自動化、オペレーションズ リサーチなどの分野に大きな影響を与えています。強力なソルバーは、無料のオープン ソース ソフトウェアとしてすぐに利用でき、制約論理プログラミングで SAT ソルバーを制約として公開するなど、一部のプログラミング言語に組み込まれています。

ブール式は、ブール（命題）変数x、y、z、...とブール演算 AND、OR、NOTを使用して記述できる任意の式です。たとえば、

( xかつy ) または ( xかつ ( zではない))

割り当ては、各変数に対して割り当て TRUE または FALSE を選択することで構成されます。任意の割り当てvに対して、ブール式を評価でき、true または false に評価されます。式が true に評価される割り当て (満足する割り当てと呼ばれる) が存在する場合、式は満足可能です。

ブール充足可能性問題は、ブール式を入力として、その式が充足可能かどうかを判断する決定問題です。この問題はNP 完全です。

SAT ソルバーは通常、 Davis-Putnam-Logemann-Loveland アルゴリズム(DPLL) と競合駆動節学習(CDCL) という 2 つのコアアプローチのいずれかを使用して開発されます。

DPLL SAT ソルバーは、体系的なバックトラッキング検索手順を使用して、（指数サイズの）変数割り当ての空間を探索し、満足のいく割り当てを探します。基本的な検索手順は、1960 年代初頭に 2 つの独創的な論文で提案され（以下の参考文献を参照）、現在では一般にDPLL アルゴリズムと呼ばれています。^{[2] [3]}実用的な SAT 解決に対する多くの最新のアプローチは、DPLL アルゴリズムから派生しており、同じ構造を共有しています。多くの場合、それらは、産業用アプリケーションに現れるインスタンスやランダムに生成されたインスタンスなど、特定のクラスの SAT 問題の効率のみを改善します。^[4]理論的には、DPLL ファミリーのアルゴリズムに対して指数関数的な下限が証明されています。^[要出典]

2000年代に開発された現代のSATソルバーには、「コンフリクトドリブン」と「先読み」の2種類があります。どちらのアプローチもDPLLから派生しています。^[4]コンフリクトドリブン節学習（CDCL）などのコンフリクトドリブンソルバーは、効率的なコンフリクト分析、節学習、バックジャンプ、ユニット伝播の「2つのウォッチリテラル」形式、適応分岐、ランダムリスタートで基本的なDPLL検索アルゴリズムを拡張します。基本的な体系的検索に対するこれらの「追加機能」は、電子設計自動化（EDA）で発生する大規模なSATインスタンスを処理するために不可欠であることが経験的に示されています。 ^[5]最先端のSATソルバーのほとんどは、2019年現在、CDCLフレームワークに基づいています。^[6]よく知られている実装には、Chaff ^[7]とGRASPがあります。^[8]

先読みソルバーは、特に削減 (単位節の伝播を超える) とヒューリスティックを強化しており、一般に、難しいインスタンスでは競合駆動ソルバーよりも強力です (一方、競合駆動ソルバーは、実際に内部に簡単なインスタンスがある大きなインスタンスでははるかに優れています)。^{[引用が必要]}

2005年のSATコンペティションで比較的成功した衝突駆動型MiniSATは、コードが約600行しかありません。最新の並列SATソルバーはManySATです。^[9]これは、重要な問題クラスで超線形の高速化を実現できます。先読みソルバーの例としては、2007年のSATコンペティションで賞を受賞したmarch_dlがあります。OR -Toolsの一部であるGoogleのCP-SATソルバーは、2018年、2019年、2020年、2021年のMinizinc制約プログラミングコンペティションで金メダルを獲得しました。

SAT の特定の種類の大規模ランダム充足可能インスタンスは、調査伝播 (SP) によって解決できます。^{[引用が必要]}特にハードウェア設計および検証アプリケーションでは、与えられた命題式の充足可能性およびその他の論理プロパティは、二分決定図(BDD)としての式の表現に基づいて決定されることがあります。

SAT解答者によって、簡単または難しいと感じる事例は異なります。また、不満足性の証明に優れている人もいれば、解決策を見つけることに優れている人もいます。これらすべての行動は、SAT解答コンテストで見ることができます。^[10]

並列SAT ソルバーには、ポートフォリオ、分割統治、並列ローカル サーチアルゴリズムの 3 つのカテゴリがあります。並列ポートフォリオでは、複数の異なる SAT ソルバーが同時に実行されます。各ソルバーは SAT インスタンスのコピーを解きますが、分割統治アルゴリズムは問題をプロセッサ間で分割します。ローカル サーチ アルゴリズムを並列化するさまざまなアプローチが存在します。

国際SATソルバーコンペティションには、並列SATソルバーの最近の進歩を反映した並列トラックがあります。2016年^[11] 、 2017年^[12]、2018年^[13]のベンチマークは24個の処理コアを備えた共有メモリシステムで実行されたため、分散メモリやメニーコアプロセッサ向けのソルバーでは不十分だった可能性があります。

一般に、すべての SAT 問題に対して他のすべてのソルバーよりも優れたパフォーマンスを発揮する SAT ソルバーは存在しません。あるアルゴリズムは、他のソルバーが苦手とする問題インスタンスでは優れたパフォーマンスを発揮するかもしれませんが、他のインスタンスではパフォーマンスが低下する可能性があります。さらに、SAT インスタンスが与えられた場合、どのアルゴリズムがこのインスタンスを特に速く解決するかを予測する確実な方法はありません。これらの制限が、並列ポートフォリオ アプローチの動機となっています。ポートフォリオとは、異なるアルゴリズムのセット、または同じアルゴリズムの異なる構成です。並列ポートフォリオ内のすべてのソルバーは、異なるプロセッサで実行され、同じ問題を解きます。1 つのソルバーが終了した場合、ポートフォリオ ソルバーは、この 1 つのソルバーに従って問題が解決可能または解決不可能であると報告します。他のすべてのソルバーは終了します。さまざまなソルバーを組み込んでポートフォリオを多様化し、それぞれが異なる問題セットで優れたパフォーマンスを発揮すると、ソルバーの堅牢性が向上します。^[14]

多くのソルバーは内部的に乱数ジェネレータを使用しています。シードを多様化することは、ポートフォリオを多様化する簡単な方法です。他の多様化戦略には、シーケンシャルソルバーの特定のヒューリスティックを有効、無効、または多様化することが含まれます。^[15]

並列ポートフォリオの欠点の 1 つは、重複作業の量です。シーケンシャル ソルバーで節学習を使用する場合、並列実行ソルバー間で学習した節を共有することで、重複作業を減らし、パフォーマンスを向上させることができます。ただし、最良のソルバーのポートフォリオを並列で実行するだけでも、競争力のある並列ソルバーになります。このようなソルバーの例は、PPfolio です。^{[16] [17]}これは、並列 SAT ソルバーが提供できるパフォーマンスの下限を見つけるために設計されました。最適化が不足しているために大量の重複作業が発生したにもかかわらず、共有メモリ マシンでは優れたパフォーマンスを発揮しました。HordeSat ^[18]は、コンピューティング ノードの大規模なクラスター用の並列ポートフォリオ ソルバーです。コアでは、同じシーケンシャル ソルバーの異なる構成のインスタンスを使用します。特に、難しい SAT インスタンスの場合、HordeSat は線形のスピードアップを実現できるため、実行時間を大幅に短縮できます。

近年、並列ポートフォリオSATソルバーは国際SATソルバーコンペティションの並列トラックで主流を占めています。そのようなソルバーの代表的な例としては、Plingelingやpainless-mcompsが挙げられます。^[19]

並列ポートフォリオとは対照的に、並列分割統治法は処理要素間で探索空間を分割しようとします。シーケンシャルDPLLなどの分割統治法アルゴリズムは、探索空間を分割する手法をすでに適用しているため、並列アルゴリズムへの拡張は簡単です。ただし、ユニット伝播などの手法により、分割後の部分的な問題は複雑さが大幅に異なる場合があります。したがって、DPLLアルゴリズムは通常、探索空間の各部分を同じ時間で処理しないため、負荷分散の問題が困難になります。^[14]

非時系列的なバックトラッキングのため、衝突駆動節学習の並列化はより困難です。これを克服する 1 つの方法は、Cube-and-Conquer パラダイムです。^[20]これは、2 つのフェーズで解決することを提案しています。「キューブ」フェーズでは、問題は数千、最大で数百万のセクションに分割されます。これは、先読みソルバーによって行われ、「キューブ」と呼ばれる一連の部分構成が見つかります。キューブは、元の式の変数のサブセットの結合と見なすこともできます。式と組み合わせて、各キューブは新しい式を形成します。これらの式は、衝突駆動ソルバーによって独立して同時に解決できます。これらの式の論理和は元の式と同等であるため、式の 1 つが満たされている場合、問題は満たされていると報告されます。先読みソルバーは、小さいが難しい問題に適しているため、^[21]問題を徐々に複数のサブ問題に分割するために使用されます。これらのサブ問題は簡単ですが、それでも規模が大きいため、コンフリクト駆動ソルバーにとって理想的な形式です。さらに、先読みソルバーは問題全体を考慮しますが、コンフリクト駆動ソルバーはよりローカルな情報に基づいて決定を下します。キューブフェーズには 3 つのヒューリスティックが関係しています。キューブ内の変数は、決定ヒューリスティックによって選択されます。方向ヒューリスティックは、どの変数割り当て (真または偽) を最初に探索するかを決定します。解決可能な問題インスタンスでは、解決可能なブランチを最初に選択すると便利です。カットオフヒューリスティックは、キューブの拡張を停止し、代わりにシーケンシャルなコンフリクト駆動ソルバーに転送するタイミングを決定します。キューブは、解決が同様に複雑であることが望ましいです。^[20]

Treengelingは、Cube-and-Conquerパラダイムを適用した並列ソルバーの一例です。2012年に導入されて以来、国際SATソルバーコンペティションで何度も成功を収めています。Cube-and-Conquerは、ブールピタゴラスの3倍問題を解くために使用されました。^[22]

Cube-and-Conquerは、2010年にVan der Waerden数w(2;3,17)とw(2;3,18)を計算するために使用されたDPLLベースのDivide-and-conquerアプローチの修正版または一般化であり^[23]、両方のフェーズ（部分問題の分割と解決）がDPLLを使用して実行されました。

SATを解くための並列ローカルサーチアルゴリズムに向けた1つの戦略は、異なる処理ユニットで複数の変数フリップを同時に試すことです。 ^[24]もう1つは、前述のポートフォリオアプローチを適用することですが、ローカルサーチソルバーは節を生成しないため、節の共有は不可能です。代わりに、ローカルで生成された構成を共有することは可能です。これらの構成は、ローカルソルバーが検索を再開することを決定したときに、新しい初期構成の生成をガイドするために使用できます。^[25]

DPLLファミリーに属さないアルゴリズムには、確率的 局所探索アルゴリズムがあります。その一例がWalkSATです。確率的手法は満足のいく解釈を見つけようとしますが、DPLLなどの完全なアルゴリズムとは異なり、SATインスタンスが満足できないと推論することはできません。^[4]

対照的に、Paturi、Pudlak、Saks、ZaneによるPPSZアルゴリズムのようなランダム化アルゴリズムは、例えば制限された幅の解決などのいくつかのヒューリスティックに従って、変数をランダムな順序で設定します。ヒューリスティックが正しい設定を見つけられない場合、変数はランダムに割り当てられます。PPSZアルゴリズムは、 3-SATでの実行時間^[明確化]がです。これは、2019年にHansen、Kaplan、Zamir、Zwickが3-SATで実行時間 のアルゴリズムの修正版を公開するまで、この問題で最もよく知られた実行時間でした。後者は現在、すべてのkの値でk-SATの最速の既知のアルゴリズムです。多くの満足できる割り当てがある設定では、Schöningによるランダム化アルゴリズムの方が境界が優れています。^{[26] [27] [28]}${\displaystyle O(1.308^{n})}$${\displaystyle O(1.307^{n})}$

SAT ソルバーは、コンピュータ支援証明を通じて数学の定理を証明するのを支援するために使用されてきました。ラムゼー理論では、これまで知られていなかったいくつかのファンデルワールデン数が、 FPGA上で実行される特殊な SAT ソルバーの助けを借りて計算されました。^{[29] [30]} 2016 年に、Marijn Heule、Oliver Kullmann、Victor Marek は、 SAT ソルバーを使用してブールピタゴラスの三つ組問題を解決し、7825 までの整数を要求された方法で色付けする方法がないことを示しました。^{[31] [32] Heule は SAT ソルバーを使用して、}シューア数の小さな値も計算しました。^[33]

SATソルバーはハードウェアとソフトウェアの形式検証に使用されます。モデル検査（特に境界付きモデル検査）では、SATソルバーは有限状態システムが意図した動作の仕様を満たしているかどうかを確認するために使用されます。^{[34] [35]}

SATソルバーは、充足可能性モジュロ理論（SMT）ソルバーが構築される中核コンポーネントであり、ジョブスケジューリング、シンボリック実行、プログラムモデルチェック、ホーアロジックに基づくプログラム検証などの問題に使用されます。^{[36]これらの技術は}、制約プログラミングや論理プログラミングとも密接に関連しています。

オペレーションズリサーチでは、SATソルバーは最適化問題やスケジューリング問題の解決に応用されてきました。^[37]

社会的選択理論では、SATソルバーは不可能定理を証明するために使われてきた。^{[38] TangとLinはSATソルバーを使って}Arrowの定理やその他の古典的な不可能定理を証明した。GeistとEndrissはそれを使って集合拡張に関連する新たな不可能性を見つけた。BrandtとGeistはこのアプローチを使って戦略的証明が不可能なトーナメントソリューションの不可能性を示した。他の著者はこの技術を使って欠席パラドックス、中間単調性、確率的投票ルールに関する新たな不可能性を示した。Brandl、Brandt、Peters、Strickerはそれを使って分数社会的選択のための戦略的証明が不可能で効率的で公平なルールの不可能性を示した。^[39]

• カテゴリ:SAT ソルバー
• コンピュータ支援による証明
• 理論による充足可能性

• 2002年以降のSat大会の概要