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))
cc.complexity-theory
sat
big-list
Subhayan
źródło
źródło
Odpowiedzi:
(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:
źródło
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
Zobacz ten post .
źródło
Po stronie „NP-complete” natknąłem się na te warianty (zadałem również podobne pytanie na cs.stackexchange):
źródło
źródło
Oprócz powyższej listy są także:
źródło
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.
źródło