Rozhodovací procedury a verifikace – NAIL094
Úkol č.1 – Tseitinovo kódování
Naprogramujte převod formule do CNF:
- klasickým algoritmem (který produkuje ekvivalentní formuli)
- Tsetinovým kódováním (které produkuje ekvisplnitelnou formuli)
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á).