Реферат: Методы улучшения сходимости алгоритма минимизации функционала, ассоциированного с задачей 3-sat. The methods of convergence improving of  3-sat associated algorithm

УДК 519.7

 
МЕТОДЫ УЛУЧШЕНИЯ СХОДИМОСТИ АЛГОРИТМА МИНИМИЗАЦИИ ФУНКЦИОНАЛА, АССОЦИИРОВАННОГО С ЗАДАЧЕЙ 3-SAT.
THE METHODS OF CONVERGENCE IMPROVING OF  3-SAT ASSOCIATED ALGORITHM
 

И.Г. Хныкин, Р.Т.Файзуллин
Омский государственный университет им.Ф.М.Достоевского, г.Омск
rtf@univer.omsk.su

 

В [2] рассматривается алгоритм минимизации функционала специального вида применительно к задаче 3-SAT. Предлагаемые в данной работе методики существенно улучшают сходимость данного алгоритма.
Общая схема
Рассмотрим  переход от задачи ВЫПОЛНИМОСТЬ (SAT) к задаче поиска глобального минимума функционала вида (1):

, где

, где ,             (1)

Суммирование ведется по всем M конъюнктам ДНФ, эквивалентной исходной КНФ. Соответствие между булевыми и вещественными переменными следующее: ЛОЖЬ0, ИСТИНА1.

Переход от булевой формуле к вещественной основан на использовании соответствия:

, где

Легко заметить, что  соответствует достижению значения ИСТИНА на исходной КНФ.

Без потери общности можно рассмотреть 3-ДНФ, эквивалентную исходной КНФ. Получим следующий функционал:

, где ,  здесь триплет          (2)

Дифференцируя функционал по всем переменным  , мы получаем систему уравнений:

,     где ,         (3)

или.

Коэффициенты  и  связаны соотношением: .

Поясним выбор представления исходной КНФ именно в виде эквивалентной 3-ДНФ. Дифференцируя функционал  (см.(1)) по всем переменным , мы получаем систему уравнений аналогичную (3), но количество вкладов в  и  определятся длиной скобок. Любая процедура решения этой системы при произвольной длине скобок будет естественным образом приводить к большим ошибкам округления. Ограничивая число переменных в скобках, мы исключаем эту техническую трудность.

Рассмотрим систему (3), как нелинейное операторное уравнение:

      (4)

Модифицированный метод последовательных приближений, так называемый метод последовательных приближений с «инерцией», есть решение следующей системы уравнений:

  (5)

Здесь описана реализация модифицированного метода последовательных приближений с «инерцией» в применении к решению задачи 3-SAT. Программа, реализующая метод написана на языке C++.
^ Реализация алгоритма (fhsat 2.0) Структуры и типы данных
Формула храниться в виде следующей структуры:

struct Formula

{

         TXIND** formula;     - 2-мерный массив, в котором хранится формула ДНФ в формате DIMMACS, без заключающих нулей. Нулевой элемент i-й строки  массива хранит количество литералов в i-й скобке.

         ^ TN nClause;               - количество скобок в формуе

         TN nVar;                   - количество литералов в формуле (количество неизвестных)

 

         ^ BOOL bCNF;             - булевская переменная, определяет тип формулы: ДНФ или КНФ

 

         TN nDoClauseFrom;

         TN nDoClauseUpto;  - скобки от nDoClauseFrom до nDoClauseUpto используются для поиска решения, остальные игнорируются.

 

         TN l;                            - служебная переменная, добавлена для предварительного расчета первых производных по всем переменным.

         string* sName;                       - служебная переменная, хранит общую информацию о формуле.

};

Размеры формулы задаются максимальными значениями для выбранного типа.

Тип ^ TN – заранее выбранный натуральный тип данных. TXIND - заранее выбранный целочисленный тип данных. TX - заранее выбранный вещественный тип данных. Вектора приближений хранятся в виде массивов типа TX. Специфика задачи предполагает, что компоненты вектора приближений
^ Процедура решения
Главная процедура состоит из последовательных итераций.

Итерация состоит из двух блоков. Первый блок, определяется формулой (5), используется схема Зейделя. Суть схемы Зейделя в том, что при нахождении очередного  на -й итерации, это значение подставляется вместо .

Надо сказать, что реализация алгоритма допускает использование схемы Якоби, когда найденные  не используются в текущей итерации.

Тесты показали, что схема Зейделя более устойчива в применении к решаемой задаче. Именно, после каждой итерации по схеме Зейделя значение функционала монотонно уменьшается, чего нельзя сказать о схеме Якоби. Кроме того, во всех случаях схема Зейделя быстрее приводила к решению.

Второй блок – т.н. сдвиг по градиенту. Рассмотрим (4). Пустьявляется решением, тогда . Уравнение (5) переписывается в виде . Это необходимое условие, которому должен удовлетворять вектор решения. Если текущее –е приближение  не является решением, то . Для итеративной формулы: . Следовательно, что бы удовлетворить необходимому условию, необходимо перейти к вектору:

                   (6)

