SATソルバー

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

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

先読みソルバーは、特に（単位節伝播を超えた）還元とヒューリスティックを強化しており、一般的に難しいインスタンスでは競合駆動型ソルバーよりも強力です（一方、競合駆動型ソルバーは、内部に簡単なインスタンスが含まれている大規模なインスタンスでははるかに優れている場合があります）。

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

特定の種類の大規模なランダム充足可能SATインスタンスは、サーベイプロパゲーション（SP）によって解くことができます。特にハードウェア設計および検証アプリケーションでは、与えられた命題論理式の充足可能性やその他の論理特性は、二分決定図（BDD）として表現された論理式に基づいて決定されることがあります。

SATソルバーによって、問題の難易度や難易度は異なり、充足不可能性の証明に長けているものもあれば、解法を見つけるのに長けているものもある。これらの特性はすべてSATソルビングコンテストで見ることができる。^{[ 10 ]}

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

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

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

近年、並列ポートフォリオSATソルバーが国際SATソルバーコンペティションの並列トラックを席巻している。そのようなソルバーの注目すべき例としては、Plingelingとpainless-mcomspsが挙げられる。^{[ 19 ]}

並列ポートフォリオとは対照的に、並列分割統治法は、処理要素間で探索空間を分割しようとします。逐次DPLLなどの分割統治アルゴリズムは、既に探索空間を分割する手法を適用しているため、並列アルゴリズムへの拡張は容易です。しかし、単位伝播などの手法により、分割後の部分的な問題の複雑さは大きく異なる場合があります。そのため、DPLLアルゴリズムは通常、探索空間の各部分を同じ時間で処理しないため、負荷分散の問題が困難になります。^{[ 14 ]}

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

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

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

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

SATソルバーは、コンピュータ支援証明による数学定理の証明を支援するために使用されてきました。ラムゼー理論では、FPGA上で動作する特殊なSATソルバーの助けを借りて、これまで知られていなかったいくつかのファンデルワールデン数が計算されました。^{[ 29 ] [ 30 ]} 2016年に、マリイン・ホイレ、オリバー・クルマン、ビクター・マレクは、 SATソルバーを使用してブールピタゴラス三つ組問題を解決し、7825までの整数を必要な方法で色付けする方法がないことを示しました。^{[ 31 ] [ 32 ]}また、ホイレはSATソルバーを使用してシュール数の小さな値も計算しました。^{[ 33 ]}

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

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

SATソルバー（Satplanを参照）は探索計画に使用されます。^{[ 37 ]}

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

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