Vybraná témata z algoritmů - úkol

Zadání úkolu

Naprogramujte sat solver založený na algoritmu DPLL a vyhodnoťte jeho výkon na vhodném datasetu. 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ě).

DIMACS formát

Textový formát. Řádky začínající c jsou komentáře. První řádek je

p cnf <variables> <clauses>

kde <variables> a <clauses> jsou celá čísla udávající počet proměnných a počet klauzulí. Na dalších řádcích jsou klauzule. Každá klauzule je uložena jako posloupnost celých čísel oddělených mezerami, která je ukončena 0 (Typicky je celá na jednom řádku). Přitom se předpokládá, že proměnné jsou čísla 1,2,…. Negativní literály jsou záportná čísla. Formuli {{x, y, ¬z}, {¬y, z}} můžeme uložit jako

p cnf 3 2
1 2 -3 0
-2 3 0

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í. Například tabulka, případně graf s výkonem solveru na benchmarku – to může být i informace o tom, že solver daný benchmark nezvládl.

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