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,

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:

(x_{1} \oplus x_{2} \oplus \neg x_{3} \oplus x_{5}) \land (x_{2} \oplus x_{3})

$(x_1\oplus x_2\oplus\lnot x_3\oplus x_5)\land (x_2\oplus x_3)$

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

x_{1} + x_{2} + (1 + x_{3}) + x_{5} \equiv 1 \mod 2

$x_1+x_2+(1+x_3)+x_5\equiv 1 \mod 2$

x_{2} + x_{3} \equiv 1 \mod 2

$x_2+x_3\equiv 1 \mod 2$

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