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ů
- Stejný vstupní formát jako v úkolu č. 1.
- 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í.