Алгоритмы расщепления и числа Ван-дер-Вардена

Привет! Решил побаловаться графоманством и поделиться результатом развлечения прошедших выходных (только эти выходные прошли давно и статья писалась гораздо дольше, чем развлечение. Как говорится, делу время — потехе час).

Я расскажу про так называемые алгоритмы расщепления (в частности, про 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| вариантов?». А все дело в отсечениях, которые весьма удобно добавлять к предложенному выше костяку алгоритма!

Список отсечений:

1. Если частично построенные A и B не подходят — откат
2. Перемещение элемента из S в A или B может повлечь перемещение других элементов из S в A или B
3. Грамотный выбор элемента a из S на каждом шаге может существенно сократить размер дерева перебора

С применением отсечений размер дерева сильно сокращается, число листьев заметно уменьшается, иногда до 0 (это означает, что разделить S на A и B нужным образом нельзя). Хотя сложность алгоритма все равно остается экспоненциальной в худшем случае.

Общий алгоритм расщепления и все предложенные отсечения удобно пояснить на примере классического DPLL-алгоритма.

DPLL-алгоритм

Алгоритм Дэвиса–Патнема–Логемана–Лавленда (DPLL) был разработан в 1962 году для определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме, т.е. для решения задачи SAT. Алгоритм оказался настолько эффективным, что спустя уже более 50 лет представляет собой основу для большинства эффективных решателей SAT.

Давайте разберем подробнее, что же делает алгоритм DPLL. Он берет булеву формулу и пытается разделить все переменные, входящие в нее, на два множества A и B, где A — множество всех переменных со значением true, а B — множество всех переменных со значением false.

На каждом шаге некоторым образом выбирается переменная, которой еще не присвоено значение (назовем такие переменные свободными) и присваивается значение true (эта переменная заносится в множество A). После этого решается полученная упрощенная задача. Если она выполнима, то и исходная формула выполнима. Иначе — выбранной переменной присваивается значение false (она заносится в B) и задача решается для новой упрощенной формулы. Если она выполнима, то и исходная формула выполнима. Иначе — увы, исходная формула невыполнима.

После каждого присваивания формула дополнительно упрощается при помощи следующих двух правил:

1. Распространение переменной (unit propagation). Если в какой-либо дизъюнкте осталась ровно одна переменная, то ей необходимо присвоить такое значение, чтобы дизъюнкта в итоге стала истинной (переместить в A или B в зависимости от того, есть отрицание или нет).
2. Исключение «чистых» переменных (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-алгоритм:

К этой формуле не применимы правила упрощения, поэтому придется ветвить наше дерево. В качестве элемента для ветвления возьмем x₁ и, для начала, присвоим ему значение true. Получим следующую цепочку упрощений:

Двойные стрелочки показывают, что мы используем первое правило, а именно — находим одинокую переменную и присваиваем ей нужное значение.

К сожалению, данная ветвь ведет к невыполнимой формуле, т.е. в этой ветви мы зря старались. Откатываемся и пробуем присвоить переменной x₁ значение false. Это приведет к следующей цепочке упрощений:

Тройные стрелки показывают, что мы применяем второе правило упрощения. В этой ветви нас ждет успех — найдено целых 2 решения!

Дерево обхода целиком:

Поскольку преобразования, показанные двойными и тройными стрелками, происходят внутри каждой вершины дерева, получается, что само дерево фактически состоит всего из трех вершин! Впрочем, вероятно, можно было придумать более заковыристый пример.

Заметим, что если бы в самом начале для ветвления был выбран, например, элемент x₂, то искомое дерево получилось бы гораздо меньше и ответ был бы найден гораздо раньше (необходимые выкладки предлагается сделать читателю самостоятельно). Поэтому стратегия выбора элемента для ветвления очень важна. Например, можно выбирать для ветвления переменную, которая входит в наибольшее число дизъюнктов.

Стоит также отметить, что с помощью данного алгоритма нельзя найти все решения — этому мешает эвристика исключения «чистых» переменных. Вполне может оказаться пропущено решение, в котором значение той переменной, которую мы, следуя эвристике, установили в 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) ≤ 2^2r22k+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(r,k) доказательство обычно сводится к следующему: фиксируется длина раскрашиваемой цепочки чисел n, после чего строится булева формула в конъюнктивной нормальной форме для проверки того, что эти n чисел можно раскрасить с учетом ограничений r и k, и проверяется ее выполнимость с помощью SAT-солвера. Если решение нашлось, то число n+1 — нижняя граница для w(r; k), иначе — число n следует считать верхней границей для w(r; k).

Учитывая, что многие SAT-солверы построены на основе DPLL-алгоритма, числа w(r; k) ищутся с использованием алгоритмов расщепления.

Приведем простой способ построения нужной булевой формулы для количества цветов r=2. Заведем n переменных x_i, означающих, в какой цвет покрашены соответствующие числа. Значение true будет означать 1й цвет, false — второй. Нам нужно ввести ограничения на то, чтобы любая арифметическая прогрессия содержала оба цвета. Делается это очень просто: дизъюнкция вида (x_a1∨x_a2∨…∨x_ak) гарантирует присутствие первого цвета, а дизъюнкция вида (¬x_a1∨¬x_a2∨…∨¬x_ak) — второго. Ну и, собственно, все — для каждой арифметической прогрессии строим 2 формулы и склеиваем все, что получилось, в одну большую КНФ.

Пример формулы для r=2, k=3 и n=9:

(x₁∨x₂∨x₃) ∧ (¬x₁∨¬x₂∨&notx₃) ∧ (x₂∨x₃∨x₄) ∧ (¬x₂∨¬x₃∨&notx₄) ∧ (x₃∨x₄∨x₅) ∧ (¬x₃∨¬x₄∨&notx₅) ∧
(x₄∨x₅∨x₆) ∧ (¬x₄∨¬x₅∨&notx₆) ∧ (x₅∨x₆∨x₇) ∧ (¬x₅∨¬x₆∨&notx₇) ∧ (x₆∨x₇∨x₈) ∧ (¬x₆∨¬x₇∨&notx₈) ∧
(x₇∨x₈∨x₉) ∧ (¬x₇∨¬x₈∨&notx₉) ∧ (x₁∨x₃∨x₅) ∧ (¬x₁∨¬x₃∨&notx₅) ∧ (x₂∨x₄∨x₆) ∧ (¬x₂∨¬x₄∨&notx₆) ∧
(x₃∨x₅∨x₇) ∧ (¬x₃∨¬x₅∨&notx₇) ∧ (x₄∨x₆∨x₈) ∧ (¬x₄∨¬x₆∨&notx₈) ∧ (x₅∨x₇∨x₉) ∧ (¬x₅∨¬x₇∨&notx₉) ∧
(x₁∨x₄∨x₇) ∧ (¬x₁∨¬x₄∨&notx₇) ∧ (x₂∨x₅∨x₈) ∧ (¬x₂∨¬x₅∨&notx₈) ∧ (x₃∨x₆∨x₉) ∧ (¬x₃∨¬x₆∨&notx₉) ∧
(x₁∨x₅∨x₉) ∧ (¬x₁∨¬x₅∨&notx₉)

В предыдушем спойлере доказано, что эта формула невыполнима.

Применяем знания на практике

Давайте теперь напишем свой собственный алгоритм расщепления для поиска чисел w(2; k), не использующий всякой мишуры вроде SAT-солвера. Писать будем на C++ (я использую MS Visual Studio). Основа алгоритма выглядит следующим образом:

#pragma comment(linker,"/STACK:64000000")
#include <iostream>
#include <bitset>
#include <time.h>
#include <memory.h>

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<N; a++)
			if (A[a]) cout << "A";
			else if (B[a]) cout << "B";
			else cout << "?";
		cout << "n";
		return true;
	}

	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 counterexamplesn";
	cout << "n=" << N << " k=" << K << "n";
	cout << "time=" << clock() << "n";

	return 0;
}

