DPLL-подобный решатель задачи выполнимости над системой уравнений в АНФ

Описаны SAT-решатель, использующий системы булевых уравнений в алгебраической нормальной форме (АНФ) для внутреннего представления задачи, и особенности реализации типичных для SAT-решателей методик для работы с таким представлением. Приводится сравнение данного решателя с рядом классических SAT-решателей при решении некоторых задач криптоанализа (как, например, атака «guess-and-determine» на потоковый шифр Grain).