sift

sift è un solver SAT basato sull'algoritmo DPLL, scritto in Haskell, insieme a un kit di strumenti di logica proposizionale: un parser del formato DIMACS e la traduzione di formule nella forma CNF con il metodo di Tseitin. Non è un esercizio sulla carta - risolve istanze reali.

SAT è uno di quei problemi che uniscono un'apparente semplicità a una profondità enorme. La domanda suona innocente, eppure la sua risposta può risolvere problemi di ambiti del tutto diversi. Questo progetto tocca proprio quel nucleo, e da un lato che costringe a capire perché un solver funzioni.

SAT chiede una cosa in apparenza banale: si possono scegliere valori di verità in modo che tutta la formula sia vera? Banale fino al momento in cui le variabili sono centinaia e dalla risposta dipendono la pianificazione, la verifica di circuiti o la soluzione di un rompicapo. Un solver SAT si trova sotto molti problemi difficili che prima vengono tradotti nel suo linguaggio.

L'input standard è il formato DIMACS - ogni riga è una clausola, i numeri sono variabili, un meno è una negazione, uno zero chiude una clausola. Testo semplice che sa codificare domande sorprendentemente difficili.

DPLL è una ricerca intelligente con backtracking. Invece di provare tutte le combinazioni, a ogni passo sceglie una variabile, ne ipotizza il valore e sorveglia due scorciatoie: se una clausola ha un solo letterale ancora indeciso, il suo valore è forzato; se una variabile compare sempre nella stessa forma, la si può impostare subito.

Sono proprio queste due scorciatoie a fare la differenza tra un secondo e un'eternità. Senza di esse il solver vaga per l'albero di tutte le possibilità; con esse interi sottoalberi cadono prima ancora di essere visitati. Implementarle correttamente è il cuore di tutto il solver.

DPLL richiede una formula in CNF, ma non ogni formula lo è già. Una conversione ingenua può far esplodere la sua dimensione in modo esponenziale, trasformando un piccolo problema in uno gigantesco ancora prima dell'avvio del solver. Il metodo di Tseitin introduce variabili ausiliarie e mantiene la crescita lineare.

Ne esce un solver funzionante che prende istanze reali in formato DIMACS e restituisce una risposta, e lungo la strada traduce qualsiasi formula in CNF senza farne esplodere la dimensione. Scritto in Haskell, perché il pattern matching e i tipi che vegliano sulla correttezza fanno leggere la logica quasi come matematica. Un piccolo progetto che tocca una parte molto profonda dell'informatica - e la risolve davvero.