odmiany SAT

14

Spojrzałem w Internecie, ale nie mogłem znaleźć żadnej „dużej listy” wariantów problemu SAT.

Oprócz (wspólnego)

  • SAT,
  • k-SAT,
  • MAX-kSAT,
  • Half-SAT,
  • XOR-SAT,
  • NAE-SAT

jakie jeszcze są warianty?

(również będzie to bardzo przydatne, jeśli podano klasy złożoności (tam, gdzie to możliwe))

Subhayan
źródło
Jaki byłby cel tej listy?
Tyson Williams,
2
Po pierwsze dlatego, że chciałem przedstawić wykład studentom studiów licencjackich. Planowałem porozmawiać o odmianach SAT i pokazać niektóre (nietrywialne) redukcje ... oni już mieli kurs wprowadzający do TOC, więc pomyślałem, że to może być dobry pomysł .. A DRUGI POWÓD to fakt nie ma takiej listy w Internecie, ta lista będzie również służyć każdemu zaciekawionemu umysłowi, który chce wiedzieć o wariantach.
Subhayan
11
Nie jestem pewien, jak ta lista pomoże w twojej rozmowie. Zamiast czytać dowolnie długą listę wariantów SAT, ciekawy umysł powinien przeczytać twierdzenie dychotomii Schaefera i uogólnienie Allendera i in. pokazuje to, że każdy możliwy wariant SAT jest kompletny dla jednej z sześciu dobrze znanych klas złożoności.
Tyson Williams,
to miła sugestia ... dzięki @TysonWilliams .. możesz też zrobić z tego odpowiedź, chociaż nie tego dokładnie szukałem, ale z pewnością jest to pomocne.
Subhayan

Odpowiedzi:

17

(Uczynienie komentarza odpowiedzią zgodnie z żądaniem i nieco rozwinięcie).

„To ciekawy umysł” powinien przeczytać dychotomia twierdzenie Schaefer za i uogólnienie przez Allender et al. pokazuje to, że każdy możliwy wariant SAT jest albo trywialny, albo jedną z sześciu dobrze znanych klas złożoności:

  1. NP-complete
  2. P-kompletne
  3. NL-kompletne
  4. L-kompletne
  5. CompleteL-kompletne
  6. co-NLOGTIME
Tyson Williams
źródło
17

Ta lista będzie bardzo długa;) Oto niektóre z moich ulubionych (kompletnych NP) wariantów SAT:

  • PLANAR (3),3)

    Patrz: Dahlhaus, Johnson, Papadimitriou, Seymour, Yannakakis, Złożoność cięć multiterminalnych, SIAM Journal of Computing 23 (1994) 864-894

  • 4-BOUNDED PLANAR 3-CONNECTED 3SAT (każda klauzula zawiera dokładnie 3 różne zmienne, każda zmienna występuje w co najwyżej 4 klauzulach, dwubiegowy wykres incydentów jest płaski i 3-połączony)

    Patrz: Kratochvíl, Specjalny problem satysfakcji planarnej i konsekwencja jego kompletności NP, Dyskretna matematyka stosowana. 52 (1994) 233–252

  • MONOTONE CUBIC 1-IN-3SAT (MONOTONE-1-IN-3SAT, w którym każda zmienna pojawia się dokładnie 3 razy)

    Zobacz: Moore i Robsen, problem z twardymi przechyłami przy prostych płytkach, Discrete Compute. Geom. 26 (2001) 573-590

  • kk

    Zobacz ten post .

użytkownik13136
źródło
4
Jeśli uznasz ostatni punkt za interesujący, być może zainteresuje Cię również to, że # PLANAR-NAE-3SAT (rozwiązania zliczające) jest również wykonalny, podczas gdy inne pozornie proste warianty SAT, takie jak PLANAR-MONOTONE-2SAT, są wykonalne (lub nawet banalne) jako problem decyzyjny, ale # P-trudny do zliczenia. Zauważ, że redukcja z ostatniego powyższego linku (redukcja PLANAR-NAE-kSAT do PLANAR-NAE-3SAT) nie jest oszczędna i że # PLANAR-NAE-4SAT jest # P-twardy.
William Whistler
11

Po stronie „NP-complete” natknąłem się na te warianty (zadałem również podobne pytanie na cs.stackexchange):

Marzio De Biasi
źródło
7

S.ZAT.(k)S.ZAT.kS.ZAT.(2))L.S.ZAT.(k)k3)

Jan Johannsen
źródło
1

Oprócz powyższej listy są także:

  • #SAT: liczenie modeli
  • All-SAT: wyliczanie modelu
qsp
źródło
1

Istnieje bardzo klasyczne połączenie logiki z algebrą, które sięga początków współczesnej logiki i twórczości George'a Boole'a. Formułę w logice zdań można interpretować jako element algebry boolowskiej. Stałe logiczne prawda i fałsz stają się algebraicznymi pojęciami górnego i dolnego elementu sieci. Logiczne operacje koniunkcji, rozłączenia i negacji staną się algebraicznymi operacjami łączenia, łączenia i uzupełniania się w algebrze logicznej. To połączenie jest mniej podkreślane w nowoczesnych metodach logiki, ale jest szczególnie interesujące w kontekście twojego pytania. Algebra pozwala nam odejść od wielu szczegółów specyficznych dla problemu i znaleźć uogólnienia problemu, które będą miały zastosowanie w wielu różnych sytuacjach.

W konkretnym przypadku SAT pytanie algebraiczne, które można zadać, dotyczy tego, co dzieje się, gdy interpretujemy formuły w bardziej ogólnych sieciach niż algebry boolowskie. Po stronie logicznej można uogólnić problem satysfakcji od logiki zdań do logiki intuicyjnej. Mówiąc bardziej ogólnie, można uogólnić problem satysfakcji zdaniowej z problemem polegającym na określeniu, czy formuła, interpretowana w ramach ograniczonej sieci (jednej z górną i dolną częścią), definiuje dolny element sieci. To uogólnienie pozwala traktować problemy w analizie programu jako problemy dotyczące satysfakcji.

Innym uogólnieniem jest pozbawiona kwantyfikatora logika pierwszego rzędu, w której pojawia się pytanie o Modulo a Teoria Satisfiable. Oznacza to, że oprócz zmiennych logicznych masz również zmienne pierwszego rzędu i symbole funkcji i chcesz wiedzieć, czy formuła jest zadowalająca. W tym momencie możesz zadawać pytania o formuły arytmetyczne, teorie ciągów lub macierzy itp. Otrzymujemy więc ścisłą i bardzo przydatną uogólnienie SAT, który ma wiele aplikacji w systemach, bezpieczeństwie komputerowym, językach programowania, weryfikacji programów, planowaniu , sztuczna inteligencja itp.

Vijay D.
źródło