Bezpośrednia redukcja SAT do 3-SAT

Tutaj celem jest zredukowanie arbitralnego problemu SAT do 3-SAT w czasie wielomianowym przy użyciu jak najmniejszej liczby klauzul i zmiennych. Moje pytanie jest motywowane ciekawością. Mniej formalnie chciałbym wiedzieć: „Jaka jest„ najbardziej naturalna ”redukcja z SAT na 3-SAT?”

Teraz zmniejszenie, które zawsze widziałem w podręcznikach, wygląda mniej więcej tak:

1. Najpierw weź przykład SAT i zastosuj twierdzenie Cooka-Levina, aby zredukować je do obwodu SAT.

2. Następnie kończysz zadanie standardową redukcją obwodu SAT do 3-SAT, zastępując bramki klauzulami.

Podczas gdy to działa, wynikowe klauzule 3-SAT wyglądają prawie tak samo jak klauzule SAT, z którymi zacząłeś, ze względu na początkowe zastosowanie twierdzenia Cooka-Levina.

Czy ktoś może zobaczyć, jak zrobić redukcję bardziej bezpośrednio, pomijając etap obwodu pośredniego i przechodząc bezpośrednio do 3-SAT? Byłbym nawet szczęśliwy z bezpośredniej redukcji w specjalnym przypadku n-SAT.

(Sądzę, że istnieją pewne kompromisy między czasem obliczeń a wielkością wyjściową. Oczywiście zdegenerowane - choć na szczęście niedopuszczalne, chyba że P = NP - rozwiązaniem byłoby po prostu rozwiązanie problemu SAT, a następnie wyemitowanie trywialnych 3 -Sat wystąpienie ...)

EDYCJA: Na podstawie odpowiedzi Ratcheta jest teraz jasne, że redukcja do n-SAT jest dość trywialna (i że naprawdę powinienem był to przemyśleć nieco bardziej ostrożnie przed opublikowaniem). Pozostawiam to pytanie na chwilę na wypadek, gdyby ktoś znał odpowiedź na bardziej ogólną sytuację, w przeciwnym razie po prostu zaakceptuję odpowiedź zapadkową.

Każda klauzula SAT ma 1, 2, 3 lub więcej zmiennych. Klauzulę 3 zmiennych można skopiować bez problemu

W 1 i 2 zmienne klauzule {a1}i {a1,a2}może być rozszerzony {a1,a1,a1}i {a1,a2,a1}odpowiednio.

Klauzula o więcej niż 3 zmiennych {a1,a2,a3,a4,a5}może być rozszerzona do {a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5}z s1oraz s2nowe zmienne, których wartość zależy od rodzaju zmienna w oryginalnej klauzuli jest prawdą

Prawdopodobnie jest to poza zakresem pytania, ale i tak chciałem to opublikować. Przy użyciu technik ze sparametryzowanej złożoności udowodniono, że przy założeniu, że hierarchia wielomianowa nie zawali się do swojego trzeciego poziomu, nie ma algorytmu wielomianowego, który bierze instancję CNF-SAT na n zmiennych o nieograniczonej długości klauzuli i wysyła wystąpienie k-CNF-SAT (brak klauzul długości większych niż k) na zmiennych gdzie n ' jest wielomianem w$n'$$n$

Jeśli potrzebujesz redukcji z k-SAT na 3-SAT, to odpowiedź zapadki działa dobrze.

Jeśli chcesz bezpośredniej redukcji z ogólnej formuły zdań do CNF (i do 3-SAT), to - przynajmniej z „perspektywy solverów SAT” - myślę, że odpowiedź na twoje pytanie Czym jest „najbardziej naturalna” redukcja ... ? , jest: Nie ma „naturalnej” redukcji !

Z wniosków rozdziału 2 - „Kodowanie CNF” (bardzo dobrej) książki: Handbook of Satisfiable :

...
Zazwyczaj istnieje wiele sposobów modelowania danego problemu w CNF, a niewiele jest znanych wytycznych dotyczących wyboru spośród nich. Często istnieje wybór funkcji problemowych, które można modelować jako zmienne, a niektóre z nich mogą wymagać zastanowienia. Kodowania tseityny są kompaktowe i można je mechanizować, ale w praktyce nie zawsze prowadzą do najlepszego modelu, a niektóre podformulacje można lepiej rozszerzyć. Niektóre klauzule mogą zostać pominięte ze względu na polaryzację, a sugerowane mogą być klauzule łamania symetrii lub blokowane. Różne kodowania mogą mieć różne zalety i wady, takie jak rozmiar lub gęstość rozwiązania, a zaletą jednego solwera SAT może być wada innej. Krótko mówiąc, modelowanie CNF jest sztuką i często musimy postępować intuicyjnie i eksperymentować.
...

Najbardziej znanym algorytmem jest Tseitin (G. Tseitin. O złożoności wyprowadzania w rachunku zdań. Automatyzacja rozumowania: dokumenty klasyczne w logice obliczeniowej, 2: 466–483, 1983. Springer-Verlag.)

Aby uzyskać dobre wprowadzenie do kodowania CNF, przeczytaj sugerowaną książkę Handbook o Satisfiable . Możesz także przeczytać najnowsze prace i przejrzeć odniesienia; na przykład:

• P. Jackson i D. Sheridan. Klauzula postaci konwersji dla obwodów boolowskich. W HH Hoos i DG Mitchell, redaktorzy, Theory and Applications of Satisfiable Testing, 7. Międzynarodowa Konferencja, SAT 2004 , tom 3542 LNCS, strony 183–198. Springer, 2004. (który ma na celu zmniejszenie liczby klauzul)
• P. Manolios, D. Vroon, Efficient Circuit to CNF Conversion. W teorii i zastosowaniach testów satysfakcji - SAT 2007 (2007), s. 4-9

Pozwól, że opublikuję inne rozwiązanie podobne do Ratchel, ale nieco inne. Zostało to zaczerpnięte bezpośrednio z rozdziału 9 2. wydania „Podręcznika projektowania algorytmów” Stevena Skieny

• Jeśli klauzula ma tylko jedną literalną C = {z1}, utwórz dwie nowe zmienne v1 i v2 oraz cztery nowe 3-literalne klauzule: {v1, v2, z1}, {! V1, v2, z1}, {v1,! v2, z1} i {! v1,! v2, z1}. Zauważ, że jedynym sposobem na jednoczesne spełnienie wszystkich czterech klauzul jest z1 = T, co oznacza również, że oryginalne C zostanie spełnione
• Jeśli klauzula ma dwa literały, C = {z1, z2}, następnie utwórz jedną nową zmienną v1 i dwie nowe klauzule: {v1, z1, z2} i {! V1, z1, z2}. Ponownie, jedynym sposobem spełnienia obu tych klauzul jest spełnienie co najmniej jednego z z1 i z2, spełniając w ten sposób C
• Jeśli klauzula ma trzy literały, C = {z1, z2, z3}, po prostu skopiuj C do instancji 3-SAT bez zmian
• Jeśli klauzula ma więcej niż 3 literały C = {z1, z2, ..., zn}, następnie utwórz n-3 nowych zmiennych i n-2 nowych klauzul w łańcuchu, gdzie dla 2 <= j <= n-2 , Cij = {v1, j-1, zj + 1,! Vi, j}, Ci1 = {z1, z2,! Vi, 1} i Ci, n-2 = {vi, n-3, zn-1, zn}