Rozhodovací procedury a verifikace – NAIL094

Úkol č.1 – Tseitinovo kódování

Naprogramujte převod formule do CNF:

1. klasickým algoritmem (který produkuje ekvivalentní formuli)
2. Tsetinovým kódováním (které produkuje ekvisplnitelnou formuli)

Můžete předpokládat, že vstupní formule je v NNF. Odevzdávejte zdrojové kódy spolu s krátkou zprávou, kde porovnáte velikosti formulí z obou algoritmů.

Bonus: Můžete zkusit naprogramovat různé verze Tseitinovho kódování a porovnat je mezi sebou.

Vstupy: Použijeme (hodně) zjednodušenou syntax jazyka SMT-LIB. Vstupní soubor obsahuje jednu formuli a ta splňuje tato gramatická pravidla:
formula ::= (and formula formula) | (or formula formula) | (not formula) | var_identifier
kde var_identifier je sekvence alphanumerických znaků začínajících písmenem.
Vstupní soubory zde.

Deadline: 11.3.2018 23:59

Hodnocení: Za úkol můžete získat až 5 bodů (plus 1 bonusový pro různé varianty Tseitina) Hodnotí se funkčnost kódu ale také zpráva se statistikami pro jednotlivé algoritmy.

Poznámka: Snažte se prosím psát přehledný kód s vysvětlujícími komentáři. Myslete na to, že to po vás bude číst další člověk (já).