SAT インスタンスの難易度の測定

cs.stackexchange https://cs.stackexchange.com/questions/407

質問

SAT のインスタンスが与えられた場合、そのインスタンスを解決するのがどれほど難しいかを推定できるようにしたいと考えています。

1 つの方法は既存のソルバーを実行することですが、これでは難易度を推定するという目的が損なわれてしまいます。2 番目の方法は、ランダム SAT の相転移で行われるように、文節と変数の比率を調べることかもしれませんが、より良い方法が存在すると確信しています。

SAT の例を考えた場合、難易度を測定するための高速ヒューリスティックはありますか?唯一の条件は、これらのヒューリスティックが、インスタンス上で既存の SAT ソルバーを実際に実行するよりも高速であることです。

関連する質問

SAT の問題はどれが簡単ですか? cs Theory.SE 上。この質問は、扱いやすいインスタンスのセットについて尋ねます。これは似た質問ですが、まったく同じではありません。私は、単一のインスタンスを与えて、そのインスタンスが解決するのが難しいかどうかをある種の半知的な推測を行うヒューリスティックに非常に興味があります。

役に立ちましたか？

解決

一般に、これは非常に関連性があり、興味深い研究課題です。「1 つの方法は、既存のソルバーを実行することです...」そして、これは正確に何を教えてくれるでしょうか?インスタンスが特定のソルバーまたは特定のアルゴリズム/ヒューリスティックにとって難しいように見えることは経験的にわかりますが、それはインスタンスの硬度について実際に何を示しているのでしょうか?

追求されてきた方法の 1 つは、効率的なアルゴリズムにつながるインスタンスのさまざまな構造特性を特定することです。これらのプロパティは実際に「簡単に」識別できることが好ましいです。例としては、さまざまなグラフ幅パラメータを使用して測定された、基礎となる制約グラフのトポロジが挙げられます。たとえば、基礎となる制約グラフのツリー幅が定数によって制限されている場合、インスタンスは多項式時間で解決できることが知られています。

別のアプローチでは、次の役割に焦点を当てています。 隠された構造 インスタンスの。一例としては、 バックドアセット, 、インスタンス化されると残りの問題が扱いやすいクラスに単純化されるような変数のセットを意味します。例えば、 ウィリアムズ他、2003 [1] は、バックドア変数の検索コストを考慮した場合でも、セットが十分に小さければ、バックドア セットに焦点を当てることで全体的な計算上の利点を得ることができることを示しています。さらに、 ディルキナら、2007 [2] ソルバーが次のように呼ばれることに注意してください。 サッツランド は、さまざまな実験ドメイン上で小規模で強力なバックドアを見つけるのが非常に得意です。

最近になって、 アンソテギ他、2008 [3] は、DPLL ベースのソルバーの尺度としてツリー状空間の複雑さを使用することを提案しています。彼らは、定数境界空間も、空間が多項式の次数である多項式時間決定アルゴリズムの存在を意味することを証明しています (論文の定理 6)。さらに、彼らは空間が 小さい サイクルカットセットのサイズよりも。実際、特定の仮定の下では、そのスペースはバックドアのサイズよりも小さくなります。

彼らはまた、私があなたが求めていると思うことを形式化します。

尺度 $\psi$ を見つけ、式 $\Gamma$ を与えられたアルゴリズムが時間 $O(n^{\psi ( \Gamma )})$ での充足可能性を決定します。測定値が小さいほど、その特徴をよりよく表します。 式の硬さ.

[1] ウィリアムズ、ライアン、カーラ P.ゴメスとバート・セルマン。「典型的なケースの複雑さへのバックドア」人工知能に関する国際合同会議。Vol.2003 年 18 日。

[2] ディルキナ、ビストラ、カーラ・ゴメス、アシシ・サバーワル。「バックドア検出の複雑さにおけるトレードオフ」制約プログラミングの原則と実践 (CP 2007), pp.256-270、2007。

[3] アンソテギ、カルロス、マリア・ルイサ・ボネット、ジョルディ・レヴィ、フェリップ・マーニャ。「SATインスタンスの硬さの測定」第23回人工知能全国会議(AAAI'08)の議事録、pp.222-228、2008年。

他のヒント

相転移についてはご存知だと思いますが、私が知っている他の簡単なチェックについてもいくつか触れさせてください (これらは制約グラフ分析に含まれる可能性があります)。

  • 初期のランダム SAT ジェネレーターの中には、すべての文節の長さのほぼ等しい割合を意味する「一定密度」を使用していたために、誤ってほとんど簡単な式を作成してしまうものもありました。予想通り、2 つの句とユニットによって問題が大幅に単純化され、非常に長い句によって分岐があまり追加されなかったり、超解像度がさらに促進されたりするため、これらはほとんど簡単でした。したがって、固定長の句を使用し、他のパラメータを変更する方がよいと思われます。
  • 同様に、強力な単純化ルールは純粋なリテラル消去です。明らかに、式が実際に難しいのは、式に含まれる不純なリテラルの数だけです。解決により新しい条項番号が作成されるため $|x|*|\lx|$ ではありません (つまり、 $x$ とその否定)、各変数の正のリテラルと負のリテラルの数が等しい場合、解決の数は最大になります。したがって、バランスの取れた SAT ジェネレーターです。
  • また、「No Triangle SAT」と呼ばれる手法もあり、これは非常に斬新なようです[1]。これは、「三角形」を禁止する一種のハード インスタンス ジェネレーターです。三角形は 3 つの変数を含む一連の文節です $v_1、v_2、v_3$ これは、いくつかの文節のセット内のすべての組み合わせでペアごとに発生します (つまり、 $\{v_1, v_2, ...\}, \{v_2, v_3, ...\}, \{v_1, v_3, ...\}$）。どうやら、三角形は既知のソルバーにとって式を簡単にする傾向があるようです。

[1] https://arxiv.org/pdf/1903.03592.pdf

Juhoの優れた答えに加えて、ここに別のアプローチがあります：

Ercsey-Ravasz＆Toroczkai、 制約満足度へのアナログアプローチにおける一時的なカオスとしての最適化の硬度, 、Nature Physics Volume 7、966〜970ページ（2011）。

このアプローチは、SATの問題を動的システムに書き換えることです。 アトラクタ システムのSAT問題の解決策です。システムの引力の盆地は、問題がより困難になるにつれてフラクタルであるため、SATインスタンスの「難易度」は、システムが収束する前にトランジェントがどの程度混oticとしているかを調べることで測定できます。

実際には、これは、さまざまな初期位置から多くのソルバーを開始し、ソルバーがアトラクタに到達する前に混oticとした過渡現象から逃げる速度を調べることを意味します。

「ソリューション」が特定のSATの問題の解決策である動的システムを考案するのは難しくありませんが、ソリューションがすべて忌避剤ではなく、すべてのアトラクタであることを確認するのは少し難しいです。彼らの解決策は、エネルギー変数（ラグランジュ乗数に似た）を導入して、制約がどれほどひどく違反されているかを表し、システムのエネルギーを最小限に抑えるためにシステムを取得しようとすることです。

興味深いことに、動的システムを使用して、アナログコンピューターで多項式時間のSAT問題を解決できます。これ自体が驚くべき結果です。キャッチがあります。エネルギー変数を表すために指数関数的に大きな電圧が必要になる場合があるため、残念ながら物理的なハードウェアでこれを実現することはできません。

ライセンス： CC-BY-SA と 帰属
所属していません cs.stackexchange
scroll top