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

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

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

18.08.2026 04:49

lapkin25 6 6500 Источник

Для решения проблемы 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 клауз)	>86000 клауз	-

Результаты для pigeonhole:

Тест	Объем структуры данных	Время решения
hole6.cnf (42 переменные, 133 клауз)	3055 клауз	63 сек.
hole7.cnf (56 переменных, 204 клауз)	28434 клауз	14218 сек.

Выводы

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

Комментарии (6)

bocovp
18.08.2026 05:23
#30341702
Это же алгоритм Дэвиса — Патнема (DP; не путать с DPLL), один из первых алгоритмов решения задачи о выполнимости...
1. lapkin25 Автор
  18.08.2026 05:23
  #30341736
  Спасибо за полезный ответ! Действительно, алгоритм очень похож на DP, но вместо эвристик "Unit-literal rule" и "Pure-literal rule" поддерживается структура данных, сразу исключающая все возможные поглощения клауз. За счет этого количество клауз в множестве становится меньше.

domix32

18.08.2026 05:23

#30343436

клауза

Выражение же. Ну или условие на крайний случай.

Элементарная дизъюнкция (клауза)

в этом месте не очень понял зачем вообще ремарка про выражения. конъюнкция тоже будет выражением. Просто ваш способ разбивает их на простые дизъюнкции. Ну и для конъюнкици тоже есть символ $\land$ .

Не хватает примера работы вашего солвера хотя бы на сгенерированных данных.

86000

не очень понял откуда такие большие цифры. по ссылке таблица устверждает что тех выражений там чуть больше 2к.

lapkin25 Автор

18.08.2026 05:23

#30344476

Число >86000 клауз - это сколько дизъюнктов в структуре данных. В самом тесте 840 дизъюнктов от 225 переменных. Дальше метод резолюций выводит новые дизъюнкты, исключая переменные и пополняя базу дизъюнктов. Одни дизъюнкты (с очередной переменной) удаляются, а их попарные резольвенты добавляются.

В качестве примера работы могу только привести, сколько дизъюнктов в базе на каждой итерации.

Лог вывода

hole7.cnf

