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. +more 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ů nebo při automatizovaném dokazování teorií, kdy je možné dokazovanou teorii transformovat 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.

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. +more 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". +more 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í. +more 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).

Kategorie:Logika