充足可能性問題について

n変数の3-CNF F が与えらたとして Fに対して次のような命題変数 X_a_b_c を用意します。
{ X_a_b_c = 1 } <=> F はクローズ (a or b or c)を持つ
この時 Xを用いて次のようなCNF G を構成することは可能でしょうか？
{ G = 1 } <=> F が充足可能

よろしくお願いします。

質問者からの補足コメント

• 

  イメージとしてはGはSAT Solverです。
  Fの持っているクローズの情報をGに代入してやればFが充足可能かどうかたちどころにわかるといいますか。
  
  もしGがnの多項式サイズで表現できるなら結構すごいことだと思うし
  Gが必ずnの指数サイズになるならそれもそれで面白いかなと。
  
  nが有限の値を取るなら原理的にはGはCNFで書けると思ってます。
  nが小さい時のGを書き下して式変形でどこまで小さく表現できるかチャレンジしてみるとか色々妄想してます。

  No.1の回答に寄せられた補足コメントです。 補足日時：2021/07/29 19:50

• 例えば3変数の3-CNF Fを考えます
  CNFのなかで使われる変数を a b c とするとFにあらわれる可能性のあるクローズは
  a or b or c
  a or b or not c
  a or not b or c
  a or not b not or notc
  not a or b or c
  not a or b or not c
  not a or not b or c
  not a or not b not or not c
  の8通りなのでそれぞれに対応する命題変数
  
  X_a_b_c
  X_a_b_not_c
  X_a_not_b_c
  X_a_not_b_not_c
  X_not_a_b_c
  X_not_a_b_not c
  X_not_a_not_b_c
  X_not_a_not_b_not_c
  
  を用意します。

    補足日時：2021/07/30 12:21

• 

  3変数の3-CNFが充足不能になるのはすべてのクローズが存在するときだけなので
  G=
  not X_a_b_c or
  not X_a_b_not_c or
  not X_a_not_b_c or
  not X_a_not_b not_c or
  not X_not_a_b_c or
  not X_not_a_b_not_c or
  not X_not_a_not_b_c or
  not X_not_a_not_b_not_c
  となります。
  
  Fが(a or b or c) なら
  
  X_a_b_c = 1
  X_a_b_not_c = 0
  X_a_not_b_c = 0
  X_a_not_b_not_c = 0
  X_not_a_b_c = 0
  X_not_a_b_not c = 0
  X_not_a_not_b_c = 0
  X_not_a_not_b_not_c =0
  
  を代入しG=1となります。

    補足日時：2021/07/30 12:25

• 

  Fがすべてのクローズを持つなら なら
  
  X_a_b_c = 1
  X_a_b_not_c = 1
  X_a_not_b_c = 1
  X_a_not_b_not_c = 1
  X_not_a_b_c = 1
  X_not_a_b_not c = 1
  X_not_a_not_b_c = 1
  X_not_a_not_b_not_c =1
  
  を代入しG=0となります。
  
  どうやって命題変数を用意するか？というのは何を聞かれているのかよくわかりません。すいません。
  
  ここ、文字数制限厳しいですね。好きなだけ書かせてくれればいいのに。

    補足日時：2021/07/30 12:39

• >あ～, ひょっとして X_a_b_c は「a∨b∨c」というクローズの存在を表す, ってこと?
  
  はい。そうです。伝わりにくい書き方ですいませんでした。
  
  >多項式サイズで書ける iff P=NP
  
  ここは本当にそうか疑ってます。
  例えばビジービーバー関数という計算不能な関数があります。
  全ての引数に対してビジービーバー関数を返す一つのプログラムは存在しないことが知られていますが、
  引数一つ一つに対してはビジービーバー関数を返すプログラムはそれぞれ存在します。
  
  すべての引数に対してCNFが充足可能かどうかを多項式時間で返す一つのプログラムが存在すればP=NPですが
  それぞれのnに対しn変数以下のCNFが充足可能かどうかを多項式時間で返すプログラムが存在してもP=NPかどうかは確定しないような気がしてます。

    補足日時：2021/08/01 09:54

No.4 ベストアンサー 回答者： Tacosan 回答日時： 2021/08/01 23:21

えぇと, uniform とか nonuniform とかいうやつかな? そっちはほとんど触ってなかったのでちょいと調べてみたら

http://lealgorithm.blogspot.com/2020/07/uniformn …
に説明がある. あと, Manahey の定理
https://en.wikipedia.org/wiki/Mahaney%27s_theorem
なんてのもあるらしい.

この回答へのお礼

おっと、多分これですね、欲しかった答えは。
時間を取ってみてみたいと思います。
ありがとうございます。

お礼日時：2021/08/02 07:55

No.3 回答者： Tacosan 回答日時： 2021/08/01 01:31

あ～, ひょっとして X_a_b_c は「a∨b∨c」というクローズの存在を表す, ってこと?

そうだとすると....
G の中に存在限量子を入れていいなら簡単だけどつまるところ元の SAT に戻るから意味ないよなぁ. 逆に存在限量子を入れないと
多項式サイズで書ける iff P=NP
になって現時点ではたぶん「なにもいえない」んじゃないかな.

No.2 回答者： Tacosan 回答日時： 2021/07/30 00:19

「命題変数 X_a_b_c」をどうやって「用意」する?

って話が全くないのはどうしてだろう.

あと「{ G = 1 }」ってどういう意味? まず「1」が何を意味するのかわからんし, 「恒等的に 1」なのか「1になることもある (1 でないこともある)」なのかによっても全く話は違うんだけど.

No.1 回答者： Tacosan 回答日時： 2021/07/29 00:21

ん～と, なにを気にしているんだろう.

というか, そもそも
{ X_a_b_c = 1 } <=> F はクローズ (a or b or c)を持つ
という「命題変数 X_a_b_c」をどうやって「用意」する?