sift

sift - это SAT-солвер на основе алгоритма DPLL, написанный на Haskell, вместе с набором инструментов пропозициональной логики: парсером формата DIMACS и переводом формул в форму CNF методом Цейтина. Это не упражнение на бумаге - он решает реальные экземпляры.

SAT - одна из тех задач, что соединяют кажущуюся простоту с огромной глубиной. Вопрос звучит невинно, а ответ на него способен решать задачи из совершенно иных областей. Этот проект касается именно этого ядра, и со стороны, которая заставляет понять, почему солвер вообще работает.

SAT спрашивает вещь на вид банальную: можно ли подобрать логические значения так, чтобы вся формула была истинной? Банально до момента, когда переменных сотни, а от ответа зависят планирование, верификация схем или решение головоломки. SAT-солвер сидит под многими трудными задачами, которые сначала переводят на его язык.

Стандартный вход - формат DIMACS - каждая строка это дизъюнкт, числа это переменные, минус это отрицание, ноль завершает дизъюнкт. Простой текст, который умеет кодировать удивительно трудные вопросы.

DPLL - это умный поиск с возвратом. Вместо того чтобы перебирать все комбинации, на каждом шаге он выбирает переменную, задаёт ей значение и следит за двумя сокращениями: если у дизъюнкта только один неразрешённый литерал, его значение вынуждено; если переменная всегда встречается в одной и той же форме, её можно сразу задать.

Именно эти два сокращения делают разницу между секундой и вечностью. Без них солвер блуждает по дереву всех возможностей; с ними целые поддеревья отпадают, ещё не будучи посещёнными. Правильно их реализовать - сердце всего солвера.

DPLL требует формулу в форме CNF, но не всякая формула уже такова. Наивное преобразование способно раздуть её размер экспоненциально, превращая маленькую задачу в гигантскую ещё до старта солвера. Метод Цейтина вводит вспомогательные переменные и удерживает рост линейным.

На выходе - работающий солвер, который берёт реальные экземпляры в формате DIMACS и возвращает ответ, а по дороге переводит любую формулу в CNF, не раздувая её размер. Написан на Haskell, потому что сопоставление с образцом и типы, стерегущие правильность, делают так, что логика читается почти как математика. Маленький проект, который касается очень глубокой части информатики - и по-настоящему её решает.