sift

sift to solver SAT oparty na algorytmie DPLL, napisany w Haskellu, wraz z zestawem narzędzi logiki zdaniowej: parserem formatu DIMACS i tłumaczeniem formuł do postaci CNF metodą Tseitina. Nie jest ćwiczeniem na papierze - rozwiązuje realne instancje.

SAT to jedno z tych zagadnień, które łączą pozorną prostotę z ogromną głębią. Pytanie brzmi niewinnie, a odpowiedź na nie potrafi rozstrzygnąć problemy z zupełnie innych dziedzin. Ten projekt dotyka właśnie tego rdzenia, i to od strony, która zmusza do zrozumienia, dlaczego solver w ogóle działa.

SAT pyta o rzecz na pozór banalną: czy da się tak dobrać wartości logiczne, żeby cała formuła była prawdziwa? Banalne aż do momentu, gdy zmiennych są setki, a od odpowiedzi zależy planowanie, weryfikacja układów albo rozwiązanie łamigłówki. Solver SAT siedzi pod wieloma trudnymi problemami, które najpierw tłumaczy się na jego język.

Standardowe wejście to format DIMACS - każda linia to klauzula, liczby to zmienne, minus to negacja, zero kończy klauzulę. Prosty tekst, który potrafi zakodować zaskakująco trudne pytania.

DPLL to inteligentne przeszukiwanie z nawrotami. Zamiast próbować wszystkich kombinacji, na każdym kroku wybiera zmienną, zakłada jej wartość i pilnuje dwóch skrótów: jeśli klauzula ma tylko jeden nierozstrzygnięty literał, jego wartość jest wymuszona; jeśli zmienna występuje zawsze w tej samej postaci, można ją od razu ustawić.

To właśnie te dwa skróty robią różnicę między sekundą a wiecznością. Bez nich solver błądzi po drzewie wszystkich możliwości; z nimi całe poddrzewa odpadają, zanim w ogóle zostaną odwiedzone. Zaimplementowanie ich poprawnie jest sercem całego solvera.

DPLL wymaga formuły w postaci CNF, ale nie każda formuła już taka jest. Naiwne przekształcenie potrafi wysadzić jej rozmiar wykładniczo, zamieniając mały problem w gigantyczny jeszcze przed startem solvera. Metoda Tseitina wprowadza pomocnicze zmienne i utrzymuje wzrost liniowy.

Na wyjściu jest działający solver, który bierze realne instancje w formacie DIMACS i zwraca odpowiedź, a po drodze tłumaczy dowolną formułę do CNF bez wysadzania jej rozmiaru. Napisany w Haskellu, bo dopasowanie wzorca i typy pilnujące poprawności sprawiają, że logika czyta się niemal jak matematyka. Mały projekt, który dotyka bardzo głębokiej części informatyki - i naprawdę ją rozwiązuje.