Процедура dfs, собсвенно, и является костяком алгоритма. Константы N и K (длина последовательности и длина арифметической прогрессии соответственно) будут вставляться в код препроцессором в виде чисел, иногда это помогает компилятору лучше оптимизироать код. Множества A и B (элементы последовательности, покрашенные в первый и во второй цвет соответсвенно) задаются битовой маской длины N. Теперь на предложенный костяк следует навесить функции

1. choice — выбор элемента, по которому мы будем ветвить наше дерево.
2. check — проверка того, что в последовательности нет арифметической прогрессии длины K.
3. reduce — покраска дополнительных элементов, для которых цвет можно определить однозначно.

Функция choice — одна из самых интересных:

int cost[N];

int choice( BSET & A, BSET & B )
{
	memset( cost, 0, sizeof(cost) );
	for (int a=0; a<N; a++)
		for (int d=1; a+d*(K-1)<N; d++)
		{
			int cnt1=0, cnt2=0;
			for (int c=0; c<K; c++) if (A[a+c*d]) cnt1 ++;
			for (int c=0; c<K; c++) if (B[a+c*d]) cnt2 ++;

			if (cnt1==0 || cnt2==0)
				for (int c=0; c<K; c++)
					if (!A[a+c*d] && !B[a+c*d])
						cost[a+c*d] += cnt1+cnt2+1;
		}

	int mx = 0;
	for (int a=0; a<N; a++) mx = max( mx, cost[a] );

	if (mx > 0)
		for (int a=0; a<N; a++)
			if (cost[a] == mx)
				return a;

	return -1;
}

