sift

sift is a SAT solver based on the DPLL algorithm, written in Haskell, together with a propositional-logic toolkit: a DIMACS format parser and formula translation to CNF via the Tseitin method. It is not a paper exercise - it solves real instances.

SAT is one of those problems that pair apparent simplicity with enormous depth. The question sounds innocent, yet its answer can settle problems from entirely different fields. This project touches that very core, and from an angle that forces you to understand why a solver works at all.

SAT asks a deceptively trivial thing: can you pick truth values so the whole formula comes out true? Trivial until there are hundreds of variables and the answer decides scheduling, circuit verification or solving a puzzle. A SAT solver sits under many hard problems that get translated into its language first.

The standard input is the DIMACS format - each line is a clause, numbers are variables, a minus is negation, and a zero ends a clause. Plain text that can encode surprisingly hard questions.

DPLL is smart search with backtracking. Instead of trying every combination, at each step it picks a variable, assumes a value, and watches two shortcuts: if a clause has only one undecided literal, that value is forced; if a variable always appears in the same form, it can be set right away.

Those two shortcuts are the difference between a second and an eternity. Without them the solver wanders the tree of all possibilities; with them whole subtrees fall away before they are ever visited. Implementing them correctly is the heart of the whole solver.

DPLL requires a formula in CNF, but not every formula already is. A naive conversion can blow up its size exponentially, turning a small problem into a giant one before the solver even starts. The Tseitin method adds helper variables and keeps the growth linear.

What comes out is a working solver that takes real DIMACS instances and returns an answer, and along the way translates any formula to CNF without blowing up its size. Written in Haskell, because pattern matching and types that guard correctness make the logic read almost like mathematics. A small project that touches a very deep part of computer science - and genuinely solves it.