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í

Termín odevzdání je 30. 6. Pokud se dostanete do časové tísně, a úkol nestihnete, můžete mi jej poslat i během prázdnin. Snažte se to ale stihnout dříve.

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.

Alternativně lze poslat link na repozitář, kde se nachází výše popsané.