Вершина переборных алгоритмов.
Вершиной переборных алгоритмов я считаю решение проблемы выполнимости булевой формулы.
Ибо переборный алгоритм по сути своей доказательство теоремы.
Вот здесь находится краткое описание, как работают современные системы.
Интересных вещей там три: обучение конфликтам, периодические перезапуски и ускоренный откат (backjumping, он же откат с учётом конфликта).
Обучение конфликтам уменьшает пространство перебора, причём экспоненциально - и это доказано. Обнаружение конфликтов в назначении переменных происходит всё быстрее и быстрее. Это справедливо для любой переборной задачи.
Периодические перезапуски позволяют избежать перебора в локальном минимуме, так сказать. Они выполняются после некоторого числа конфликтов (которое возрастает после каждого рестарта, гарантируя определение решения, если оно есть) и начинает назначение переменных заново - желательно, в другом порядке.
Ускоренный откат ещё интересней. Для доказательства отсутствия решения нам надо перебрать все возможные варианты назначений переменных. Если у нас проблема всего лишь в одном узком месте, а пространство перебора велико, то мы можем безуспешно перебирать очень долго. По ссылке выше приведён пример с 4-мя переменными, которые надо присвоить в определённые значения, а есть ещё 100 переменных, которые практически неважно, как присвоить. И вот представьте себе, что у вас противоречие в этих нескольких переменных, а все остальные не столь важны. Без ускоренного отката не получится сократить время перебора всех значений.
Так что, если вы решаете переборную задачу, то просто необходимо знать о SAT. Переборные задачи чаще всего встречаются в компиляторах. Поэтому... ;)
Ибо переборный алгоритм по сути своей доказательство теоремы.
Вот здесь находится краткое описание, как работают современные системы.
Интересных вещей там три: обучение конфликтам, периодические перезапуски и ускоренный откат (backjumping, он же откат с учётом конфликта).
Обучение конфликтам уменьшает пространство перебора, причём экспоненциально - и это доказано. Обнаружение конфликтов в назначении переменных происходит всё быстрее и быстрее. Это справедливо для любой переборной задачи.
Периодические перезапуски позволяют избежать перебора в локальном минимуме, так сказать. Они выполняются после некоторого числа конфликтов (которое возрастает после каждого рестарта, гарантируя определение решения, если оно есть) и начинает назначение переменных заново - желательно, в другом порядке.
Ускоренный откат ещё интересней. Для доказательства отсутствия решения нам надо перебрать все возможные варианты назначений переменных. Если у нас проблема всего лишь в одном узком месте, а пространство перебора велико, то мы можем безуспешно перебирать очень долго. По ссылке выше приведён пример с 4-мя переменными, которые надо присвоить в определённые значения, а есть ещё 100 переменных, которые практически неважно, как присвоить. И вот представьте себе, что у вас противоречие в этих нескольких переменных, а все остальные не столь важны. Без ускоренного отката не получится сократить время перебора всех значений.
Так что, если вы решаете переборную задачу, то просто необходимо знать о SAT. Переборные задачи чаще всего встречаются в компиляторах. Поэтому... ;)