Splnitelnost

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání

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 v Booleovské logice pouze 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, jestli pro zadaný výraz žádné takové přiřazení neexistuje, taková skutečnost implikuje, že zadaná funkce vyjádřená pomocí stanovených 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í povahy této úlohy se zdůrazňuje pojem Booleovská resp. výroková splnitelnost.

SAT představuje první 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 P versus NP problém). 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[editovat | editovat zdroj]

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 \or \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 NL-ú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).