Array ( [0] => 15012202 [id] => 15012202 [1] => cswiki [site] => cswiki [2] => Splnitelnost [uri] => Splnitelnost [3] => [img] => [4] => [day_avg] => [5] => [day_diff] => [6] => [day_last] => [7] => [day_prev_last] => [8] => [oai] => [9] => [is_good] => [10] => [object_type] => [11] => 0 [has_content] => 0 [12] => [oai_cs_optimisticky] => ) Array ( [0] => '''Splnitelnost''' (často zkracovaná jako '''SAT''' z anglického ''satisfiability'') je v [[logika|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''), [1] => [2] => Konkrétně ve [[Booleova logika|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.'' [3] => [4] => SAT je obecně [[NP-úplnost|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 solver]]y 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ý obvod|elektrických obvodů]]{{Fakt/dne|20140829214939}} nebo při automatizovaném dokazování teorií, kdy je možné dokazovanou teorii transformovat jako instanci SAT{{Fakt/dne|20140829214939}}. 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.{{Fakt/dne|20140829214939}} [5] => [6] => == Základní definice, terminologie a aplikace == [7] => V [[Teorie složitosti|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-úplnost|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 [[informatika|informatiky]], včetně [[teoretická informatika|teoretické informatiky]], [[Algoritmus|algoritmizace]], [[Umělá inteligence|umělé inteligence]], návrhu [[hardware]], automatizace návrhu elektroniky a dalších. [8] => [9] => '''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 Morganovy zákony|De Morganových zákonů]]). Například \textstyle{x_1} představuje '''pozitivní literál''' a \neg x_2 představuje '''negativní literál'''. [10] => [11] => '''Klauzule''' je [[disjunkce]] literálů. Například x_1 \lor \neg x_2 je klauzule (čti "x-jedna nebo non-x-dva"). [12] => [13] => Existuje několik speciálních případů splnitelnosti, kdy je požadováno, aby ve formuli byly v [[Konjunkce (matematika)|konjunkci]] klauzulí (jedná se formule v [[Konjunktivní normální forma|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 [[P (třída složitosti)|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]]. [14] => [15] => [[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í kontrola rovnocennosti|formální kontrolu rovnocennosti]], kontrolu modelů, formální verifikaci [[Mikroprocesor|pipeline mikroprocesorů]], automatické generování testovacího vzoru, směrování [[Programovatelné hradlové pole|FPGA]] atd. V současnosti se zvažuje využití SAT solveru jakožto základní komponenty pro automatizované návrhy elektroniky (EDA). [16] => {{Autoritní data}} [17] => [18] => [[Kategorie:Logika]] [] => )
good wiki

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.

More about us

About

Expert Team

Vivamus eget neque lacus. Pellentesque egauris ex.

Award winning agency

Lorem ipsum, dolor sit amet consectetur elitorceat .

10 Year Exp.

Pellen tesque eget, mauris lorem iupsum neque lacus.

You might be interested in

,'NP-úplnost','informatika','Programovatelné hradlové pole','Formální kontrola rovnocennosti','Hornova-splnitelnost','Hornova klauzule','P (třída složitosti)','Konjunkce (matematika)','disjunkce','De Morganovy zákony','hardware','Umělá inteligence'

Disjunkce

Hardware

Informatika

NP-úplnost