Алгоритмы расщепления и числа Ван-дер-Вардена
Привет, Хабр! Решил побаловаться графоманством и поделиться результатом развлечения прошедших выходных (только эти выходные прошли давно и статья писалась гораздо дольше, чем развлечение. Как говорится, делу время — потехе час).Я расскажу про так называемые алгоритмы расщепления (в частности, про DPLL-алгоритм), про теорему и числа Ван-дер-Вардена, а в заключение статьи мы напишем свой собственный алгоритм расщепления и за полчаса вычислений докажем, что число w (2; 5) равно 178 (первооткрывателям в 1978 году на это потребовалось более 8 дней вычислений).
Алгоритм расщепленияЭто достаточно общий алгоритм, который решает следующую задачу: есть некоторое конечное множество S и мы хотим разделить его на два подмножества A и B, обладающими некоторыми свойствами, или же определить, что нужным способом множество S разделить нельзя.Делается это следующим образом: заводятся и на каждом шаге поддерживаются 3 не пересекающихся подмножества A, B, C, которые полностью покрывают множество S, где C — это множество тех элементов, которые мы еще не распределили между A и B. Изначально C=S, а A и B пусты. На каждой итерации в множестве C произвольно выбирается элемент a, который можно поместить либо в множество A, либо в множество B. На самом деле, мы делаем и то, и другое, а затем рекурсивно обрабатываем оба возможных варианта.
В итоге получается дерево расщепления, в листьях которого находятся всевозможные разделения множества S на A и B, а множество C пусто. Теперь нам нужно просто для всех листьев проверить выполнение интересующих нас свойств.
«Позвольте!», — скажете вы, — «чем это лучше очевидного перебора из 2|S| вариантов?». А все дело в отсечениях, которые весьма удобно добавлять к предложенному выше костяку алгоритма!
Список отсечений:
Если частично построенные A и B не подходят — откат Перемещение элемента из S в A или B может повлечь перемещение других элементов из S в A или B Грамотный выбор элемента a из S на каждом шаге может существенно сократить размер дерева перебора С применением отсечений размер дерева сильно сокращается, число листьев заметно уменьшается, иногда до 0 (это означает, что разделить S на A и B нужным образом нельзя). Хотя сложность алгоритма все равно остается экспоненциальной в худшем случае.Общий алгоритм расщепления и все предложенные отсечения удобно пояснить на примере классического DPLL-алгоритма.
DPLL-алгоритм Алгоритм Дэвиса–Патнема–Логемана–Лавленда (DPLL) был разработан в 1962 году для определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме, т.е. для решения задачи SAT. Алгоритм оказался настолько эффективным, что спустя уже более 50 лет представляет собой основу для большинства эффективных решателей SAT.Давайте разберем подробнее, что же делает алгоритм DPLL. Он берет булеву формулу и пытается разделить все переменные, входящие в нее, на два множества A и B, где A — множество всех переменных со значением true, а B — множество всех переменных со значением false.
На каждом шаге некоторым образом выбирается переменная, которой еще не присвоено значение (назовем такие переменные свободными) и присваивается значение true (эта переменная заносится в множество A). После этого решается полученная упрощенная задача. Если она выполнима, то и исходная формула выполнима. Иначе — выбранной переменной присваивается значение false (она заносится в B) и задача решается для новой упрощенной формулы. Если она выполнима, то и исходная формула выполнима. Иначе — увы, исходная формула невыполнима.
После каждого присваивания формула дополнительно упрощается при помощи следующих двух правил:
Распространение переменной (unit propagation). Если в какой-либо дизъюнкте осталась ровно одна переменная, то ей необходимо присвоить такое значение, чтобы дизъюнкта в итоге стала истинной (переместить в A или B в зависимости от того, есть отрицание или нет). Исключение «чистых» переменных (pure literal elimination). Если какая-либо переменная входит в формулу только с отрицаниями, либо всегда без отрицаний — она называется чистой. Этой переменной можно присвоить такое значение, что все ее вхождения будут иметь значение true, что уменьшит число свободных переменных. Данные два правила следует применять до тех пор, пока они применяются: обычно после первого присваивания следует целый каскад упрощений, что хорошо уменьшает число свободных переменных.Если после упрощения мы получили пустую дизъюнкту (все ее простые конъюнкты ложны) — текущая формула не выполнима и следует откатиться. Если же свободных переменных не осталось — то формула выполнима и работу алгоритма можно закончить. Также закончить работу алгоритма можно в том случае, если дизъюнкт не осталось — неиспользованные свободные переменные можно назначить произвольным образом.
Небольшой C-подобный псевдокод, поясняющий что происходит:
bool DPLL (eq F, set A, set B, set C) { while (1) { // проверка на допустимость if (F is empty) { // формула допустима! write A, B, C; return true; } if (F contains an empty clause) return false; // формула не допустима // упрощения bool flag = false; if (unit_propagation (&F, &A, &B, &C)) flag = true; if (pure_literal_elimination (&F, &A, &B, &C)) flag = true; if (! flag) break; // упрощений не произошло } // ветвление x = choose_literal (F, С); if (DPLL (F ∧ (x), A^x, B, C^x)) return true; if (DPLL (F ∧ (¬x), A, B^x, C^x)) return true; return false; } Символом & показано, что в функции unit_propagation и pure_literal_elimination переменные F, A, B и C передаются по ссылке, т.е. они могут меняться внутри. Если что-нибудь изменилось, данные функции возвращают true. При рекурсивном спуске — напротив, создаются копии объектов. Значок ^ исключает объект из множества, если он есть или добавляет, если его нет.
Рассмотрим следующую формулу и на ее примере посмотрим как работает DPLL-алгоритм:
К этой формуле не применимы правила упрощения, поэтому придется ветвить наше дерево. В качестве элемента для ветвления возьмем x1 и, для начала, присвоим ему значение true. Получим следующую цепочку упрощений: 
Двойные стрелочки показывают, что мы используем первое правило, а именно — находим одинокую переменную и присваиваем ей нужное значение.К сожалению, данная ветвь ведет к невыполнимой формуле, т.е. в этой ветви мы зря старались. Откатываемся и пробуем присвоить переменной x1 значение false. Это приведет к следующей цепочке упрощений:
Тройные стрелки показывают, что мы применяем второе правило упрощения. В этой ветви нас ждет успех — найдено целых 2 решения! Дерево обхода целиком:
Поскольку преобразования, показанные двойными и тройными стрелками, происходят внутри каждой вершины дерева, получается, что само дерево фактически состоит всего из трех вершин! Впрочем, вероятно, можно было придумать более заковыристый пример.Заметим, что если бы в самом начале для ветвления был выбран, например, элемент x2, то искомое дерево получилось бы гораздо меньше и ответ был бы найден гораздо раньше (необходимые выкладки предлагается сделать читателю самостоятельно). Поэтому стратегия выбора элемента для ветвления очень важна. Например, можно выбирать для ветвления переменную, которая входит в наибольшее число дизъюнктов.
Стоит также отметить, что с помощью данного алгоритма нельзя найти все решения — этому мешает эвристика исключения «чистых» переменных. Вполне может оказаться пропущено решение, в котором значение той переменной, которую мы, следуя эвристике, установили в true, равно false. Для поиска всех решений нужно исключить второе правило из алгоритма.
Теорема и числа Ван дер Вардена Теорема Ван дер Вардера является одним из важнейших результатов в теории Рамсея — раздела математики, изучающем появление закономерностей с объектах, состоящих из большого числа случайных элементов. А начиналось все так: В двадцатых годах прошлого века один математик столкнулся со следующей задачей:
Пусть множество всех натуральных чисел покрашено в 2 различных цвета. Можно ли утверждать, что найдется сколько угодно длинная арифметическая прогрессия, числа которой покрашены в один и тот же цвет?
Задача кажется очень простой и положительное решение представляется почти очевидным. Однако, попытки доказать это утверждение поначалу ни к чему не приводили. Спустя несколько лет задача наконец поддалась молодому голландскому математику Бартелю Леендерту Ван дер Вардену. Он доказал более общий вариант в немного другой формулировке:
Для любых r и k найдется такое число n (r; k), что при любом раскрашивании множества натуральных чисел S={ 1, 2, …, n (r; k) } в r различных цветов данное множество S будет содержать арифметическую прогрессию из чисел, покрашенных в один и тот же цвет.
Доказательство базируется на так называемой двойной индукции. С упрощенной версией этого доказательства можно ознакомиться, например, здесь.
Минимальное из чисел n (r; k) обозначим за w (r; k). Числа w (r; k) принято называть числами Ван дер Вардена. Доказательство теоремы Ван дер Вардена не дает точных значений чисел w (r; k), только верхнюю границу. И поверьте, эта верхняя граница просто огромна! Оказалось, что даже для двух цветов оценка на число w (r; k) растет как функция Аккермана! Эта оценка сверху постепенно улучшалась. Последний результат, полученный Тимоти Гауэрсом в 2001 году, гласит:
w (r; k) ≤ 22r22k+9.
Результат чуть менее страшный, чем первоначальный, но все равно немного пугающий. И все равно эта граница очень далека от точных значений w (r; k).
Отдельная ветвь исследований — определение точных значений чисел w (r; k) для различных r и k. Эта задача весьма ресурсозатратна (это свойственно большинству задач Теории Рамсея). Википедия говорит, что на данный момент точное значение w (r; k) известно только для 7 пар чисел r и k.
r / k 3 4 5 6 2 цвета 9 35 178 1132 3 цвета 27 293 4 цвета 76 Тривиально получается ответ для w (2; 3): Доказательство того, что w (2; 3)=9 Другое доказательство с аналогичной идеей и в чуть более развернутом виде приведено здесь.Пример покраски 8 чисел в 2 цвета так, что среди нет одноцветной арифметической прогрессии длины 3 выглядит так:
1 2 3 4 5 6 7 8
Это означает, что w (2;3)>8. Для 9 же цветов давайте рассмотрим числа 4 и 6. Без ограничения общности, возможны два случая: либо эти два числа покрашены в один цвет, либо в разные.
1) Пусть 4 и 6 покрашены в красный цвет:
1 2 3 4 5 6 7 8 9
Тогда мы обязаны покрасить 5 в синий цвет, поскольку иначе образуется тройка красных чисел 4 5 6. Аналогичные рассуждения для 2 и 8. В итоге получаем синюю тройку 2 5 8:
1 2 3 4 5 6 7 8 9
2) Пусть 4 синяя, а 6 красная:
1 2 3 4 5 6 7 8 9
Тогда, без ограничения общности, 5 можно покрасить в синий цвет. Из этого следует, что 3 следует покрасить в красный цвет, чтобы избежать синих 3 4 5. Далее, 9 следует покрасить в синий, чтобы избежать красных 3 6 9. Промежуточный итог:
1 2 3 4 5 6 7 8 9
Число 1 должно быть красным, чтобы избежать синих 1 5 9. Из этого следует синяя 2, поскольку иначе получим красные 1 2 3. Чтобы избежать красных 2 5 8, красим 8 в красный цвет и в итоге получаем:
1 2 3 4 5 6 7 8 9
Теперь, если мы покрасим 7 в красный цвет, то получим красную тройку 6 7 8. Если же 7 покрасить в синий цвет, то выйдет синяя тройка 5 7 9.
Для чуть больших значений w (r, k) доказательство обычно сводится к следующему: фиксируется длина раскрашиваемой цепочки чисел n, после чего строится булева формула в конъюнктивной нормальной форме для проверки того, что эти n чисел можно раскрасить с учетом ограничений r и k, и проверяется ее выполнимость с помощью SAT-солвера. Если решение нашлось, то число n+1 — нижняя граница для w (r; k), иначе — число n следует считать верхней границей для w (r; k).
Учитывая, что многие SAT-солверы построены на основе DPLL-алгоритма, числа w (r; k) ищутся с использованием алгоритмов расщепления.
Приведем простой способ построения нужной булевой формулы для количества цветов r=2. Заведем n переменных xi, означающих, в какой цвет покрашены соответствующие числа. Значение true будет означать 1й цвет, false — второй. Нам нужно ввести ограничения на то, чтобы любая арифметическая прогрессия содержала оба цвета. Делается это очень просто: дизъюнкция вида (xa1∨xa2∨…∨xak) гарантирует присутствие первого цвета, а дизъюнкция вида (¬xa1∨¬xa2∨…∨¬xak) — второго. Ну и, собственно, все — для каждой арифметической прогрессии строим 2 формулы и склеиваем все, что получилось, в одну большую КНФ.
Пример формулы для r=2, k=3 и n=9:
(x1∨x2∨x3) ∧ (¬x1∨¬x2∨¬x3) ∧ (x2∨x3∨x4) ∧ (¬x2∨¬x3∨¬x4) ∧ (x3∨x4∨x5) ∧ (¬x3∨¬x4∨¬x5) ∧(x4∨x5∨x6) ∧ (¬x4∨¬x5∨¬x6) ∧ (x5∨x6∨x7) ∧ (¬x5∨¬x6∨¬x7) ∧ (x6∨x7∨x8) ∧ (¬x6∨¬x7∨¬x8) ∧(x7∨x8∨x9) ∧ (¬x7∨¬x8∨¬x9) ∧ (x1∨x3∨x5) ∧ (¬x1∨¬x3∨¬x5) ∧ (x2∨x4∨x6) ∧ (¬x2∨¬x4∨¬x6) ∧(x3∨x5∨x7) ∧ (¬x3∨¬x5∨¬x7) ∧ (x4∨x6∨x8) ∧ (¬x4∨¬x6∨¬x8) ∧ (x5∨x7∨x9) ∧ (¬x5∨¬x7∨¬x9) ∧(x1∨x4∨x7) ∧ (¬x1∨¬x4∨¬x7) ∧ (x2∨x5∨x8) ∧ (¬x2∨¬x5∨¬x8) ∧ (x3∨x6∨x9) ∧ (¬x3∨¬x6∨¬x9) ∧(x1∨x5∨x9) ∧ (¬x1∨¬x5∨¬x9)
В предыдушем спойлере доказано, что эта формула невыполнима.
Применяем знания на практике
Давайте теперь напишем свой собственный алгоритм расщепления для поиска чисел w (2; k), не использующий всякой мишуры вроде SAT-солвера. Писать будем на C++ (я использую MS Visual Studio). Основа алгоритма выглядит следующим образом:
#pragma comment (linker,»/STACK:64000000»)
#include
using namespace std;
#define N 178 #define K 5
#define BSET bitset< N >
bool dfs (BSET & A, BSET & B)
{
int i = choice (A, B);
if (i<0)
{
for (int a=0; a A[i] = true;
if (check (A, B))
{
BSET A1 = A, B1 = B;
if (reduce (A1, B1))
if (dfs (A1, B1))
return true;
}
A[i] = false; B[i] = true;
if (check (A, B))
{
BSET A1 = A, B1 = B;
if (reduce (A1, B1))
if (dfs (A1, B1))
return true;
}
B[i] = false;
return false;
} int main ()
{
freopen («input.txt», «r», stdin);
freopen («output.txt», «w», stdout); BSET A, B;
if (! dfs (A, B)) cout << "No counterexamples\n";
cout << "n=" << N << " k=" << K << "\n";
cout << "time=" << clock() << "\n"; return 0;
}
Процедура dfs, собсвенно, и является костяком алгоритма. Константы N и K (длина последовательности и длина арифметической прогрессии соответственно) будут вставляться в код препроцессором в виде чисел, иногда это помогает компилятору лучше оптимизироать код. Множества A и B (элементы последовательности, покрашенные в первый и во второй цвет соответсвенно) задаются битовой маской длины N. Теперь на предложенный костяк следует навесить функцииchoice — выбор элемента, по которому мы будем ветвить наше дерево.
check — проверка того, что в последовательности нет арифметической прогрессии длины K.
reduce — покраска дополнительных элементов, для которых цвет можно определить однозначно.
Функция choice — одна из самых интересных:
int cost[N]; int choice (BSET & A, BSET & B)
{
memset (cost, 0, sizeof (cost));
for (int a=0; a if (cnt1==0 || cnt2==0)
for (int c=0; c int mx = 0;
for (int a=0; a if (mx > 0)
for (int a=0; a return -1;
}
Стратегия выбора элемента, заложенная в choice, следующая: выбирается тот элемент, который входит в наибольшее число потенциальных одноцветных арифметических прогрессий. Но и это еще не все: чем больше в потенциальной прогрессии покрашенных чисел, тем больший вклад она вносит в оценку. Как правило, в алгоритмах расщепления всегда нужно выбирать тот элемент, который делает все как можно хуже и быстрее приводит к конфликту (когда функция check возвращает false). Такая стратегия чаще отсекает ненужные ветви, уменьшая пространство вариантов.Теперь рассмотрим процедуру check:
bool check (BSET & A, BSET & B)
{
for (int a=0; a
bool reduce (BSET & A, BSET & B)
{
while (1)
{
bool flag = false;
for (int a=0; a A и B — цвета. Вопросик означает, что нам не важно, какой именно цвет в данной позиции. Т.е., на самом деле, мы нашли аж 32 примера длины 177, в которых нет одноцветной арифметической прогрессии длины 5. На параметрах N=178 K=5 код проработал 20,5 минут и показал, что искомых арифметических прогрессий нет. Неплохо для 2178 вариантов в общем случае. Данный код можно бесконечно оптимизировать — подобрать нужные структуры данных для быстрого выполнения choice, check и reduce, поискать более оптимальную стратегию выбора элемента для ветвления, ну или хотя бы красить самый первый выбранный элемент только в один цвет. Но это уже выходит за рамки данной статьи. Конечно же, код работает и для вычисления w (2; 3) и w (2; 4) (на них все это дело тестировалось изначально). Что можно сказать насчет случая K=6? Совсем недавно (в 2008 году) было доказано, что w (2; 6)=1132 и на это ушло около 250 дней вычислений на кластере из 200 ядер. Кстати, реализация их алгоритма доказывает, что w (2; 5)=178, менее чем за 3 секунды на одном ядре. Для случая K=7 вопрос остается открытым. Почитать
Алгоритмы расщепления на Лекториуме (видео, слайды лекции)
Алгоритм Брона-Кербоша поиска всех клик в графе (по сути алгоритм расщепления)
DPLL-алгоритм на Википедии (рус, eng)
Теорема и числа Ван дер Вардена (eng)
А.Я. Хинчин. Три жемчужины теории чисел
Библейский код, теория Рэмзи и существование Бога
Рональд Л. Грэм, Джоуэл X. Спенсер. Теория Рамсея
R.S. Stevens, R. Shantaram. Computer-Generated van der Waerden Partitions (eng, pdf)
Michal Kouril, Jerome L. Paul. The van der Waerden Number W (2,6) Is 1132 (eng, pdf)
P.S. Не по всем ссылкам с глубоко вчитывался, поэтому если какая ссылка на самом деле не по теме — уберу.
