満たされないコア

数理論理学では、充足不可能なブール命題式が連言標準形で与えられた場合、その連言が依然として充足不可能な節のサブセットは、元の式の 充足不可能なコアと呼ばれます。

多くのSAT ソルバーは、元の問題の不満足性を証明する 解決グラフを生成できます。これを分析して、より小さな不満足なコアを生成できます。

不満足核は、そのすべての適切な部分集合（任意の節の削除が可能）が満足可能である場合、極小不満足核と呼ばれます。したがって、そのような核は局所最小値ですが、必ずしも大域最小値ではありません。極小不満足核を計算する実用的な方法はいくつかあります。^[1]^[2]

最小不満足コアには、不満足のままであるために必要な元の節の最小数が含まれます。最小不満足コアを計算する実用的なアルゴリズムは知られておらず、^[3]連言標準形の入力式の最小不満足コアを計算することは-完全問題です。 ^[4]用語に注意してください。最小不満足コアは簡単な解を持つローカル問題でしたが、最小不満足コアは簡単な解が知られていない グローバル問題です。 $\Sigma _{2}^{\mathsf {P}}$

参考文献

^ Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). 「最小の不満足なコア抽出のためのスケーラブルなアルゴリズム」(PDF)。 Biere, A.; Gomes, CP (編)。満足可能性テストの理論と応用 — SAT 2006。コンピュータサイエンスの講義ノート。 Vol. 4121。 Springer。 pp. 36–41。arXiv : cs/0605085。CiteSeerX 10.1.1.101.5209。doi :10.1007/11814948_5。ISBN 978-3-540-37207-3. S2CID 2845982。
^ Szeider, Stefan (2004 年 12 月). 「有界な節変数差を持つ最小の不満足な式は固定パラメータで扱いやすい」. Journal of Computer and System Sciences . 69 (4): 656–674. CiteSeerX 10.1.1.634.5311 . doi :10.1016/j.jcss.2004.04.009.
^ Liffiton, MH; Sakallah, KA (2008). 「制約の最小不満足サブセットを計算するためのアルゴリズム」(PDF) . J Autom Reason . 40 : 1–33. CiteSeerX 10.1.1.79.1304 . doi :10.1007/s10817-007-9084-z. S2CID 11106131.
^ 「最小不満足コアの計算の複雑さ」。理論計算機科学スタックエクスチェンジ。 2024年9月24日閲覧。

[1] Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). 「最小の不満足なコア抽出のためのスケーラブルなアルゴリズム」(PDF)。 Biere, A.; Gomes, CP (編)。満足可能性テストの理論と応用 — SAT 2006。コンピュータサイエンスの講義ノート。 Vol. 4121。 Springer。 pp. 36–41。arXiv : cs/0605085。CiteSeerX 10.1.1.101.5209。doi :10.1007/11814948_5。ISBN 978-3-540-37207-3. S2CID 2845982。

[2] Szeider, Stefan (2004 年 12 月). 「有界な節変数差を持つ最小の不満足な式は固定パラメータで扱いやすい」. Journal of Computer and System Sciences . 69 (4): 656–674. CiteSeerX 10.1.1.634.5311 . doi :10.1016/j.jcss.2004.04.009.

[3] Liffiton, MH; Sakallah, KA (2008). 「制約の最小不満足サブセットを計算するためのアルゴリズム」(PDF) . J Autom Reason . 40 : 1–33. CiteSeerX 10.1.1.79.1304 . doi :10.1007/s10817-007-9084-z. S2CID 11106131.

[4] 「最小不満足コアの計算の複雑さ」。理論計算機科学スタックエクスチェンジ。 2024年9月24日閲覧。