Ubah CNF menjadi 3-CNF setara yang didefinisikan pada variabel yang sama

8

(Saya memposting pertanyaan ini di CS sepuluh hari yang lalu, tanpa jawaban sejak saat itu - jadi saya posting di sini.)

Setiap rumus CNF dapat diubah dalam waktu polinomial menjadi rumus 3-CNF dengan menggunakan variabel baru. Tidak selalu mungkin jika variabel baru tidak diperbolehkan (misalnya, rumus satu klausa: ).(x1∨x2∨x3∨x4)

Mari tentukan masalah (SAT hingga 3-SAT): Diberi , rumus CNF. Apakah mungkin untuk mengubah menjadi setara 3-CNF yang didefinisikan pada variabel yang sama dengan ? - di mana "setara" berarti dengan set model yang sama.FFFF

Apa kompleksitas masalah ini?

cc.complexity-theory complexity-classes sat Xavier Labouze
sumber
Dengan ekivalen yang Anda maksud adil-memuaskan, saya kira?
Jan Johannsen
1
Sebaliknya, "dengan set model yang sama".
Xavier Labouze
fyi tseitin transform adalah nama untuk transformasi dari -SAT ke 3-SAT menggunakan vars tambahan. sepertinya pertanyaan Anda adalah sesuatu seperti menanyakan tentang keberadaan algoritma kompresi untuk SAT. kedengarannya seperti Anda menginginkan solusi yang sama dengan memperpendek klausa menjadi 3 atau lebih sedikit variabel. dari EE, ini terkait dengan penghitungan semua minterm dan menemukan penutup minimal dan menanyakan apakah ada yang sesuai dengan kriteria (dalam hal ini semua klausa 3 atau lebih sedikit vars). tampaknya memiliki kompleksitas yang berpotensi tinggi. n
vzn
Mungkin ini merupakan co-NP-complete: pilih formula 3CNF , buat formula baru dengan 4 variabel baru . memiliki rumus setara 3CNF pada variabel yang sama jika dan hanya jika tidak memuaskan. φ ′ = ( y 1 ∨ y 2 ∨ y 3 ∨ y 4 ) ∧ C 1 ∧ . . . ∧ C n y 1 , . . . , y 4 φ ′ φφ=C1∧...∧Cnφ′=(y1∨y2∨y3∨y4)∧C1∧...∧Cny1,...,y4φ′φ
Marzio De Biasi
@MarzioDeBiasi. Bagus! Namun, saya tidak yakin itu cukup untuk membuktikan kelengkapan co-NP (entah bagaimana, saya mengharapkan compexity yang lebih tinggi tetapi itu hanya sebuah intuisi ...)
Xavier Labouze

Jawaban:

6

(Dari komentar di atas) Masalahnya tampaknya sulit-TNNP; reduksi sederhananya dari 3CNF-UNSAT (yang dilengkapi coNP): diberi rumus 3CNF , perluas penambahan klausa baru dengan 4 variabel baru:φ=C1∧...∧Cm

φ′=(y1∨y2∨y3∨y4)∧C1∧...∧Cm

φφ′ memiliki rumus 3CNF setara yang didefinisikan pada variabel yang sama jika dan hanya jika rumus asli tidak memuaskan.φ

( ) rumus 3CNF setara dengan( y 1 ∨ y 2 ∨ y 3 ) ∧ ( y 1 ∨ y 2 ∨ y 4 ) ∧ C 1 ∧ . . . ∧ C m φ ′⇐(y1∨y2∨y3)∧(y1∨y2∨y4)∧C1∧...∧Cmφ′

