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

Число >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. До середины итераций число дизъюнктов растет, дальше уменьшается.

Comments 6

bocovp yesterday at 05:23

Это же алгоритм Дэвиса — Патнема (DP; не путать с DPLL), один из первых алгоритмов решения задачи о выполнимости...

lapkin25 23 hours ago

Спасибо за полезный ответ! Действительно, алгоритм очень похож на DP, но вместо эвристик "Unit-literal rule" и "Pure-literal rule" поддерживается структура данных, сразу исключающая все возможные поглощения клауз. За счет этого количество клауз в множестве становится меньше.

domix32 16 hours ago

клауза

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

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

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

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

86000

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

domix32 10 hours ago

то есть это кумулятивное значений со всех шагов итерации? Или это именно вводное количество выражений?

lapkin25 6 hours ago

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