Для решения проблемы SAT предлагается алгоритм, который вытекает из нестандартного доказательства полноты метода резолюций. В отличие от SAT-солверов, использующих поиск с возвратом, алгоритм исключает переменные по очереди, порождая новые клаузы. Все клаузы хранятся в структуре данных, в которой никакая клауза не является частью другой клаузы. На основании результатов тестирования выдвинуто предположение о небольшом объеме этой структуры данных, что определяет теоретическую оценку времени выполнения алгоритма.
Проблема выполнимости КНФ
В булевой алгебре хорошо известно понятие конъюнктивной нормальной формы булевой формулы (КНФ).
КНФ – это конъюнкция элементарных дизъюнкций.
Элементарная дизъюнкция (клауза) – это дизъюнкция булевых переменных и их отрицаний.
Выполнимость булевой формулы означает существование набора значений переменных, на котором формула принимает значение 1.
Метод резолюций
Рассмотрим пример КНФ:
Перечислим клаузы: сначала содержащие переменную 
, затем содержащие отрицание переменной 
, а затем не содержащие 
:
Клаузы без переменной 
просто перепишем. А клаузы с 
попарно соединим (по правилу резолюции) с клаузами с 
. То есть преобразуем конъюнкцию:
Справедлива теорема:
Пусть 
- формулы, не содержащие переменной 
, причем формула 
выполнима. Тогда формула 
также выполнима.
Доказательство. Если
на некотором наборе значений переменных, то присвоим 
. Если 
на некотором наборе значений переменных, присвоим 
.
Из теоремы вытекает, что, если мы перейдем от формулы 
к формуле 
, то невыполнимость формулы сохранится.
Таким образом, исключив переменную 
, мы пришли к таким клаузам:
Повторяя ту же процедуру для переменной 
, получаем клаузы:
Это противоречие. Значит, исходная КНФ невыполнима.
Алгоритм решения SAT
Перечисляем и исключаем все переменные по очереди. Храним текущее множество клауз. В этом множестве выделяем три подмножества: 
, 
, 
.
В структуре данных на следующем шаге останутся элементы множества 
. Перечисляем элементы декартова произведения 
, находим резольвенту и пробуем добавить её в структуру данных. Если резольвента является частью клауз из структуры данных, то все они удаляются, а резольвента добавляется в структуру. Если какая-нибудь клауза является частью резольвенты или совпадает с ней, то резольвента не добавляется в структуру.
По сравнению с SAT-солверами, использующими поиск с возвратом, предложенный алгоритм накапливает клаузы в едином множестве, исключая поглощения клаузами друг друга. Интерес представляет максимальный объем этого множества в ходе выполнения алгоритма. Этот объем определяет сложность алгоритма, поскольку время выполнения полиномиально зависит от этого объема.
Тестирование алгоритма
Пробная реализация алгоритма доступна на GitHub. Текущая версия не находит значения переменных, при которых КНФ принимает значение 1, а только определяет выполнимость.
В качестве тестов были взяты задачи раскрашивания графов (выполнимые КНФ) и задачи pigeonhole (невыполнимые КНФ) с ресурса SATLIB.
Результаты для раскрашивания графов:
Тест | Объем структуры данных | Время решения |
flat-30-1.cnf (90 переменных, 300 клауз) | 867 клауз | 4 сек. |
flat-50-1.cnf (150 переменных, 545 клауз) | 10574 клауз | 3939 сек. |
flat-75-1.cnf (225 переменных, 840 клауз) | >40000 клауз | - |
Результаты для pigeonhole:
Тест | Объем структуры данных | Время решения |
hole6.cnf (42 переменные, 133 клауз) | 3055 клауз | 63 сек. |
hole7.cnf (56 переменных, 204 клауз) | >26000 клауз | - |
Выводы
Несмотря на большой объем вычислений (за счет наивной реализации структуры данных), объем структуры данных оказался небольшим. Именно объем множества клауз определяет сложность алгоритма. Для ускорения алгоритма следует ускорить поиск клауз в множестве, добавление новых клауз в множество и удаление клауз из множества.