1 of 56
204 clauses
Counter({2: 196, 7: 8})
pos 1; neg 7
2 of 56
203 clauses
Counter({2: 189, 7: 14})
pos 1; neg 7
3 of 56
202 clauses
Counter({2: 183, 7: 18, 12: 1})
pos 1; neg 7
4 of 56
201 clauses
Counter({2: 178, 7: 20, 12: 3})
pos 1; neg 7
5 of 56
200 clauses
Counter({2: 174, 7: 20, 12: 6})
pos 1; neg 7
6 of 56
199 clauses
Counter({2: 171, 7: 18, 12: 10})
pos 1; neg 7
7 of 56
198 clauses
Counter({2: 169, 12: 15, 7: 14})
pos 1; neg 7
8 of 56
197 clauses
Counter({2: 168, 12: 21, 7: 8})
pos 1; neg 7
9 of 56
196 clauses
Counter({2: 168, 12: 28})
pos 7; neg 7
10 of 56
224 clauses
Counter({2: 161, 12: 63})
pos 12; neg 7
11 of 56
277 clauses
Counter({2: 154, 12: 123})
pos 17; neg 7
12 of 56
355 clauses
Counter({12: 208, 2: 147})
pos 22; neg 7
13 of 56
458 clauses
Counter({12: 318, 2: 140})
pos 27; neg 7
14 of 56
586 clauses
Counter({12: 453, 2: 133})
pos 32; neg 7
15 of 56
739 clauses
Counter({12: 613, 2: 126})
pos 37; neg 37
16 of 56
852 clauses
Counter({12: 700, 2: 120, 16: 26, 11: 6})
pos 41; neg 41
17 of 56
979 clauses
Counter({12: 796, 2: 114, 16: 56, 11: 12, 20: 1})
pos 209; neg 40
18 of 56
1725 clauses
Counter({12: 1293, 16: 223, 2: 108, 11: 66, 20: 24, 15: 10, 24: 1})
pos 323; neg 63
19 of 56
2789 clauses
Counter({12: 1751, 16: 514, 11: 216, 2: 102, 20: 99, 15: 80, 24: 14, 19: 12, 28: 1})
pos 508; neg 101
20 of 56
4469 clauses
Counter({12: 2570, 16: 869, 11: 366, 15: 240, 20: 201, 2: 96, 19: 72, 24: 36, 23: 12, 28: 6, 32: 1})
pos 771; neg 147
21 of 56
7004 clauses
Counter({12: 3750, 16: 1576, 11: 516, 15: 400, 20: 366, 19: 180, 2: 90, 24: 60, 23: 48, 27: 10, 28: 7, 36: 1})
pos 1073; neg 376
22 of 56
9606 clauses
Counter({12: 4690, 16: 2428, 20: 663, 11: 655, 15: 556, 19: 285, 24: 110, 23: 94, 2: 85, 27: 19, 28: 10, 31: 10, 35: 1})
pos 1254; neg 1031
23 of 56
11846 clauses
Counter({12: 5001, 16: 3040, 15: 912, 20: 909, 11: 830, 19: 618, 23: 284, 24: 88, 2: 80, 26: 41, 27: 24, 30: 10, 28: 4, 31: 4, 34: 1})
pos 1484; neg 1515
24 of 56
13395 clauses
Counter({12: 4864, 16: 3312, 15: 1377, 19: 1173, 11: 1070, 20: 804, 23: 338, 22: 115, 2: 75, 18: 70, 24: 57, 26: 53, 14: 48, 27: 21, 30: 12, 29: 5, 33: 1})
pos 1678; neg 1782
25 of 56
14897 clauses
Counter({12: 4832, 16: 3456, 15: 1848, 19: 1640, 11: 1280, 20: 688, 23: 390, 22: 270, 18: 194, 26: 100, 14: 96, 2: 70, 29: 20, 21: 10, 25: 2, 32: 1})
pos 4962; neg 1527
26 of 56
19793 clauses
Counter({15: 4497, 12: 4352, 11: 2936, 16: 2565, 19: 1844, 18: 1564, 22: 629, 14: 504, 21: 278, 20: 272, 25: 129, 23: 106, 2: 65, 26: 20, 28: 20, 24: 8, 29: 3, 31: 1})
pos 6295; neg 2010
27 of 56
25784 clauses
Counter({15: 6282, 11: 5040, 12: 4096, 18: 3040, 14: 1872, 16: 1863, 19: 1292, 21: 930, 17: 522, 22: 352, 24: 208, 20: 137, 2: 60, 25: 40, 27: 24, 23: 19, 28: 6, 30: 1})
pos 7620; neg 3701
28 of 56
26857 clauses
Counter({15: 5070, 12: 4224, 11: 4072, 14: 3480, 18: 2830, 16: 1989, 17: 1329, 19: 855, 21: 809, 13: 640, 10: 640, 20: 416, 24: 137, 22: 136, 23: 130, 2: 56, 26: 20, 25: 14, 27: 9, 29: 1})
pos 7428; neg 4139
29 of 56
28077 clauses
Counter({14: 5344, 11: 4836, 15: 4125, 12: 3264, 17: 2753, 18: 2165, 16: 1585, 13: 984, 10: 816, 20: 731, 19: 603, 21: 476, 23: 156, 22: 103, 24: 55, 2: 52, 25: 16, 26: 12, 28: 1})
pos 7475; neg 4607
30 of 56
28434 clauses
Counter({11: 5560, 14: 5142, 15: 4062, 17: 3129, 12: 2304, 13: 2106, 16: 1807, 18: 1326, 10: 944, 20: 876, 19: 676, 22: 213, 21: 131, 23: 82, 2: 48, 25: 15, 24: 12, 27: 1})
pos 8041; neg 4659
31 of 56
27573 clauses
Counter({11: 5424, 14: 5130, 15: 3473, 17: 3143, 13: 3080, 16: 1978, 12: 1728, 19: 1225, 10: 1144, 18: 485, 20: 334, 21: 194, 22: 164, 2: 44, 24: 18, 23: 8, 26: 1})
pos 7927; neg 4691
32 of 56
26553 clauses
Counter({11: 6183, 14: 5628, 13: 3720, 16: 3610, 15: 1865, 17: 1536, 10: 1104, 18: 916, 19: 907, 12: 648, 21: 273, 20: 97, 2: 40, 23: 21, 22: 4, 25: 1})
pos 10187; neg 3924
33 of 56
28075 clauses
Counter({11: 6372, 13: 5568, 14: 3979, 15: 3179, 16: 2511, 10: 1872, 17: 1430, 12: 1323, 18: 978, 19: 335, 20: 220, 9: 192, 21: 59, 2: 36, 22: 18, 23: 2, 24: 1})
pos 6818; neg 6221
34 of 56
23835 clauses
Counter({13: 5638, 11: 4347, 15: 3529, 14: 2656, 10: 2040, 12: 1593, 16: 1548, 17: 1441, 18: 490, 19: 288, 9: 144, 20: 64, 2: 33, 21: 21, 22: 2, 23: 1})
pos 8337; neg 4737
35 of 56
21227 clauses
Counter({13: 5747, 11: 3996, 15: 3324, 10: 2334, 14: 1740, 12: 1492, 17: 1056, 16: 978, 18: 247, 8: 144, 19: 112, 2: 30, 20: 22, 21: 4, 22: 1})
pos 7527; neg 4164
36 of 56
18622 clauses
Counter({13: 3717, 11: 3332, 12: 2964, 14: 2756, 10: 1744, 15: 1698, 16: 1145, 9: 540, 17: 414, 18: 141, 8: 108, 19: 29, 2: 27, 20: 6, 21: 1})
pos 6132; neg 3936
37 of 56
15724 clauses
Counter({12: 3608, 11: 2822, 14: 2596, 13: 2360, 10: 1516, 15: 1100, 9: 648, 16: 634, 8: 189, 17: 178, 18: 40, 2: 24, 19: 8, 20: 1})
pos 5428; neg 3407
38 of 56
13383 clauses
Counter({12: 2972, 11: 2682, 13: 2426, 10: 1908, 14: 1568, 15: 814, 9: 504, 16: 254, 8: 162, 17: 61, 2: 21, 18: 10, 19: 1})
pos 4355; neg 3419
39 of 56
10272 clauses
Counter({12: 2506, 11: 2292, 13: 1856, 10: 1476, 14: 933, 9: 636, 15: 348, 8: 108, 16: 85, 2: 19, 17: 12, 18: 1})
pos 3112; neg 2910
40 of 56
7568 clauses
Counter({11: 2127, 12: 1860, 13: 1181, 10: 1150, 9: 528, 14: 502, 15: 116, 8: 72, 2: 17, 16: 14, 17: 1})
pos 1927; neg 2445
41 of 56
5251 clauses
Counter({12: 1576, 11: 1522, 10: 800, 13: 716, 9: 404, 14: 153, 8: 48, 15: 16, 2: 15, 16: 1})
pos 2426; neg 1085
42 of 56
4502 clauses
Counter({11: 1437, 10: 1157, 12: 940, 9: 551, 13: 262, 8: 108, 14: 33, 2: 12, 15: 2})
pos 1857; neg 1203
43 of 56
3395 clauses
Counter({10: 1142, 11: 982, 9: 640, 12: 390, 8: 164, 13: 63, 2: 10, 14: 4})
pos 1487; neg 850
44 of 56
2601 clauses
Counter({10: 988, 9: 743, 11: 488, 8: 240, 12: 96, 7: 32, 2: 8, 13: 6})
pos 976; neg 858
45 of 56
1819 clauses
Counter({9: 732, 10: 651, 8: 228, 11: 158, 7: 32, 12: 12, 2: 6})
pos 629; neg 680
46 of 56
1143 clauses
Counter({9: 622, 8: 236, 10: 230, 7: 32, 11: 18, 2: 5})
pos 276; neg 559
47 of 56
584 clauses
Counter({9: 400, 8: 132, 10: 32, 7: 16, 2: 4})
pos 236; neg 237
48 of 56
347 clauses
Counter({8: 264, 9: 72, 7: 8, 2: 3})
pos 72; neg 201
49 of 56
146 clauses
Counter({8: 140, 7: 4, 2: 2})
pos 95; neg 49
50 of 56
97 clauses
Counter({7: 96, 2: 1})
pos 64; neg 33
51 of 56
64 clauses
Counter({6: 64})
pos 32; neg 32
52 of 56
32 clauses
Counter({5: 32})
pos 16; neg 16
53 of 56
16 clauses
Counter({4: 16})
pos 8; neg 8
54 of 56
8 clauses
Counter({3: 8})
pos 4; neg 4
55 of 56
4 clauses
Counter({2: 4})
pos 2; neg 2
56 of 56
2 clauses
Counter({1: 2})
pos 1; neg 1
UNSAT
Время выполнения: 14218 секунд

Здесь Counter(...) - это статистика по длинам дизъюнктов.

pos .., neg ... - это сколько дизъюнктов попарно резольвируется (pos - дизъюнкты с очередной переменной, neg - с отрицанием переменной)

Пример теста - pigeonhole. До середины итераций число дизъюнктов растет, дальше уменьшается.

domix32
18.08.2026 05:23
#30344716
то есть это кумулятивное значений со всех шагов итерации? Или это именно вводное количество выражений?
1. lapkin25 Автор
  18.08.2026 05:23
  #30345036
  В структуру данных дизъюнкты добавляются и удаляются. Число в таблице - это максимальный объем структуры данных, который был в ходе итераций. Например, в логе это 28434.

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

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

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

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

Тестирование алгоритма

Выводы

Комментарии (6)

bocovp

lapkin25 Автор

domix32

lapkin25 Автор

domix32

lapkin25 Автор