Rozšíření matched formulí

• Název práce v češtině: Rozšíření matched formulí
• Název v anglickém jazyce: Extensions to the class of matched formulae
• Klíčová slova: Matched formule, splnitelnost, maximální deficience formule.
• Klíčová slova anglicky: Matched formulae, satisfiability, maximum deficiency of a formula.
• Akademický rok vypsání: 2014/2015
• Typ práce: diplomová práce
• Jazyk práce: čeština
• Ústav: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Vedoucí / školitel: RNDr. Petr Kučera, Ph.D.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 23.03.2015
• Datum zadání: 23.03.2015
• Datum potvrzení stud. oddělením: 14.04.2015
• Datum a čas obhajoby: 08.09.2015 10:00
• Datum odevzdání elektronické podoby: 30.07.2015
• Datum odevzdání tištěné podoby: 30.07.2015
• Datum proběhlé obhajoby: 08.09.2015
• Oponenti: RNDr. Martin Babka

Zásady pro vypracování

Cílem diplomanta je navázat na známé algoritmy pro splnitelnost založené na matched formulích a pokusit se rozšířit tyto postupy pro třídy zobecňující matched formule. Vzhledem k tomu, že pro známá rozšíření matched formulí (biclique satisfiable a varsat) je těžké již rozpoznání toho, zda daná formule do dané třídy patří, měl by diplomant prozkoumat i heuristické přístupy jejichž kvalitu by měl ověřit na známých instancích pro splnitelnost používaných například při soutěžích řešičů splnitelnosti.

Seznam odborné literatury

[1] A. Biere. M. Heule, H. van Maaren, and T. Walsh. Handbook of Satisfiability, IOS Press 2009
[2] S. Szeider. Minimal Unsatisfiable Formulas with Bounded Clause-Variable Difference are Fixed-Parameter Tractable. Computinb and Combinatorics, LNCS 2697 (2003), Springer.
[3] S. Szeider. Generalizations of matched CNF formulas. Annals of Mathematics and Artificial Intelligence, 43 (2005), Springer.