Splnitelnost

V logice představuje splnitelnost (často zkracovaná jako SAT z anglického satisfiability) problém odpovědi na otázku, zdali existuje zadanému výrazu (formuli) zapsaného ve výrokové ... Booleovské logice například pomocí operací AND, OR a NOT přiřazení, při kterém bude výraz ohodnocen jako pravdivý. Zároveň je důležité určit,^[zdroj⁠?] jestli pro zadaný výraz žádné takové přiřazení neexistuje, taková skutečnost implikuje, že zadaná funkce vyjádřená pomocí stanovených^[zdroj⁠?] formulí je kontradikce (tedy že při jakémkoli vstupu je na výstupu hodnota FALSE) - při takové situaci říkáme, že je funkce nesplnitelná (anglicky unsatisfiable), jinak je funkce splnitelná (satisfiable). Například výraz a AND b je splnitelný, protože existují hodnoty a = TRUE and b = TRUE, na při kterých výraz (a AND b) = TRUE. Pro zdůraznění binární^[zdroj⁠?] povahy této úlohy se zdůrazňuje pojem Booleovská resp. výroková splnitelnost.

SAT představuje první^[zdroj⁠?] známý NP-úplný problém. To ve zkratce znamená, že není znám žádný efektivní algoritmus řešící všechny instance SAT problému v polynomiálním čase. Obecně se předpokládá, že takový algoritmus neexistuje (není to však dokázáno, viz Problém P versus NP). Dále může být široká škála přirozeně se vyskytujících problémů při rozhodování a optimalizacích transformována jako SAT problém. Třída algoritmů^[zdroj⁠?] nazývaná SAT solvery může efektivně vyřešit dostatečně velké podmnožiny instancí SAT a být tak užitečná při řadě praktických aplikací, jako například při návrhu elektrických obvodů^[zdroj⁠?] nebo při automatizovaném dokazování teorií, kdy je možné dokazovanou teorii transformovat^[zdroj⁠?] jako instanci SAT. Rozšiřování potenciálu SAT solverů představuje v současnosti značně pokrokovou oblast, avšak prozatím neexistuje žádná metoda pro efektivní řešení všech instancí SAT.^[zdroj⁠?]

Základní definice, terminologie a aplikace

V teorii složitosti představuje otázka splnitelnosti (resp. SAT) rozhodnutí, jehož dílčí části formují pouze Booleovské výrazy (formule) zapsané pomocí AND, OR, NOT, proměnných a závorek. Otázka zní: existují pro proměnné zadané formule hodnoty TRUE nebo FALSE v takové kombinaci, při které bude celá formule nabývat hodnoty TRUE? Pokud taková kombinace existuje, označujeme Booleovskou formuli jako splnitelnou a ekvivalentně pokud taková kombinace neexistuje, je formule nesplnitelná. Problém splnitelnosti Booleovských formulí je NP-úplný. Problém splnitelnosti výroku (též PSAT za anglického propositional satisfiability problem) tedy rozhodnutí, zdali zadaná výroková formule je splnitelná či nikoli, představuje klíčovou úlohu v mnoha oblastech informatiky, včetně teoretické informatiky, algoritmizace, umělé inteligence, návrhu hardware, automatizace návrhu elektroniky a dalších.

Literál je buď proměnná nebo negace proměnné (negace výrazu může být redukována na negované proměnné pomocí De Morganových zákonů). Například $\textstyle {x_{1}}$ představuje pozitivní literál a $\neg x_{2}$ představuje negativní literál.

Klauzule je disjunkce literálů. Například $x_{1}\lor \neg x_{2}$ je klauzule (čti "x-jedna nebo non-x-dva").

Existuje několik speciálních případů splnitelnosti, kdy je požadováno, aby ve formuli byly v konjunkci klauzulí (jedná se formule v konjunktivní normální formě). Určení splnitelnosti formule v konjunktivní normální formě, kde každá klauzule je omezena na nejvýše tři literály představuje NP-úplný problém, tento problém se nazývá "3SAT", "3CNFSAT", nebo "3-satisfiability". Určení splnitelnosti formule, ve kterém je každá klauzule omezena na nejvýše dva literály je P-úplný problém, tento problém se nazývá "2SAT". Určení splnitelnosti formule, v níž každá klauzule je Hornova klauzule (tj. obsahuje nanejvýš jeden pozitivní literál) je P-úplný problém, tento problém se nazývá Hornova-splnitelnost.

Cook-Levinova teorie tvrdí, že splnitelnost Booleovských formulí je NP-úplný problém, a fakticky představuje první problém, u kterého byla prokázána NP-úplnost. Nicméně, nad rámec této teorie, je třeba zmínit, že efektivní algoritmy pro SAT vyvinuté v průběhu posledního desetiletí přispěly k dramatickému pokroku v našich možnostech automatizovaně řešit problémové případy zahrnující desítky tisíc proměnných a miliony dalších omezení. Ukázky těchto problémů v oblasti automatizace návrhu elektroniky (EDA) zahrnují formální kontrolu rovnocennosti, kontrolu modelů, formální verifikaci pipeline mikroprocesorů, automatické generování testovacího vzoru, směrování FPGA atd. V současnosti se zvažuje využití SAT solveru jakožto základní komponenty pro automatizované návrhy elektroniky (EDA).