Необходимо сказать, что после (6) возможна ситуация, когда . В этом случае необходимо насильно ограничивать , иначе метод начинает расходится. Особенно это проявляется на K-SAT формулах при K>4.

При приближении к решению скорость сходимости может сильно уменьшаться, по сути алгоритм зацикливается на некотором плато и траектория сходимости больше не выходит за пределы этого плато. Чтобы сойти с плато и продолжить сходимость к решению применяется т.н. метод смены траектории.

Метод смены траектории заключается в поиске нового вектора приближения, который бы обладал свойствами не хуже, чем текущий вектор приближения, но позволял бы продолжить поиск решения. Суть метода нахождения такого вектора в следующем.

Рассмотрим 3-КНФ, эквивалентную исходной 3-ДНФ (см. (1)).

, где ,  здесь триплет (7)

 



Для данного приближения , рассмотрим множество переменных . С вероятностью m_p поменяем значения  на противоположные. При этом, вероятность того, что другие триплеты станут невыполнимыми невысока. Экспериментально установлено, что полученный вектор  обладает свойствами не худшими, чем  (количество невыполнимых триплетов до и после операции примерно одинаково). Используя данный вектор  в качестве нового начального приближения, алгоритм очень быстро (в большинстве случаев за 5-10 итераций) находит следующее приближение, на котором функционал  достигает значения не хуже, чем на векторе . При этом, очень часто, удается проскочить плато, но при дальнейшем движении по новой траектории метод может зациклиться на другом плато. Тогда метод смены траектории повторяется.

Наряду с множеством  рассмотрим множество . Введем вероятности m_p0, m_p1. С вероятностью m_p0 при смене траектории будем использовать множество . С вероятностью m_p1  – . Вероятность m_p0 влияет на величину изменения вектора и при этом количество невыполнимых триплетов не увеличивается. Вероятность m_p1 влияет на качественное изменение вектора, количество невыполнимых триплетов может увеличиться. В принципе, чем выше m_p1, тем меньшую роль играют рестарты.

Метод смены траектории применяется при достижении условия .
Результаты
После каждой модификации проводилось тестирование алгоритма для определения эффективности проделанных изменений. При тестировании использовалось несколько типов примеров. Тесты с соревнований решателей SAT 2005 года www.lri.fr/~simon/. Тесты библиотеки SATLib www.cs.ubc.ca/~hoos/. Тесты, сформированные для задачи факторизации. Тесты больших размерностей, сформированные случайным образом.

^ Метод последовательных приближений с «инерцией»

Основной результат вычислительных экспериментов относительно модифицированного метода последовательных приближений, проводившихся для случайного наполнения наборов скобок SAT и 3-SAT, представлен в [2]. При соотношении , где  это число переменных, число скобок в 3-SAT (вплоть до , ), итерационная процедура всегда сходится к решению. Но при увеличении  скорость сходимости резко падает и, хотя большинство компонент решения  формируется верно, и быстро, оставшаяся часть  оказывается практически недостижимой в силу накопления ошибок округления.

^ Метод последовательных приближений с инерцией (+ Сдвиг по градиенту)

Сдвиг по градиенту хорошо сокращает погрешности и ускоряет сходимость алгоритма. Вычислительные эксперименты со случайными формулами показали заметное уменьшение времени решения тестов. Число решенных примеров увеличилось примерно на 20%.

Применение данного приема позволяет  достаточно эффективно решать тесты uf20-91 (из 1000 тестов решены 703). Однако некоторые тесты решаются только после задания определенного начального приближения, что говорит о необходимости рестартов.

На примерах uf250-1065 алгоритм показал результат 6% (предыдущая версия алгоритма - 1%).

Тесты SAT-2005 (OKGenerator10000-42000 – 10000 переменных, 42000 скобок) использовались в сокращенной форме. Максимально удалось решить подформулы из 36000 скобок (предыдущая версия алгоритма – 35000 скобок). На подформулах из более чем 36000 скобок метод зацикливается на некотором плато. Это говорит о необходимости смены траектории.

^ Метод последовательных приближений с инерцией (+ Метод смены траектории)

Метод смены траектории существенно увеличил число решаемых примеров (особенно SATLib). Результаты следующие:

Тесты
SATLib

Количество литералов (N)

Количество скобок (M)

Число тестов

% решенных тестов

Максимальное число итераций

Backbone-minimal Sub-instances (формулы с минимальным хребтом), 3-SAT

RTI

BMS

100

100

429

<429

500

500

98,6

79,8

19988

29831

Controlled Backbone Size Instances (b – размер хребта), 3-SAT

CBS_b10

CBS_b10

CBS_b90

100

100

100

403

449

449

1000

1000

1000

100

100

98

38972

38880

29738

Uniform Random 3-SAT (UF)

uf20-91

uf250-1065

20

250

91

1065

1000

100

100

98

448

9731

