Témata pro diplomové a bakalářské práce

Zde jsem shromáždil několik možných témat diplomových prací. Všeobecně pokud máte zájem o diplomovou práci z oblasti booleovských funkcí budu rád, když se mi ozvete. Konkrétní téma můžeme uzpůsobit dle aktuálního zájmu.

• Úpravy a heuristiky v SAT solverech
• Aplikace SAT solverů na konkrétní problémy
• Kompilace do různých reprezentací booleovských funkcí (například do DNNF a odvozených struktur, disjunkce skrytě hornovských formulí)
• Kódování problémů a podmínek do KNF v podobě vhodné pro SAT solvery
• Parametrizované a heuristické algoritmy pro úlohy související se SAT a reprezentacemi booleovských funkcí
• Minimální reprezentace booleovských funkcí

Konkrétnější témata

Efektivní DP eliminace

Davisův-Putnamův algoritmus je algoritmus pro test splnitelnosti formule v konjunktivní normální formě. Je založen na rezoluci, která je použita k postupné eliminaci proměnných. Jde o specifickou formu rezoluce, které se též říká DP rezoluce. V současnosti se používá DP rezoluce pro eliminaci proměnných ve formulích. Cílem práce by byla efektivní implementace tohoto postupu, která by byla použitelná i pro velké formule. Jde o volbu vhodných datových struktur pro reprezentaci množiny klauzulí (například set-trie) a volbu vhodných heuristik pro výběr další proměnné k eliminaci.

Dualizace formulí v konjunktivní normální formě s pomocí SAT solverů

Jde o problém, jehož instancí je formule v konjunktivní normální formě (KNF) a cílem je sestrojit ekvivalentní formuli v disjunktivní normální formě (DNF). Tento problém je zejména zkoumaný pro případ monotónních formulí, pro něž je popsán superpolynomiální algoritmus, který tento problém řeší. Objevil se i jeden článek, který s pomocí SAT solverů řešil související problém, v němž se testuje ekvivalence monotónní KNF s DNF. Cílem by bylo prozkoumat současné postupy, implementovat je, zobecnit je pro případ konstrukce DNF (ne jen test ekvivalence) a pokusit se o vylepšení.

Anotace PDF zpět do LaTeXu

Cílem by bylo vytvořit systém, kterým by bylo možno anotace, které jsou vytvořené v PDF souboru dostat zpět do zdrojového kódu v LaTeXu (z něhož byl PDF soubor vytvořen a který je přístupný). Na straně LaTeXu by bylo možno využít SyncTeX a balík pdfcomment. Jedná se zejména o anotace typu zvýraznění, komentář, případně textový box atp. Příklad použití: Vytvořím PDF v LaTeXu, vyznačím si v něm pomocí anotací, co chci v dokumentu opravit, programem anotace dostanu zpět do zdrojového kódu, kde je již rovnou mohu využít v běžném editoru pro úpravu zdrojového kódu podle požadovaných změn. Je možné uvažovat i o tom, že pokud by byly v textových anotacích zvláštní příkazy, mohl by být na základě nich přímo nahrazen text ve zdrojovém kódu. Například, označím text v PDF a potom se tento text přímo nahradí novým, který bude uveden v komentáři specifikovaného tvaru, např. uvozen pomocí REPLACE. Anotace přeškrtnutí by mohla rovnou vést k vymazání dané části z textu atp.