( ) misalkan memiliki rumus 3CNF yang setara dan memuaskan. Pilih tugas yang memuaskan dari , dan sederhanakan dan mengganti variabel dengan kebenaran yang sesuai nilai . Kita mendapatkan yang memuaskan jika dan hanya jika memuaskan (keduanya hanya berisi variabel ). Jelas⇒φ′ φ X = ⟨ ˙ x 1 , . . . , ˙ x n ⟩ φ φ ' φ " x i ˙ x i φ ' X φ " X y i φ ' X = ( y 1 ∨ y 2 ∨ y 3 ∨ y 4 ) φ " X ( yφ″φX=⟨x˙1,...,x˙n⟩φφ′φ″xix˙iφX′φX″yiφX′=(y1∨y2∨y3∨y4). Setiap klausa dari berisi paling banyak tiga variabel, jadi kita dapat memilih salah satunya, misalnya , dan menggunakannya untuk membangun tugas yang memuaskan untuk : yang bukan tugas yang memuaskan untuk , yang mengarah ke kontradiksi.φX″φ ' ⟨ y 1 = f a l s e , y 2 = t r u e , y 3 = f a l s e , y 4 = t r u e , ˙ x 1 , . . . , ˙ x n ⟩ φ "(y1∨¬y2∨y3)φ′⟨y1=false,y2=true,y3=false,y4=true,x˙1,...,x˙n⟩φ″

Marzio De Biasi
sumber
Tks untuk jawabannya. Saya tidak mendapatkan : Saya akan mengatakan bahwa jika dapat dimaafkan maka , yang kemudian setara dengan klausa kosong (ukuran 0). Untuk ), hanya berpikir jika , maka setara dengan ...φ φ ′ ( ⇒ φ = ( x ∨ ¬ x ) ( y 1 ∨ y 2 ∨ y 3 ∨ y 4 ) ∧ ( x ∨ ¬ x ) ( y 1 ∨ y 2 ∨ x ) ∧ ( y 3 ∨ y 4 ∨ ¬ x )(⇐)φφ′(⇒φ=(x∨¬x)(y1∨y2∨y3∨y4)∧(x∨¬x)(y1∨y2∨x)∧(y3∨y4∨¬x)
Xavier Labouze
@XavierLabouze: ya tampak lebih baik. Dalam ( saya berasumsi bahwa ada 3CNF setara , dan kemudian memperoleh kontradiksi dari asumsi bahwa asli memuaskan. Apakah Anda pikir itu salah? ⇒ ) φ ′ φ(⇐)⇒)φ′φ
Marzio De Biasi
Anda benar - saya salah dalam menyatakan memiliki model yang sama dengan . ( y 1 ∨ y 2 ∨ x ) ∧ ( y 3 ∨ y 4 ∨ ¬ x )(y1∨y2∨y3∨y4)∧(x∨¬x)(y1∨y2∨x)∧(y3∨y4∨¬x)
Xavier Labouze
Apakah Anda memperhatikan bahwa sama dengan ? Bisakah Anda jelaskan ini: "Kami mendapatkan yang memuaskan jika dan hanya jika memuaskan", daripada Anda menambahkan "(keduanya hanya berisi variabel )", bagaimana Anda bisa yakin bahwa mereka akan hanya mengandung ? Saya juga tidak mengerti kesimpulannya, apakah Anda membuktikan bahwa menambahkan 4 variabel klausa menjadi 3-cnf dari variabel yang sama adalah coNP-Complete? ( y 1 ∨ y 2 ) ∧ ( y 3 ∨ y 4 ) φ ′ X φ ″ X y i y i(y1∨y2∨y3)∧(y1∨y2∨y4)(y1∨y2)∧(y3∨y4)φX′φX″yiyi
Ilya Gazman
1
φ 2 = ( y 1 ∨ y 2 ) ∧ ( y 3 ∨ y 4 )φ1=(y1∨y2∨y3)∧(y1∨y2∨y4) dan -sama memuaskan tetapi tidak setara (sama) serangkaian model): y1 = F, y2 = F, y3 = T, y4 = T adalah model yang valid untuk tetapi tidak untuk . Dalam pertanyaan kita berbicara tentang rumus yang setara. Buktinya bergantung pada fakta bahwa tidak dapat memiliki set model yang sama dari formula 3CNF apa pun. φ2=(y1∨y2)∧(y3∨y4)φ 2 ( y 1 ∨ y 2 ∨ y 3 ∨ y 4 )φ1φ2(y1∨y2∨y3∨y4)
Marzio De Biasi