Rozhodovací procedury a verifikace – NAIL094

Úkol č.2 – DPLL algoritmus

Naprogramujte základní DPLL algoritmus: prohledávání stromu částečných ohodnocení s využitím jednotkové propagace. Váš program by měl být schopen spracovat 2 druhy vstupních souborů

1. Stejný vstupní formát jako v úkolu č. 1.
2. DIMACS formát jak je popsán zde.

Výstupem je odpověď na standardní výstup: SAT nebo UNSAT. V případě SAT vypište i splňující ohodnocení.

Pro testování můžete použít příklady z prvního úkolu, následně svůj solver vyskoušejte na menších příkladech z této stránky. Vyberte si pár příkladů z kategorie Uniform Random-3-SAT, změřte časy běhu a napište krátkou správu jak si váš solver vede pro rostoucí zložitost problémů.

Deadline: 8.4.2018 23:59

Hodnocení: Za úkol můžete získat až 5 bodů. Hodnotí se funkčnost kód a taky správa s naměřenými statistikami.

Poznámka: V dalších úkolech budete rozšiřovat tento základní algoritmus o reprezentaci pomocí two watched literals, učení klauzulí a rozhodovací heuristiky. Mějte to na paměti a můžete začít integrovat některé tyto prvky již nyní.