Application of SAT-approach for solving combinatorial problems.pdf Рассмотрим использование SAT-подхода в решении различных дискретных задач«переборной» природы. Для многих относительно простых по постановкам дискрет-ных задач не известно алгоритмов, эффективных хотя бы на некоторых практическизначимых подклассах рассматриваемых задач.Простейший пример такого рода - анализ свойств недетерминированного автома-та A, распознающего некоторый регулярный язык. Может оказаться так, что диагно-стируемое свойство (либо его отсутствие) может быть установлено эффективно длядетерминированного автомата A, который эквивалентен A. Однако процедура преоб-разования A в A обычно крайне трудоемка [1]. Более того, реализация этой процедурытребует работы со структурами данных, представляющими автоматы. Другой подходк этой проблеме состоит в переходе от автомата A к кодирующей его системе буле-вых уравнений S(A). Такой переход осуществляется эффективно [2]. Диагностируемоесвойство автомата A либо его отсутствие может быть установлено на основе решениясистемы S(A). Решение системы S(A) может быть найдено с применением современ-ных быстрых булевых решателей (SAT-решателей, [3]).Следующий пример такого рода - автоматные модели в современной вычислитель-ной биологии [4]. На первый взгляд совершенно непонятно, какие вычислительные ме-тоды следует использовать для их изучения. Однако с этими моделями естественнымобразом связываются некоторые дискретные функции (см., например, [5]), и для вы-явления тех или иных свойств моделей приходится решать задачи обращения такихфункций, которые также допускают эффективную сводимость к булевым уравнениям.Еще одна область применения SAT-подхода связана с задачами комбинаторнойоптимизации. Имеются мощные коммерческие пакеты решения оптимизационных за-дач из семейства 0-1-целочисленного линейного программирования (ЦЛП). Соответ-ствующие алгоритмы комбинируют технику ветвей, границ и отсечений с методамирешения задач линейного программирования над полем рациональных чисел. Одна-ко данные методы подходят далеко не ко всем задачам комбинаторной оптимизации.Современные решатели ЦЛП-задач, как правило, не работают с нелинейными и невы-пуклыми целевыми функциями. Между тем и такие задачи допускают эффективнуюсводимость к булевым уравнениям и, в конечном счете, к SAT-задачам.В работе приведены результаты решения задачи поиска неподвижных точек и цик-лов автоматных отображений в генных сетях дискретно-автоматной природы со слож-ными многофакторными механизмами внутреннего взаимодействия и результаты па-раллельного решения SAT-задач, кодирующих квадратичную задачу о назначениях,в отношении которой коммерческие решатели, основанные на методе ветвей и границ,оказываются низкоэффективными.

Скачать электронную версию публикации