Boolean satisfiability problem
Boolean satisfiability problem (SAT) je problém v oblasti počítačové teorie a logiky, který se zabývá otázkou, zda je možné přiřadit pravdivostní hodnoty proměnným v logickém výrazu tak, aby celý výraz byl pravdivý. SAT se obvykle představuje ve formátu CNF (konjunktivní normální formě), což znamená, že výrazy jsou zapsány jako součin disjunkcí literálů. Tento problém je první příkladem NP-úplného problému, což znamená, že je velmi obtížné nalézt efektivní algoritmus, který by jej vyřešil v rozumném čase pro všechny případy. Existuje mnoho různých algoritmů a technik vyvinutých pro řešení SAT, včetně DPLL algoritmu a dalších modernějších metod, jako jsou SAT solver, které se široce využívají v oblastech jako je automatizované dokazování teoremat, ověřování hardwaru a softwaru či při plánování a optimalizaci.