Splnitelnost

Splnitelnost (často zkracovaná jako SAT z anglického satisfiability) je v logice problém, zda pro daný logický výraz s proměnnými (formuli) existují takové přípustné hodnoty proměnných, aby formule byla pravdivým výrokem. Taková formule se pak zove splnitelná (anglicky satisfiable), v opačném případě (kdy při jakékoli hodnotě vstupů dává nepravdivý výrok) je nesplnitelná (unsatisfiable),

Konkrétně ve výrokové logice, kde se používají binární proměnné (pravda/nepravda) a operace AND, OR a NOT, se problém splnitelnosti nazývá problém splnitelnosti booleovské formule a používá se pojem booleovská splnitelnost.

SAT je obecně 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ů 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 jako instanci SAT[zdroj?!]. 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 představuje pozitivní literál a představuje negativní literál.

Klauzule je disjunkce literálů. Například 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).