Хабр·Russia·Tuesday, August 18, 2026 at 04:49 AM

SAT-солвер на основе метода резолюций

Translate

lapkin255 минут назад

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

Проблема выполнимости КНФ

В булевой алгебре хорошо известно понятие конъюнктивной нормальной формы булевой формулы (КНФ).

КНФ – это конъюнкция элементарных дизъюнкций.

Элементарная дизъюнкция (клауза) – это дизъюнкция булевых переменных и их отрицаний.

Выполнимость булевой формулы означает существование набора значений переменных, на котором формула принимает значение 1.

Метод резолюций

Рассмотрим пример КНФ:

$(\neg x_1 \vee x_2) \,\&\, (\neg x_2 \vee x_3) \,\&\, (\neg x_3 \vee \neg x_1) \,\&\, x_1$

Перечислим клаузы: сначала содержащие переменную , затем содержащие отрицание переменной $\neg x_1$ , а затем не содержащие :

$\neg x_1 \vee x_2$

$\neg x_3 \vee \neg x_1$

$\neg x_2 \vee x_3$

Клаузы без переменной просто перепишем. А клаузы с попарно соединим (по правилу резолюции) с клаузами с $\neg x_1$ . То есть преобразуем конъюнкцию:

$x_1 \,\&\, (\neg x_1 \vee x_2) \,\&\, (\neg x_3 \vee \neg x_1) =$ $= (x_1 \vee 0) \,\&\, (\neg x_1 \vee x_2 \,\&\, \neg x_3)$

Справедлива теорема:

Пусть - формулы, не содержащие переменной , причем формула $A \vee B$ выполнима. Тогда формула $(x \vee A) \,\&\, (\neg x \vee B)$ также выполнима.

Доказательство. Если на некотором наборе значений переменных, то присвоим . Если на некотором наборе значений переменных, присвоим .

Из теоремы вытекает, что, если мы перейдем от формулы $(x_1 \vee 0) \,\&\, (\neg x_1 \vee x_2 \,\&\, \neg x_3)$ к формуле $x_2\,\&\, \neg x_3$ , то невыполнимость формулы сохранится.

Таким образом, исключив переменную , мы пришли к таким клаузам:

$\neg x_2 \vee x_3, \; x_2, \; \neg x_3$

Повторяя ту же процедуру для переменной , получаем клаузы:

$\neg x_3, \; x_3$

Это противоречие. Значит, исходная КНФ невыполнима.

Алгоритм решения SAT

Перечисляем и исключаем все переменные по очереди. Храним текущее множество клауз. В этом множестве выделяем три подмножества: $A = \{\text{клаузы, содержащие переменную }x_i\}$ , $B = \{\text{клаузы, содержащие }\neg x_i\}$ , $C = \{\text{клаузы без }x_i\}$ .

В структуре данных на следующем шаге останутся элементы множества . Перечисляем элементы декартова произведения $A \times B$ , находим резольвенту и пробуем добавить её в структуру данных. Если резольвента является частью клауз из структуры данных, то все они удаляются, а резольвента добавляется в структуру. Если какая-нибудь клауза является частью резольвенты или совпадает с ней, то резольвента не добавляется в структуру.

По сравнению с 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 клауз	-

Выводы

Несмотря на большой объем вычислений (за счет наивной реализации структуры данных), объем структуры данных оказался небольшим. Именно объем множества клауз определяет сложность алгоритма. Для ускорения алгоритма следует ускорить поиск клауз в множестве, добавление новых клауз в множество и удаление клауз из множества.

View the original on Хабр →

KioskNews shows a cleaned-up reading view extracted from the publisher’s page — the original always lives on their site, not ours.