Název: Třídy Booleovských formulí s efektivně řešitelným SATem.
Překlad názvu: Classes of Boolean Formulae with effectively soluable SAT.
Autoři: Vlček, Václav
Typ dokumentu: Rigorózní práce
Rok: 2014
Jazyk: cze
Abstrakt: [cze] [eng]
Práce se zabývá třídami Booleovských formulí, pro které je problém splnitelnosti (SAT) řešitelný v polynomiálním čase. Zkoumá chování těchto tříd vzhledem k základním operacím s formulemi (komplementaci literálu, komplementaci proměnné, odebrání literálu nebo klauzule, částečné dosazení a spojení formulí). Dále se zabývá problémem rozpoznávání náležení formule do dané třídy, rozpoznávání splnitelnosti dané formule a vzájemnými vztahy těchto tříd vzhledem k inkluzi. This work studies classes of Boolean formulae with polynomially solvable satsiability problem (SAT). It investigates the behavior of these classes with respect to basic operation with formulae (variable and literal complementation, deletition of a literal or a clause, partial assignment and joining formulae). Furthermore the work studies recognition problems for a formula and a given class of functions, satisability testing, and mutual relations of the studied classes with respect to inclusion.
Klíčová slova: SAT; splnitelnost; třídy booleovských formulí; classes of boolean formulae; SAT; satisfiability

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/61272

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-438905


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Rigorózní práce