Czy uogólniony XOR-SAT jest sprawnie rozwiązywalny?

12

Widziałem, w jaki sposób XOR-3-SAT można skutecznie rozwiązać (na przykład zobacz sekcję „Zgodność XOR” we wpisie w Wikipedii na temat problemu logicznej satysfakcji ).

Zastanawiam się nad podstawowym pytaniem: czy XOR-k-SAT można skutecznie rozwiązać w przypadku formuł o różnej ilości literałów w klauzuli?

Naprawdę chciałbym wiedzieć, czy możemy zwiększyć liczbę literałów na klauzulę powyżej 3 i czy możemy mieć mieszane długości klauzul.

complexity-theory satisfiability Matt Groff
źródło
2
Jakie badania przeprowadziłeś? Oczekujemy, że najpierw podejmiesz poważny wysiłek, zanim zapytasz, i pokażesz nam w pytaniu, jakie badania przeprowadziłeś i co próbowałeś. Wikipedia wspomina, że ​​algorytmem rozwiązywania XOR-3-SAT jest eliminacja Gaussa. Czy próbowałeś zrozumieć, jak to działa, i sprawdzić, czy dotyczy to XOR-k-SAT?
DW
@DW Przyznaję, że nie przeprowadziłem wielu badań na ten temat. Widziałem wzmiankę o eliminacji Gaussa i pomyślałem, że to zadziała dla uogólnionego XOR-SAT. Ale chyba szukałem potwierdzenia. Mam nadzieję, że wybaczysz moje lenistwo. Spróbuję przeprowadzić więcej badań w przyszłości, zanim zadam takie pytania.
Matt Groff,

Odpowiedzi:

11

Wygląda na to, że artykuł w Wikipedii, z którym się łączysz, mówi, że XORSAT (nie tylko 3-XORSAT) znajduje się w P. Metoda, dzięki której rozwiązują tę formułę 3-XORSAT w ich przykładzie bardzo łatwo uogólniają się do formuł, w których klauzule mogą mieć dowolnie duża liczba zmiennych i różna liczba zmiennych.

Po prostu patrzysz na wzór jako układ równań liniowych, w którym masz równanie dla każdej klauzuli i zmienną dla każdej zmiennej. Na przykład formuła:

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

ma zadowalające przypisanie wtedy i tylko wtedy, gdy istnieje następujący układ równań:

x 2 + x 3 ≡ 1

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

I możemy znaleźć rozwiązania dla liniowych układów równań takich jak te w czasie wielomianowym, stosując eliminację Gaussa!

Dylan McKay
źródło
6

Tak. Można go rozwiązać dzięki eliminacji Gaussa. Eliminacja Gaussa może rozwiązać dowolny układ równań, który jest modułem liniowym. XOR działa jako moduł dodawania 2, więc każda klauzula XOR-SAT działa jako równanie liniowe modulo 2. W związku z tym eliminacja Gaussa może rozwiązać dowolną formułę XOR-k-SAT lub dowolną formułę XOR-SAT, nawet jeśli istnieje różna liczba literałów długości klauzul lub mieszanych, w czasie wielomianowym.

DW
źródło