Vybraná témata z algoritmů - úkol

Zadání úkolu

Naprogramujte sat solver založený na algoritmu DPLL (s unit propagací) a vyhodnoťte jeho výkon na vhodném datasetu. (Další vylepšení jsou volitelná). Očekává se, že studenti se budou snažit o co nejefektivnější implementaci.

Použití programu

Použití programu je

solver input.cnf

kde solver je jméno spustitelného souboru a input.cnf je soubor s formulí v DIMACS formátu

Výstup programu

Na standardní výstup vypíše program následující:

• První řádek výsledek, buď SAT nebo UNSAT
• Pokud je výsledek SAT, obsahuje druhý řádek seznam pravdivých literálů, uspořádaný vzestupně podle čísla proměnné. Pokud je výsledek UNSAT, je druhý řádek prázdný
• Třetí řádek obsahuje procesorový čas potřebný pro načtení a inicializaci
• Čtvrtý řádek obsahuje procesorový čas při potřebný pro výpočet
• Pátý řádek je počet aplikací unitární propagace během výpočtu
• Šestý řádek je počet vrcholů ve stromu rekurze, které odpovídají rozhodovací proměnné (strom rekurze může být pouze virtuální, algoritmus může být implementován iterativně).

Testovací datasety

Benchmarky (.zip)

Adresáře n-vars obsahují formule s n proměnnými, adresář coloring obsahuje formule získané z barvení grafu rozdělené do podadresářů podle velikostí grafu, adresář pigeon-hole obsahuje formule získané z formalizace pigeonhole principu.

Podle splnitelnosti jsou soubory v adresářích sat a unsat.

Odevzdání

Odevzdávejte mailem. V příloze pošlete archiv obsahující:

• zdrojové kódy a README obsahující návod pro sestavení a spuštění
• dokument obsahující rozumné experimentální vyhodnocení.

Archiv nesmí obsahovat spustitelné soubory!! Volba jazyka je na studentech, preferuji věci snadno spustitelné na unixovém systému (jiné systémy ale nejsou zakázány).