SAT-encoded "Flat" Graph Colouring Problems

flat30-60

90

300

100

100

4317

Примеры SAT-2005 OKGenerator оказались самыми сложными.

Тесты SAT-2005 OKGenerator10000-42000 (10000 переменных, 42000 скобок) использовались в сокращенной форме. Максимум удалось решить подформулы из 41000 скобок. Максимальное время решения – 12 часов, число итераций . При этом подформулы из 40000 скобок решались за 20 минут, число итераций .

Для тестов SAT-2005 OKGenerator2000-8400 (2000 переменных, 8400 скобок) удалось решить в среднем подформулы из 8300 скобок. Максимальное время решения – 20 минут.

Надо сказать, что при увеличении числа скобок в подформулах тестов OKGenerator плато, на которых зацикливался алгоритм, появлялись раньше. По мере приближения к решению плато появлялись чаще и сходить с них становилось сложней. Это обусловлено тем, что траекторий, ведущих к решению, становиться все меньше и поэтому метод смены траектории может не работать. Меняя слишком много компонент вектора приближения, мы отбрасываем траекторию назад и впоследствии можем снова попасть на то же плато. Меняя слишком мало компонент, мы рискуем не сойти с плато вообще. Сложно определить, какие компоненты вектора необходимо изменить, что бы остаться на той же (или эквивалентной) траектории и в то же время сойти с плато.
^ Увеличение разрядности вычислений
Была исследована сходимость алгоритма при увеличении разрядности вычислений. Испытания с типами DOUBLE и FLOAT показали преимущество вычислений с двойной точностью. При переходе на тип DOUBLE количество решенных примеров увеличивается на 10%, скорость сходимости в среднем также увеличивается.

Дальнейшее увеличение разрядности к значимому эффекту не приводит. Скорость сходимости на плато падает очень быстро с любой точностью вычислений.

Сравнительные результаты вычислений для различных типов тестов с количеством значащих цифр после запятой 19 (LONG DOUBLE) и 200 приведены на графике.



Как видно из графиков траектория при приближении к плато хорошо аппроксимируется функцией вида:

. Это говорит о том, что сойти с плато без смены траектории практически невозможно.

Для увеличения разрядности вычислений использовалась библиотека больших чисел WinNTL версия 5.4.
^ Дальнейшие направления
Дальнейшие исследования связаны с разработкой дополнительных методик улучшения сходимости алгоритма.

Рассмотрим тесты серии Backbone-minimal Sub-instances библиотеки SATLib. Тесты BMS являются подформулами соответствующих тестов RTI. Однако также являются более трудными для решения, несмотря на то, что количество скобок в них не больше, а решений не меньше. Частично обоснование описано в [5]. Следовательно, необходимо найти эквивалентную КНФ, которая бы обладала лучшими свойствами для решения предложенным алгоритмом. Одним из таких видоизменений является метод резольвент, который используется в некоторых других решателях (см. [3]).

Можно анализировать поведение значений компонент последовательности векторов приближений и на основе этого экстраполировать конечное значение. Например, если компонента вектора больше 0.5 и постоянно растет, то можно сделать вывод, что в векторе решении она равна 1, и наоборот. Предварительные испытания дали некоторые результаты. В частности, данная эвристика была подтверждена в 70% случаев. Было решено разрабатывать и тестировать данную эвристику далее.

Экспериментально показано, что для примеров с небольшим числом скобок (около 500) вероятность m_p1 должна быть маленькой. Иначе метод смены траектории отбрасывает траекторию решения назад. На больших примерах с увеличением m_p1 и m_p0 сначала скорость сходимости заметно увеличивается. Но при приближении к нулевой отметке (т.е. к решению) слишком большие значения m_p1 и m_p0 опять же приводят к отбрасыванию траектории назад. Следовательно, при приближении к решению необходимо уменьшать эти вероятности. Таким образом, необходимо определить оптимальные значения m_p1 и m_p0, либо внедрить адаптивный алгоритм определения оптимальных значений в ходе работы алгоритма.
Литература
[1] Файзуллин Р.Т. О решении нелинейных алгебраических систем гидравлики // Сибирский журнал индустриальной математики. -1999.-№2. –С. 176-184.

[2] Файзуллин Р.Т., Cалаев Е.В. Применение метода последовательных приближений с «инерцией» к решению задачи выполнимость, ОМГУ, г.Омск.

[3] Duc Nghia Pham and Anbulagan. Resolution Enhanced SLS solvers: R+PAWS, R+RSAPS and R+ANOV+, 2005

[4] Gu J.,Purdom P.W.,Franco J.,Wah B.W Algorithms for the Satisfiability Problem: A Survey // DIMACS Series in Discrete Mathematics and Theoretical Computer Science. -1996. –C. 19-151.

[5] Josh Singer, Ian Gent and Alan Smaill Backbone Fragility and the Local Search Cost Peak. Journal of Artificial Intelligence Research, 12: 235-270 2000