odmiany SAT

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))

(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

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

• PLANAR ($\le 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

• $k$$k$

  Zobacz ten post .

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

• Planar 3-SAT;
• Planar 1-w-3 SAT i dodatni Planar 1-w-3 SAT (patrz Mulzer i Rote );
• NAE 3-SAT;
• 2/2/4-SAT (patrz Znalezienie najkrótszego rozwiązania dla rozszerzenia NxN 15-Puzzle jest niemożliwe do znalezienia przez D. Ratnera i M. Warmuth (1986) );
• XSAT, NAE-SAT dla liniowych form monotonicznych, XSAT dla dokładnych formuł liniowych (patrz dobra praca Ewalda Speckenmeyera na temat liniowych problemów XSAT: Złożoność obliczeniowa SAT, XSAT i NAE-SAT dla liniowych i mieszanych wzorów Horn CNF );
• k-colourable Monotone NAE-3SAT (patrz P Jain, Na wariancie Monotone NAE-3SAT i problem z cięciem bez trójkątów, 2010 ).

$\mathrm{SAT}(k)$$\mathrm{SAT}$$k$$\mathrm{SAT}(2)$$\mathsf{L}$$\mathrm{SAT}(k)$$k\geq 3$

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

• #SAT: liczenie modeli
• All-SAT: wyliczanie modelu

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.