Zobrazení zdroje stránky Problém splnitelnosti booleovské formule

'''Problém splnitelnosti booleovské formule''' (anglickou zkratkou '''SATISFIABILITY''' nebo '''SAT''') je v [[Matematická logika|matematické logice]] úloha zjistit, zda existuje interpretace, která [[Splnitelnost|vyhovuje]] dané [[Booleova algebra|booleovské]] formuli. Jedná se o jednu konkrétní formulaci obecnějšího problému [[Splnitelnost|splnitelnosti]]. Jde tedy o to, zda proměnné daného booleovského výrazu s proměnnými (formule) mohou být nahrazeny hodnotami TRUE (pravda) nebo FALSE (nepravda) takovým způsobem, že se výsledný výraz vyhodnotí jako pravdivý (TRUE). Pokud je tomu tak, formule se nazývá ''splnitelná''. V opačném případě výraz má hodnotu FALSE pro všechna možná přiřazení proměnných a formule je ''nesplnitelná''. Například formule ''„a'' AND NOT ''b“'' je splnitelná, protože po dosazení ''a'' =&nbsp;TRUE a ''b'' = FALSE je výraz (TRUE AND NOT FALSE) = TRUE. Naopak formule ''„a'' AND NOT ''a''“ je nesplnitelná (jinými slovy tato formule vyjadřuje protimluv, [[Kontradikce|kontradikci]]).

SAT byl první problém, u kterého se ukázalo, že je [[NP-úplnost|NP-úplný]]; viz [[Cookova–Levinova věta]]. To znamená, že všechny problémy ve třídě složitosti [[NP (třída složitosti)|NP]], která zahrnuje širokou škálu přirozených rozhodovacích a optimalizačních problémů, jsou nejméně tak obtížné jako SAT. Neexistuje žádný známý algoritmus, který by účinně (tj. v polynomiálním čase) vyřešil libovolný problém SAT, a obecně se věří, že takový algoritmus neexistuje. Přesto to nebylo dokázáno a otázka, zda pro SAT existuje [[Asymptotická složitost|polynomiálně složitý]] algoritmus, je ekvivalentem [[Problém P versus NP|problému P versus NP]], což je slavný otevřený problém teorie algoritmů.

Existují však [[heuristické algoritmy]] schopné řešit úlohy SAT s desítkami tisíc proměnných a s vzorci sestávajícími z milionů symbolů, což je dostačující pro mnoho praktických problémů SAT, např. v oblastech [[Umělá inteligence|umělé inteligence]], [[Návrh elektronických obvodů|návrhu elektronických obvodů]] a [[Automatické dokazování vět|automatického dokazování vět]].

== Reference ==
{{Překlad|en|Boolean satisfiability problem|931374507}}

== Externí odkazy ==
* {{Commonscat}}
{{Autoritní data}}

[[Kategorie:NP-úplné problémy]]
[[Kategorie:Matematická logika]]