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⁠?]