Apakah XOR-SAT yang digeneralisasi secara efisien dapat dipecahkan?

12

Saya telah melihat bagaimana XOR-3-SAT dapat dipecahkan secara efisien (misalnya, lihat bagian "XOR-satisfiability" di entri Wikipedia untuk masalah kepuasan Boolean ).

Saya bertanya-tanya pertanyaan mendasar: Apakah XOR-k-SAT efisien dipecahkan, untuk formula dengan jumlah liter yang berbeda per klausa?

Saya benar-benar ingin tahu apakah kita dapat meningkatkan jumlah literal per klausa melebihi 3, dan jika kita dapat memiliki panjang klausa campuran.

complexity-theory satisfiability Matt Groff
sumber
2
Penelitian apa yang telah Anda lakukan? Kami berharap Anda melakukan upaya serius sendiri terlebih dahulu, sebelum bertanya, dan menunjukkan kepada kami dalam pertanyaan penelitian apa yang telah Anda lakukan dan apa yang telah Anda coba. Wikipedia menyebutkan bahwa algoritma untuk menyelesaikan XOR-3-SAT adalah eliminasi Gaussian. Sudahkah Anda berupaya memahami cara kerjanya, dan melihat apakah itu berlaku untuk XOR-k-SAT?
DW
@DW saya akui bahwa saya tidak melakukan banyak penelitian tentang itu. Saya melihat penyebutan Gaussian, dan berpikir bahwa ini akan bekerja untuk XOR-SAT yang digeneralisasi. Tapi saya kira saya sedang mencari konfirmasi. Saya harap Anda akan memaafkan kemalasan saya. Saya akan mencoba melakukan penelitian lebih lanjut di masa depan, sebelum mengajukan pertanyaan seperti ini.
Matt Groff

Jawaban:

11

Sepertinya artikel Wikipedia yang Anda tautkan mengatakan bahwa XORSAT (bukan hanya 3-XORSAT) ada dalam P. Metode yang digunakan untuk menyelesaikan rumus 3-XORSAT dalam contoh mereka sangat mudah digeneralisasikan ke rumus di mana klausa dapat secara sewenang-wenang sejumlah besar variabel dan jumlah variabel yang berbeda.

Anda cukup melihat rumus sebagai sistem persamaan linear di mana Anda memiliki persamaan untuk setiap klausa, dan variabel untuk setiap variabel. Misalnya, rumusnya:

(x1⊕x2⊕¬x3⊕x5)∧(x2⊕x3)

memiliki penugasan yang memuaskan jika dan hanya jika sistem persamaan berikut memiliki solusi:

x1+x2+(1+x3)+x5≡1mod2
x2+x3≡1mod2

Dan kita dapat menemukan solusi untuk sistem persamaan linear seperti ini dalam waktu polinomial menggunakan eliminasi Gaussian!

Dylan McKay
sumber
6

Iya. Ini dipecahkan dengan eliminasi Gaussian. Eliminasi gaussian dapat menyelesaikan sistem persamaan apa pun yang modulo linier. XOR bertindak sebagai modulo 2 tambahan, sehingga setiap klausa XOR-SAT bertindak sebagai modulo persamaan linier 2. Akibatnya, eliminasi Gaussian dapat menyelesaikan setiap rumus XOR-k-SAT atau rumus XOR-SAT apa pun, bahkan jika ada sejumlah literal yang berbeda per klausa atau panjang klausa campuran, dalam waktu polinomial.

DW
sumber