Loading article…
コンピュータ科学および形式手法において、SATソルバーとは、ブール充足可能性問題（SAT）を解くことを目的としたコンピュータプログラムのことです。入力として「( x or y ) and ( x or not y )」のようなブール変数に関する式が与えられると、SATソルバーは、その式が充足可能（つまり、式を真にするxとyの値が存在する）か、充足不可能（つまり、そのようなxとyの値が存在しない）かを出力します。この場合、xが真であれば式は充足可能なので、ソルバーは「充足可能」を返す必要があります。1960年代にSATのアルゴリズムが導入されて以来、現代のSATソルバーは、効率的に動作するために多数のヒューリスティックとプログラム最適化を含む複雑なソフトウェアへと発展してきました。
クック・レヴィン定理として知られる結果により、ブール充足可能性問題は一般にNP完全問題である。そのため、最悪ケースの計算量が指数関数的に増加するアルゴリズムしか知られていない。それにもかかわらず、2000年代にはSATの効率的でスケーラブルなアルゴリズムが開発され、数万の変数と数百万の制約を含む問題インスタンスを自動的に解決する能力が劇的に向上した。[ 1 ]
SATソルバーは、多くの場合、まず論理式を連言標準形に変換することから始まります。これらは、 DPLLアルゴリズムなどのコアアルゴリズムに基づいていることが多いですが、多くの拡張機能や機能も組み込まれています。ほとんどのSATソルバーにはタイムアウト機能があり、解が見つからない場合でも妥当な時間内に終了し、後者の場合は「不明」などの出力が表示されます。多くの場合、SATソルバーは単に答えを提供するだけでなく、論理式が充足可能な場合は例となる代入（x、yなどの値）などの追加情報を提供したり、論理式が充足不可能な場合は最小限の不充足節セットを提供したりすることができます。
現代のSATソルバーは、ソフトウェア検証、プログラム解析、制約解決、人工知能、電子設計自動化、オペレーションズリサーチなどの分野に大きな影響を与えています。強力なソルバーは、フリーソフトウェアやオープンソースソフトウェアとして容易に入手できるほか、制約論理プログラミングにおける制約としてSATソルバーを公開するなど、一部のプログラミング言語にも組み込まれています。
ブール式とは、ブール（命題）変数x、y、z、...とブール演算 AND、OR、NOTを使用して記述できる任意の式のことです。たとえば、
割り当てとは、各変数に対して、TRUEまたはFALSEのいずれかの割り当てを選択することです。任意の割り当てvに対して、ブール式を評価することができ、その結果は真または偽となります。式が真となる割り当て（充足割り当てと呼ばれる）が存在する場合、その式は充足可能であると言えます。
SATソルバーは通常、Davis–Putnam–Logemann–Lovelandアルゴリズム（DPLL）と、競合駆動型節学習（CDCL）という2つの主要なアプローチのいずれかを使用して開発されます。
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ソルバーは、ポートフォリオ、分割統治、並列局所探索アルゴリズムの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-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 ]
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 ]
SATソルバーは、コンピュータ支援証明による数学定理の証明を支援するために使用されてきました。ラムゼー理論では、FPGA上で動作する特殊なSATソルバーの助けを借りて、これまで知られていなかったいくつかのファンデルワールデン数が計算されました。[ 29 ] [ 30 ] 2016年に、マリイン・ホイレ、オリバー・クルマン、ビクター・マレクは、 SATソルバーを使用してブールピタゴラス三つ組問題を解決し、7825までの整数を必要な方法で色付けする方法がないことを示しました。[ 31 ] [ 32 ]また、ホイレはSATソルバーを使用してシュール数の小さな値も計算しました。[ 33 ]
SATソルバーは、ハードウェアとソフトウェアの形式検証に使用されます。モデル検査（特に、境界付きモデル検査）では、SATソルバーは、有限状態システムが意図された動作の仕様を満たしているかどうかを確認するために使用されます。[ 34 ] [ 35 ]
SATソルバーは、ジョブスケジューリング、シンボリック実行、プログラムモデル検査、ホーア論理に基づくプログラム検証などの問題に使用される充足可能性モジュロ理論（SMT）ソルバーが構築されるコアコンポーネントです。[ 36 ]これらの技術は、制約プログラミングや論理プログラミングとも密接に関連しています。
オペレーションズリサーチでは、SATソルバーは最適化問題やスケジューリング問題の解決に適用されてきた。[ 38 ]
社会選択理論では、SATソルバーは不可能性定理の証明に用いられてきた。[ 39 ] TangとLinはSATソルバーを用いてアローの定理やその他の古典的な不可能性定理を証明した。GeistとEndrissはこれを用いて集合拡張に関連する新たな不可能性を発見した。BrandtとGeistはこのアプローチを用いて戦略耐性のあるトーナメント解に関する不可能性を証明した。他の著者らはこの技術を用いて、欠席パラドックス、中間単調性、確率的投票ルールに関する新たな不可能性を証明した。Brandl、Brandt、Peters、Strickerはこれを用いて、分数社会選択における戦略耐性のある効率的かつ公平なルールの不可能性を証明した。[ 40 ]
数百万の制約と数十万の変数を持つ問題を処理できることが多い。