Стратегия выбора элемента, заложенная в choice, следующая: выбирается тот элемент, который входит в наибольшее число потенциальных одноцветных арифметических прогрессий. Но и это еще не все: чем больше в потенциальной прогрессии покрашенных чисел, тем больший вклад она вносит в оценку. Как правило, в алгоритмах расщепления всегда нужно выбирать тот элемент, который делает все как можно хуже и быстрее приводит к конфликту (когда функция check возвращает false). Такая стратегия чаще отсекает ненужные ветви, уменьшая пространство вариантов.

Теперь рассмотрим процедуру check:

bool check( BSET & A, BSET & B )
{
	for (int a=0; a<N; a++)
		for (int d=1; a+d*(K-1)<N; d++)
		{
			bool f1=true, f2=true;
			for (int c=0; c<K; c++) f1 &= A[a+c*d];
			for (int c=0; c<K; c++) f2 &= B[a+c*d];
			if (f1 || f2) return false;
		}
	return true;
}

Данная процедура маленькая, простая и понятная, поэтому нет смысла на ней останавливаться.

Наконец, процедура reduce:

bool reduce( BSET & A, BSET & B )
{
	while ( 1 )
	{
		bool flag = false;
		for (int a=0; a<N; a++)
			for (int d=1; a+d*(K-1)<N; d++)
			{
				int cnt1=0, cnt2=0;
				for (int c=0; c<K; c++) if (A[a+c*d]) cnt1 ++;
				for (int c=0; c<K; c++) if (B[a+c*d]) cnt2 ++;
				if (cnt1+cnt2<K)
				{
					if (cnt1 == K-1)
						for (int c=0; c<K; c++)
							if (!A[a+c*d])
							{
								B[a+c*d] = true;
								flag = true;
							}
					if (cnt2 == K-1)
						for (int c=0; c<K; c++)
							if (!B[a+c*d])
							{
								A[a+c*d] = true;
								flag = true;
							}
				}
			}
		if (!flag) break;
		if (!check( A, B )) return false;
	}
	return true;
}

Мы просто ищем прогрессии, в которых все элементы кроме одного покрашены в один цвет, а один — не покрашен. Ну и, собственно, красим его в противоположный цвет. Переменная flag хранит в себе — красили мы что-нибудь на текущем проходи или нет. Если нет — выходим, иначе же проверяем на наличие противоречий и если их нет — проходим по всем прогрессиям еще раз.

Результаты

Код тестировался на ноутбуке Core i5 4Gb RAM. При значениях параметров N=177 K=5 за 2 минуты нашелся следующий пример:

BBBABBBBABB?BAAABABBBA?AABAAAABAAAABBBABAAABBBBABBBBABB?BAAABABBBAAAABAAAABAABABBBABAAABA
BBABBBBABBABAAABABBBAAAABAAAABAABABBBABAAABABBABBBBABB?BAAABABBBABAABAAAABAABABBBABAAAB?

A и B — цвета. Вопросик означает, что нам не важно, какой именно цвет в данной позиции. Т.е., на самом деле, мы нашли аж 32 примера длины 177, в которых нет одноцветной арифметической прогрессии длины 5.

На параметрах N=178 K=5 код проработал 20,5 минут и показал, что искомых арифметических прогрессий нет. Неплохо для 2¹⁷⁸ вариантов в общем случае.

Данный код можно бесконечно оптимизировать — подобрать нужные структуры данных для быстрого выполнения 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 вопрос остается открытым.

Почитать

1. Алгоритмы расщепления на Лекториуме (видео, слайды лекции)
2. Алгоритм Брона-Кербоша поиска всех клик в графе (по сути алгоритм расщепления)
3. DPLL-алгоритм на Википедии (рус, eng)
4. Теорема и числа Ван дер Вардена (eng)
5. А. Я. Хинчин. Три жемчужины теории чисел
6. Библейский код, теория Рэмзи и существование Бога
7. Рональд Л. Грэм, Джоуэл X. Спенсер. Теория Рамсея
8. R. S. Stevens, R. Shantaram. Computer-Generated van der Waerden Partitions (eng, pdf)
9. Michal Kouril, Jerome L. Paul. The van der Waerden Number W(2,6) Is 1132 (eng, pdf)

P.S. Не по всем ссылкам с глубоко вчитывался, поэтому если какая ссылка на самом деле не по теме — уберу.

Автор: ripatti

Источник