コンピュータサイエンスにおいて、シャープ充足可能性問題(シャープSAT、#SAT、モデルカウントとも呼ばれる)は、与えられたブール式を満たす解釈の数を数える問題であり、1979年にValiantによって導入された。[1]言い換えれば、与えられたブール式の変数を一貫してTRUEまたはFALSEの値に置き換えて、式がTRUEと評価されるようにする方法が何通りあるかという問題である。たとえば、式は変数の3つの異なるブール値の割り当てによって充足可能である。つまり、割り当て(= TRUE、 = FALSE)、(= FALSE、= FALSE)、および(= TRUE、= TRUE)のいずれに対しても、次のようになる。
#SAT は、ブール式の解が存在するかどうかを問うブール充足可能性問題(SAT)とは異なります。代わりに、#SAT では、ブール式のすべての解を列挙することが求められます。ブール式の解の総数がわかれば、SAT を定数時間で決定できるという意味で、#SAT は SAT よりも困難です。ただし、逆は当てはまりません。ブール式に解があることがわかっても、可能性は指数関数的に増えるため、 すべての解を数えるのに役立たないからです。
#SAT は、 #P 完全(シャープ P 完全と読む)として知られる計数問題のクラスのよく知られた例です。言い換えると、複雑性クラス#Pの問題のすべてのインスタンスは、#SAT 問題のインスタンスに還元できます。これは重要な結果です。なぜなら、列挙組合せ論、統計物理学、ネットワーク信頼性、人工知能では、既知の公式がない困難な計数問題が多数発生するためです。問題が難しいことが示されれば、見栄えの良い公式が存在しない理由を複雑性理論的に説明できます。 [2]
#P完全性
#SAT は#P 完全です。これを証明するために、まず #SAT が明らかに #P にあることに注目してください。
次に、#SAT が #P 困難であることを証明します。#P の任意の問題 #A を取ります。A は非決定性チューリングマシンM を使用して解決できることがわかっています。一方、Cook-Levin の定理の証明から、M をブール式 F に簡約できることがわかります。ここで、F の有効な割り当てはそれぞれ M 内の許容可能な一意のパスに対応し、その逆も同様です。ただし、M が取る許容可能なパスはそれぞれ A の解を表します。言い換えると、F の有効な割り当てと A の解の間には一対一の関係があります。したがって、Cook-Levin の定理の証明で使用される簡約は簡潔です。これは、#SAT が #P 困難であることを意味します。
解決困難な特殊なケース
充足可能性が扱いやすい (P の場合) 多くの特殊なケース、および充足可能性が扱いにくい (NP 完全) 場合、解を数えることは扱いにくい (#P 完全) です。これには次のものが含まれます。
#3土曜
これは3SATの計数バージョンです。SAT の任意の式は、満足する割り当ての数を保存しながら 3- CNF形式の式として書き直すことができることが示されます。したがって、#SAT と #3SAT は計数的に同等であり、#3SAT は #P 完全でもあります。
#2SAT
2SAT(2CNF式に解があるかどうかの判定)は多項式であるが、解の数を数えることは#P完全である。[3]単調な場合、つまり否定がない場合(#MONOTONE-2-CNF) には、すでに#P完全性がある。
NP がRPと異なると仮定すると、各変数が最大 6 つの節に出現すると仮定しても、#MONOTONE-2-CNF も完全多項式時間近似スキーム(FPRAS) では近似できないことが知られています。ただし、各変数が最大 5 つの節に出現する場合は完全多項式時間近似スキーム (FPTAS) が存在することが知られています。[4]これは、グラフ内の独立集合の数を数える問題♯ISに関する同様の結果から導かれます。
#ホーンSAT
同様に、ホーン充足可能性は多項式であるにもかかわらず、解の数を数えることは#P完全である。この結果は、どのSATのような問題が#P完全であるかを特徴付ける一般的な二分法から導かれる。[5]
プラナー #3SAT
これは平面3SATの計数バージョンである。リヒテンシュタイン[6]によって与えられた3SATから平面3SATへの困難性削減は簡潔である。これは平面#3SATが#P完全であることを意味する。
平面モノトーン直線 #3SAT
これはPlanar Monotone Rectilinear 3SATの計数バージョンです。[7] de Berg & Khosravi [7]によって与えられたNP困難性削減は簡潔です。したがって、この問題は#P完全でもあります。
#DNF
選言標準形(DNF) 式の場合、すべての節のサイズが 2 で否定がない場合でも、解の数を数えることは #P 完全です。これは、ド・モルガンの法則により、DNF の解の数を数えることは、連言標準形(CNF) 式の否定の解の数を数えることと同じだからです。#PP2DNF と呼ばれる場合でも、変数が 2 つのセットに分割され、各節に各セットから 1 つの変数が含まれる場合でも、扱いにくい問題となります。[8]
対照的に、この問題のFPRASであるKarp-Lubyアルゴリズムを使用すると、選言正規形式の解の数を扱いやすく近似することができます。[9]
扱いやすい特殊なケース
アフィン制約充足問題
シェーファーの二分法定理の意味でのアフィン関係に対応するSATの変種、すなわち節がXOR演算子を伴う2を法とする方程式に相当するものは、#SAT問題を多項式時間で解くことができる唯一のSAT変種である。[10]
制限付きツリー幅
SATのインスタンスがグラフパラメータを使用して制限されている場合、#SAT問題は扱いやすくなります。たとえば、ツリー幅が定数で制限されているSATインスタンスの#SATは、多項式時間で実行できます。[11]ここで、ツリー幅は、SAT式に関連付けられたハイパーグラフの主ツリー幅、双対ツリー幅、またはインシデンスツリー幅であり、その頂点は変数であり、各節はハイパーエッジとして表されます。
制限された回路と図のクラス
モデルカウントは、(順序付き) BDDや、 d-DNNF などの 知識コンパイルで研究されるいくつかの回路形式に対しては扱いやすい(多項式時間で解ける)ものです。
一般化
重み付きモデルカウント (WMC) は、モデルをカウントするだけでなく、モデルの線形結合を計算することで #SAT を一般化します。WMC のリテラル重み付きバリアントでは、各リテラルに重みが割り当てられます 。
WMCは確率的推論に使用され、ベイジアンネットワークなどの離散ランダム変数に対する確率的クエリはWMCに還元できる。[12]
代数モデルカウントは、任意の可換半環上の#SATとWMCをさらに一般化します。[13]
参考文献
- ^ Valiant, LG (1979). 「パーマネントを計算する複雑さ」.理論計算機科学. 8 (2): 189– 201. doi : 10.1016/0304-3975(79)90044-6 .
- ^ ヴァダン、サリル・ヴァダン (2018 年 11 月 20 日)。 「講義 24: 計算問題」(PDF)。
- ^ Valiant, Leslie G. (1979). 「列挙と信頼性の問題の複雑さ」SIAM Journal on Computing . 8 (3): 410– 421. doi :10.1137/0208032.
- ^ Liu, Jingcheng; Lu, Pinyan (2015). モノトーンCNFを数えるためのFPTAS. 工業応用数学協会. pp. 1531– 1548. arXiv : 1311.3728 . doi :10.1137/1.9781611973730.101. ISBN 978-1-61197-374-7。
- ^ Creignou, Nadia; Hermann, Miki (1996). 「一般化された満足度計算問題の複雑性」.情報と計算. 125 : 1–12 . doi :10.1006/inco.1996.0016. hdl : 10068/41883 .
- ^リヒテンシュタイン、デイビッド (1982)。 「平面公式とその使用法」。SIAM Journal on Computing。11 ( 2): 329– 343。doi :10.1137/0211025。
- ^ ab de Berg, Mark ; Khosravi, Amirali (2010). 「平面における最適なバイナリ空間分割」。タイ語、My T.; Sahni, Sartaj (編)。コンピューティングと組み合わせ論: 第 16 回国際会議、COCOON 2010、ベトナム、ニャチャン、2010 年 7 月 19 ~ 21 日、議事録。コンピュータ サイエンスの講義ノート。第 6196 巻。ベルリン: Springer。pp. 216 ~ 225。doi : 10.1007 /978-3-642-14031-0_25。ISBN 978-3-642-14030-3. MR 2720098。
- ^ スシウ、ダン;オルテアヌ、ダン。レ、クリストファー。コッホ、クリストフ (2011)、スシウ、ダン。オルテアヌ、ダン。レ、クリストファー。 Koch、Christoph (編)、「クエリ評価問題」、確率的データベース、データ管理に関する総合講義、Cham: Springer International Publishing、pp. 45–52、doi :10.1007/978-3-031-01879-4_3、ISBN 978-3-031-01879-4、 2023年9月16日取得
- ^ Karp, Richard M; Luby, Michael; Madras, Neal (1989-09-01). 「列挙問題に対するモンテカルロ近似アルゴリズム」. Journal of Algorithms . 10 (3): 429– 448. doi :10.1016/0196-6774(89)90038-2. ISSN 0196-6774.
- ^ Creignou, Nadia; Hermann, Miki (1996-02-25). 「一般化された満足度計算問題の複雑性」.情報と計算. 125 (1): 1– 12. doi : 10.1006/inco.1996.0016 . ISSN 0890-5401.
- ^ FICHTE, JOHANNES K.; HECHER, MARKUS; THIER, PATRICK; WOLTRAN, STEFAN (2021-03-12). 「データベース管理システムとツリー幅を利用したカウント」.論理プログラミングの理論と実践. 22 (1): 128– 157. arXiv : 2001.04191 . doi :10.1017/s147106842100003x. ISSN 1471-0684.
- ^ Chavira, Mark; Darwiche, Adnan (2008年4月). 「重み付けモデルカウントによる確率的推論について」.人工知能. 172 ( 6–7 ): 772–799 . doi :10.1016/j.artint.2007.11.002.
- ^ キミッグ、アンジェリカ;ヴァン・デン・ブロック、ガイ。 De Raedt、リュック(2017 年 7 月)。 「代数モデルの計数」。応用論理ジャーナル。22 : 46–62.arXiv : 1211.4475。土井:10.1016/j.jal.2016.11.031。
