Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

Оглавление

Введение

1. О задаче выполнимости булевых формул

2. Существующие алгоритмы решения SAT

2.1 Семейство DPLL

2.2 Семейство WalkSAT

2.3 Модель UniSAT

3. Анализ применимости непрерывных форм к алгоритмам решения

3.1 Анализ DPLL

3.2 Анализ WalkSAT

4. Примененные трансформации в непрерывные формы

5. Экспериментальные результаты

Заключение

Список литературы

Введение

Задача о выполнимости булевых формул (boolean satisfiability problem, или SAT) - задача, которая заключается в ответе на вопрос: можно ли для данной булевой формулы найти такие значения переменных, которую обращают эту формулу в истину? SAT является важной задачей для теории вычислительной сложности. В 1971 году для конъюнктивной нормальной формы задачи была доказана принадлежность к классу NP.

В настоящее время SAT применяется в разных областях компьютерных наук. Наиболее широко эта задача используется в автоматизации разработки микросхем, искусственном интеллекте и биоинформатике. Несмотря на большой прогресс, который был достигнут в области за последние 20 лет, множество возможных применений все еще недостижимы для современных решателей из-за сложности и объема задач, которые возникают в этих направлениях.

Решатели, использующие наиболее популярные в последнее время подходы, применяют дискретный поиск, в то время как непрерывные подходы в классическом SAT не находят широкого применения. Однако непрерывный подход может дать решателю больше информации об исследуемой формуле. Целью данной работы является создание подхода, использующего достижения современных алгоритмов и расширенного на использование непрерывных моделей.

Задачи работы:

1. Описать существующие методы и их особенности;

2. Проанализировать возможность использования непрерывных форм в этих методах;

3. Разработать расширенный алгоритм, использующий непрерывные формы.

Работа вносит вклад в исследование существующих подходов и представляет усовершенствованную версию алгоритма решения задачи. Объектом изучения являются алгоритмы решения проблемы булевой выполнимости, а предметом изучения - целевые функции этих алгоритмов.

Работа разбита на несколько частей: сначала приводится общая информация о задаче выполнимости булевых формул, далее производится обзор существующих методов решения. Эти методы проанализированы с точки зрения использования непрерывных форм булевых переменных. После этого представлены три непрерывные модели трансформации булевых операторов, а также модификация алгоритма gNovelty+, использующая эти модели.

1. О задаче выполнимости булевых формул

В задаче о выполнимости дана булева формула Ц, которая состоит из N переменных x₁, x₂, …, x_n, операторов конъюнкции (), дизъюнкции ( и отрицания (), а также скобок. Задача заключается в поиске ответа на вопрос, можно ли присвоить такие значения переменным, чтобы формула стала истинной.

Пример формулы:

Приведенный пример также является формулой в конъюнктивной нормальной форме (КНФ), т. е. формулы, состоящей из конъюнкций дизъюнкций.

Данная работа фокусируется на задаче в конъюнктивной нормальной форме, так как для формул в дизъюнктивной нормальной форме решение тривиально и производится за линейное время - для разрешимости достаточно, чтобы присутствовала хотя бы одна конъюнкция, не содержащая одновременно противоположные литералы (x и для некоторого x).

Теорема Кука-Левина утверждает, что для формул в конъюнктивной нормальной форме SAT является NP-полной. Концепция NP-полноты была развита параллельно учеными из США и СССР в 60-х и 70-х годах XX века. В 1971 году была опубликована работа Стивена Кука «The complexity of theorem proving procedures», в которой доказывается принадлежность SAT в КНФ к NP-полным задачам. Независимо в то же время доказательство было получено советским математиком Леонидом Левиным, которое было опубликовано в 1973 году в статье «Универсальные задачи перебора».

Класс NP это множество задач разрешимости (задачи квазипереборного типа в терминологии Левина), т. е. заключающихся в ответе «да» или «нет» на некоторый вопрос, в которых доказательство ответа может быть проверено за полиномиальное время на детерминированной машине Тьюринга. Эквивалентным определением является то, что это множество задач разрешимости, которые могут быть решены за полиномиальное время на недетерминированной машине Тьюринга.

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

булевый оператор алгоритм

2. Существующие алгоритмы решения SAT

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

2.1 Семейство DPLL

Полные алгоритмы, как правило, основаны на алгоритме Дэвиса-Патнема-Логемана-Лавленда (DPLL). Этот алгоритм заключается в присвоении некоторой переменной значения истина, упрощении формулы и рекурсивной проверки выполнимости упрощенной формулы. На каждом шаге используются два правила:

· Исключение чистых литералов (pure literal elimination) - литерал называется «чистым» если в формуле встречается либо переменная, либо ее отрицание. В случае встречи чистого литерала можно присвоить значение таким образом, чтобы выполнить дизъюнкты, в состав которых он входит.

· Распространение переменной (Unit propagation или Boolean Constraint Propagation) - если в формуле встречается дизъюнкт с только одним литералом, то обязательно нужно присвоить такое значение переменной, которое выполнит этот дизъюнкт.

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

Формула считается выполнимой, когда все дизъюнкты равны истине, а невыполнимой - когда в процессе решения возникает пустой дизъюнкт, что означает, что всем литералам в этой формуле были присвоены такие значения, которые не приводят к выполнимости этого дизъюнкта. Псевдокод алгоритма:

function DPLL(F):

if F выполнима:

return SAT;

if F содержит пустой дизъюнкт:

return UNSAT;

исключить чистые литералы;

распространить чистые переменные;

if встречен конфликт:

проанализировать конфликт;

добавить выученный дизъюнкт в F;

откатить решение до уровня конфликта;

выбрать переменную x и значение для присвоения;

return DPLL(F с присвоенным x);

На каждом шаге производится выбор «переменной ветвления». Скорость решения зависит от этого выбора и разные решатели используют разные эвристики для того, чтобы выбрать переменную, которая приведет к наиболее эффективному решению.

Дальнейшим развитием алгоритма DPLL стало добавление обучение дизъюнктам, основанное на конфликтах (Conflict-Driven Clause Learning, CDCL). CDCL добавляет две основных оптимизации:

· Нехронологический откат (non-chronological backtracking)

· Получение и запоминание дизъюнктов для предотвращения повторения конфликтов

Ключевым этапом в алгоритме является анализ конфликта. Конфликт возникает тогда, когда необходимо присвоение переменной значений истина (1) и ложь (0) одновременно. Для анализа строится граф импликаций. В графе импликаций с конфликтом присутствует одновременно две вершины для переменной, содержащие присвоение противоположных значений.



Рис. 1. Пример графа импликаций

Граф импликаций показывает, как присвоения значений одних переменных привело к изменению значений других. Вершиной графа выступает присвоение значения переменной, название вершины -x₁₂(7) означает, что переменной x₁₂ был присвоен 0 на 7 уровне решения. В данном случае переменной ветвления явилась x₂, после чего произошел каскад упрощений формулы, который привел к конфликту дизъюнкт и .

В графе вершина x_a доминирует над вершиной x_b тогда, когда все пути от переменной ветвления на данном уровне решения до x_b проходят через x_a. Точкой единичной импликации (Unique Implication Point, UIP) в графе импликаций называется вершина, которая доминирует над обеими вершинам, относящимися к конфликтной переменной. Переменная ветвления всегда является точкой единичной импликации. Для анализа конфликта и создания дизъюнкта конфликта используется разбиение графа на две части: сторону конфликта и сторону причины. Сторона причины включает в себя переменные ветвления, а сторона конфликта - конфликтные литералы. Далее находится разрез графа по точке импликации. Переменные, ребра от которых пересекают границу, добавляются в формулу как дизъюнкт конфликта.

Рис. 2. Примеры разрезов графа импликаций

Различные схемы обучения используют разные разрезы, например, в схеме 1UIP используется первая точка единичной импликации от конфликта, в приведенном примере это -x₄, и, таким образом, будет запомнен новый дизъюнкт . В схеме last-UIP будет использована последняя точка единичной импликации, то есть переменная ветвления, и добавленным дизъюнктом конфликта будет . 1UIP была найдена наиболее эффективной благодаря тому, что запомненный дизъюнкт содержит наиболее близкую к конфликту информацию (Zhang L. и др. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. 2001).

Далее производится возврат решателя на предыдущий уровень решения. В простых версиях DPLL решатель возвращается на один уровень вверх, однако в CDCL возврат происходит на максимальный уровень решения выше текущего в переменных, входящих в дизъюнкт конфликта. В данном примере это 5 уровень, к которому относится присвоение x₉. Откат на этот уровень заставляет переменную поменять свое значение и таким образом выполнить дизъюнкт конфликта.

Многие решатели применяют перезапуск решения. Это помогает избежать траты времени на части пространства решений, в которых нет полезных результатов. Благодаря выученным дизъюнктам решатель не встречает такие же конфликты снова, поэтому перезапуски не вредят процессу решения даже для невыполнимых формул.

2.2 Семейство WalkSAT

Эффективные стохастические алгоритмы локального поиска для решения данной задачи в большинстве своем базируются на WalkSAT или, сокращенно, WSAT. Этот метод, в свою очередь, основан на GSAT (Greedy SAT) - жадном алгоритме локального поиска, разработанном в 1992 (Selman B. и др. A New Method for Solving Hard Satisfiability Problems).

GSAT работает начиная со случайного присвоения значений переменных, после чего производится жадный локальный поиск, в котором в качестве целевой функции используется количество выполненных дизъюнкт. Псевдокод алгоритма приведен ниже:

function GSAT(F):

for try = 0 to max_tries:

создать случайное присвоение переменных A;

for step = 0 to max_steps:

if A выполняет F:

return SAT;

выбрать переменную x в соответствии с целевой функцией;

обратить значение x;

return UNSAT;

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

Концепция использования неоптимальных шагов была дальше расширена в статье «Noise Strategies for Improving Local Search» (Selman B. и др. 1994). Авторы вводят стратегию случайного блуждания (random walk): с некоторой вероятностью p берется случайный невыполненный дизъюнкт, в котором выбирается переменная, значение которой обращается. В оставшихся случаях (с вероятностью 1-p) переменная выбирается с помощью жадного поиска. Авторами предлагается два варианта использования этой стратегии: как дополнение к существующему решению (GSAT+w) и как основа для другого алгоритма - WSAT. В нем сначала выбирается случайный невыполненный дизъюнкт, а уже потом из его переменных выбирается минимизирующая целевую функцию переменная. Таким образом, GSAT+w является добавлением случайного блуждания к жадному алгоритму локального поиска, а WalkSAT - добавлением жадности как эвристики к случайному блужданию.

Позже в статье «Evidence for Invariants in Local Search» (McAllester D. и др. 1997) были представлены две новые процедуры - Novelty и R-Novelty. Их основное отличие заключается в том, что они учитывают то, насколько давно было обращено значение переменной.

В алгоритме Novelty среди двух переменных с одинаковой оценкой выбирается та, которая была обращена наиболее давно. При этом если есть только одна лучшая переменная, и она же была обращена на прошлом шаге, то с вероятностью p (которая названа также уровень шума) берется следующая по оптимальности.

R-Novelty схожа с Novelty, но обладает несколько более сложной логикой. При принятии решения учитывается разница в значении целевой функции, которая принимается за n (где ). Определены четыре случая:

1. Если p < 0,5 и n > 1, выбирается лучшая переменная;

2. Если p < 0,5 и n =1, тогда с вероятностью 2p выбирается вторая по оценке переменная;

3. Если и n =1, выбирается вторая по оценке переменная;

4. Если и n >1, тогда с вероятностью 2(p-0,5) выбирается вторая по оценке переменная.

Авторы отмечают, что производительность R-Novelty сильно зависит от параметра p и имеет почти детерминированное поведение. Чтобы избавиться от определенности, каждые 100 шагов переменная выбирается случайным образом.

Для Novelty и R-Novelty была доказана неполнота с помощью примера выполнимой формулы, которая никогда не будет решена этими алгоритмами (Hoos H. H., 1999). Хотя перезапуски решения позволяют обходить эту проблему, на практике было выяснено, что зачастую такое поведение приводит к стагнации и непродуктивному расходованию времени. Эти недостатки были решены в Novelty+ (Hoos H.H., Tompkins D. A.D. Novelty+ and Adaptive Novelty+. 2004), в котором было добавлено случайное блуждание, сходное с GSAT+w. Как показывает автор, даже использование wp=0,01 позволяет избежать стагнации, наблюдаемой в Novelty. В той же статье приводится адаптивный вариант процедуры, названный AdaptiveNovelty+. В нем уровень шума p подстраивается динамически. В начале поиска p имеет значение 0 (максимально жадный поиск). Это, как правило, приводит к быстрым улучшениям и последующей стагнации, когда значение целевой функции не улучшается за некоторое количество шагов. В таком случае p увеличивается. Когда решатель выходит из области вызвавшей стагнацию, значение постепенно снижается.

Chu Min Li и Wen Qi Huang предложили другой подход к решению проблемы детерминизма в Novelty. Они использовали решение, основанное на сохранении времени изменения переменных чтобы разнообразить поиск. Их эвристика Novelty++ в вероятностью dp выбирает наиболее давно измененную переменную из случайного дизъюнкта, а в остальных случаях ведет себя так же как Novelty. Авторы дольше улучшили Novelty++ с помощью сочетания жадного поиска из GSAT с вариантом табу-поиска. В алгоритме G²WSAT dо время поиска все переменные, которые не ведут к строгому улучшению целевой функции, считаются табу (то есть не могут быть выбраны в этой фазе). После того, как значение переменной обращается, переменные, которые становятся перспективными, то есть те, которые приведут к строгому улучшению целевой функции, становятся доступными для поиска. На следующем шаге решатель попытается выбрать лучшую перспективную переменную, основываясь на целевой функции. Если же таких переменных нет, то есть решатель находится в локальном минимуме, используется эвристика Novelty++.

В алгоритмах стохастического локального поиска большое внимание уделяется выходу из локальных минимумов и изменению направления поиска в случае попадания в эти минимумы. Одной из техник является использование взвешенной целевой функции. Этот подход называется динамический локальный поиск (Dynamic Local Search, DLS). DLS-алгоритмы можно разделить на две категории: алгоритмы, использующие мультипликативное взвешивание, и алгоритмы, использующие аддитивное взвешивание.

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

Аддитивное взвешивание заключается в увеличении весов дизъюнкт на 1 при нахождении в локальном минимуме и уменьшении на 1 после некоторого количества увеличений весов.

Подходы DLS и SLS были объединены в одном из наиболее эффективных современных алгоритмов - gNovelty+ (Pham D. N. Combining Adaptive and Dynamic Local Search for Satisfiability. 2008). Псевдокод алгоритма представлен ниже:

function gNovelty+(F, max_tries, max_steps, sp, wp):

for try = 1 to max_tries

выставить вес дизъюнкт в 1;

создать случайное присвоение переменных A;

for step = 1 to max_steps

if A выполняет F

return SAT;

else

с вероятностью случайного блуждания wp

выбрать случайную переменную x из невыполненного дизъюнкта;

else if существует перспективная переменна

жадно выбрать перспективную переменную x, выбирая более давно измененную, если оценка одинаковая;

else

выбрать переменную x в соответствии со взвешенной эвристикой AdaptNovelty;

увеличить вес невыполенных дизъюнкт на 1;

с вероятностью sp сгладить вес всех дизъюнкт;

обратить значение x в A;

return UNSAT;

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

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

В локальных минимумах, если невозможно сделать шаг с улучшением показания целевой функции используется взвешенный алгоритм выбора переменной AdaptNovelty. Этот алгоритм выбирает случайную дизъюнкту и выбирает лучшую переменную (относительно целевой функции) и, если это не самая недавно измененная переменная, выбирает ее для изменения. Если это самая недавно измененная переменная, то она выбирается с вероятностью 1-p, а с вероятностью p выбирается вторая лучшая переменная. Параметр шума p при этом адаптивно настраивается - если сделанные шаги не приводят к улучшению значения целевой функции, то он увеличивается, а если наоборот, то уменьшается.

2.3 Модели UniSAT

В 1988 Jun Gu представил группу моделей, названную «Универсальные модели проблемы SAT» (The Universal SAT Problem Models, UniSAT). Эти модели представляют собой трансформацию дискретных операторов в непрерывные. Он заменил операторы и на + и соответственно. Каждой булевой переменной была поставлена в соответствие вещественная переменная . Для этих переменных определена целевая функция:

Где функция переменной это произведение функций литералов :



Функция литерала определяется следующим образом:

Значение равно истине, если , и лжи, если . В ином случае это значение неопределенно.

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

3. Анализ применимости непрерывных форм к алгоритмам решения

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

Использование непрерывной формы повлечет дополнительные расходы по памяти, так как число с плавающей точкой занимает больше места, чем булева переменная. Однако на практике разница достаточно маленькая. Для того, чтобы оценить изменение затрат на хранение состояния переменных возьмем случай для формулы с 1500 000 переменными. Это примерно соответствует максимальному размеру формул в соревнованиях SAT Competitions (например, формула transport-transport-city-sequential-35nodes-1000size-4degree-100mindistance-4trucks-14packages-2008seed.050-SAT.cnf содержит 1 575 206 переменных и 8464620 дизъюнкт), хотя большинство формул имеют гораздо меньший размер. За тип данных, используемый в дискретном представлении, примем 8-битное целое число (unsigned short в C или bool в C++). В таком случае одно присвоение будет занимать 1500000 байт или 1,43 МБ. Если же на каждую переменную выделять 32-битное значение, то присвоение займет в четыре раза больше, или 5,72 МБ. При этом стоит учесть, что затраты на хранение остальных структур составят гораздо больше и не зависят от того, в каком виде хранятся переменные. Например, если эти 8000000 дизъюнкт каждая имеют по три переменные (то есть если это задача 3SAT), то решатель будет хранить 24000000 указателей на переменные, каждый из которых занимает 32 или 64 байта, в зависимости от разрядности системы. В такой ситуации дизъюнкты займут 732,42 МБ или 1464,84 МБ соответственно. На этом фоне 4,29 МБ затрат не имеют большой важности.

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

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

3.1 Анализ DPLL

DPLL на практике основывается на распространении переменной, анализе конфликтов и выборе переменной ветвления. Исключение чистых литералов зачастую не используется ввиду относительно больших затрат на их обнаружение и редкости их появления (Johannsen J. 2005).

Недавнее исследование влияние различных оптимизаций на производительность DPLL-решателей на примере MiniSAT показало, что наибольшую значимость имеет обучение конфликтам - из 10000 задач в стандартной конфигурации MiniSAT решил 9068, а с отключенным обучением конфликтам - только 4837. При этом анализ конфликта, а точнее построение графа импликаций, зависит от распространения переменной. Таким образом, можно утверждать, что распространение переменной является центральной процедурой для алгоритма.

Для распространения переменной необходимо, чтобы все остальные переменные отсутствовали или были выставлены в противоположное значение от встречаемого в дизъюнкте. Если же переменные выставляются в дробные значения, то это означает, что их нельзя игнорировать при обнаружении единичных дизъюнкт.

Покажем, что использовать дробные значения нецелесообразно. Например, пусть в некоторой формуле присутствует дизъюнкт:



Допустим, что значение не определено, и . 0 соответствует лжи, а 1 - истине. С такими значениями мы можем не учитывать переменные , так как только определяет выполнимость этого дизъюнкта. В реальных имплементациях могут быть удалены из дизъюнкта для экономии времени при его обработке. На оставшейся переменной может сработать распространение. Теперь рассмотрим случай с . В этой ситуации уже не является определяющей переменной, и распространение не будет вызвано.

Дальше покажем, что при срабатывании распространения имеет смысл присваивать только целое значение. Пусть на некотором шаге алгоритма остается формула из нескольких дизъюнктов:

Если подвергается распространению со значением 0, то мы можем удалить его из дизъюнктов, в которых встречается литерал и удалить дизъюнкты, в которых встречается литерал . За этим последует каскад упрощений. После распространения формула примет следующий вид:

Далее сработает распространение , после которого останется только литерал , который также упростится. Однако если вначале использовать не 0, то вид формулы останется неизменным, так как мы не можем считать выполненными дизъюнкты с , и не можем удалить из тех дизъюнкт, где он встречается.

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

Еще одним важным шагом является выбор переменной ветвления. На данный момент самой эффективным подходом является динамическая оценка, основанная на истории конфликтов. Основой таких эвристик является устаревающая сумма, независимая от состояния переменной (Variable State Independent Decaying Sum, VSIDS). Впервые эта эвристика была реализована в решателе Chaff. Во время конфликта для всех литералов, присутствующих в дизъюнкте конфликта, счетчик увеличивается на единицу. На каждом шаге в качестве переменной ветвления берется переменная и ее значение с максимальной оценкой. Периодически все счетчики делятся на некоторую константу. При использовании непрерывных форм возникает проблема - если хранится оценка для переменной и ее отрицания, то как решать, какое дробное значение использовать для выбранной переменной на каждом шаге? Возможное решение включает в себя присвоение значения, основанного на разнице оценок:

Где - оценки литералов соответственно.

Проблема с таким подходом в том, что оценки соответствуют только встречаемости литералов в конфликте и поэтому их разница не несет никакой полезной информации относительно значения переменной. Такую информацию дает другой способ - динамическая наибольшая индивидуальная сумма (Dynamic Largest Individual Sum, DLIS), который выбирает самый частый литерал, встречающийся в невыполненных дизъюнктах. Однако уже было показано, что такой способ гораздо менее эффективен, чем VSIDS (Moskewicz M. W. и др. 2001).

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

3.2 Анализ WalkSAT

В алгоритмах семейства WalkSAT было уделено внимание двум частям: случайному блужданию и целевой функции. Не все решатели этого семейства используют случайное блуждание, поэтому анализ применим для алгоритмов, начиная с Novelty+. Что же касается Novelty, то расширение на непрерывные формы не избавляет его от неполноты, которая исходит из того ограничения, что он рассматривает только переменные, присутствующие в невыполненных дизъюнктах.

Важной проблемой, возникающей при локальном поиске, является избежание локальных минимумов и выход из областей стагнации, которые не содержат решений. Для этого используется случайное блуждание. Эту технику можно расширить на присваивание дробного значения вместо целого - это так же поможет изменить область решения, хотя и не имеет преимуществ перед обычным присваиванием значения, выполняющим случайно выбранный дизъюнкт.

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

Было решено реализовать решатель, использующий алгоритм gNovelty+, расширенный на использование непрерывных форм.

4. Примененные трансформации в непрерывные формы

В общем виде трансформация дискретных значений в непрерывный вид включает в себя два связанных изменения - преобразование переменных и преобразование операторов.

Преобразование переменных заключается в их приведении в непрерывный вид. Если в дискретной форме переменная может принять значение 0 или 1, то в непрерывной форме она принимает некоторый диапазон значений. Так, например, в модели UniSAT переменные принимают значение в диапазоне от -1 до 1. В данной работе использовался диапазон от 0 до 1.

Были рассмотрены три модели преобразования операторов. Первая модель, названная varprob, представляет непрерывную переменную , соответствующую дискретной переменной как вероятность того, что равно истине:

Трансформации операторов при этом соответствуют сложениям и умножениям вероятности:

Вторая модель называется vardiv и использует следующие преобразования операторов:



Третья модель - varchoice - использует выбор между значениями двух переменных в качестве операторов:

Важной характеристикой моделей является тот факт, что если решатель делает выбор только между двумя значениями - 0 и 1, они ведут себя аналогично дискретному варианту. Такое поведение гарантирует, что применение этих моделей к существующим дискретным алгоритмам будет являться именно расширением процесса решения, а не его изменением.

Также все модели предоставляют информацию о том, выполняется ли формула. Так как модели ведут себя так же, как и булевы операторы на дискретных значениях, результат вычисления модели на формуле F с присвоением X дает оценку, насколько выполнима формула:

· При формула является невыполненной;

· При есть шанс, что формула является выполненной;

· При формула выполняется;

Стоит заметить, что значение, отличное от нуля и меньше единицы само по себе не гарантирует, что формула выполнима, например, для очевидно невыполнимого случая , с присвоением , значение S будет равно 0,25.

Рассмотрим возможное изменение целевой функции. В WalkSAT в качестве целевой функции используется число невыполненных дизъюнкт. Можно представить эту функцию в виде следующих формул для случая с n переменных и m дизъюнктов:

Здесь - вектор присвоения переменных , а - оценка для некоторого дизъюнкта.

Для алгоритмов, использующих взвешенную целевую функцию, таких как gNovelty+, в целевую функцию добавляется вектор весов дизъюнктов и она принимает следующий вид:

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

Отметим, что в целевой функции не используется непрерывная оценка для всей формулы. Эту оценку мы будем использовать как источник дополнительной информации о формуле. Хотя, как было показано выше, оценка не позволяет определить, выполнима ли формула, ее можно использовать для того, чтобы направить решатель в более перспективные области решения. В расширенном алгоритме, S используется для того, чтобы сделать выбор между переменными с одинаковым значением целевой функции. Если же S для двух переменных совпадают, то используется переменная, значение которой менялось более давно.

Псеводокод шага получившегося алгоритма, gNovelty+c:

if оценка формулы равна 1:

return SAT;

с вероятностью случайного блуждания wp:

выбрать случайную переменную x из невыполненного дизъюнкта;

выставить x в значение, выполняющее этот дизъюнкт;

else if существует перспективная переменная:

жадно выбрать перспективную переменную x и ее значение, между двух одинаковых выбирая ту, у которой более высокая оценка S, а при равных S более давно измененную;

else

выбрать переменную x и ее значение в соответствии со взвешенной эвристикой AdaptNovelty с непрерывной целевой функцией;

увеличить вес невыполенных дизъюнкт на 1;

с вероятностью sp сгладить вес всех дизъюнкт;

выставить x в найденное значение

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

Есть два подхода к поиску значения переменной: выбор лучшего из нескольких вариантов (например, 0, 0,5 и 1) и подбор оптимального значения с заданной точностью. Было решено применить первый подход, так как он работает существенно быстрее. Фактически производится выбор только из двух вариантов - то значение, которое уже присвоено переменной, можно не рассматривать.

5. Экспериментальные результаты

Было выяснено, что оптимальным подходом является varprob. Хотя данная модель показывает себя хуже, чем varchoice на маленьких формулах, она работает за лучшее время на больших задачах, что является неожиданным результатом, так как ожидалось, что varchoice будет самой быстрой моделью из-за простоты реализации. Скорее всего, оптимизированные арифметические функции показывают лучшую производительность.

Модель vardiv является самой медленной. Это неудивительно учитывая то, что ее трансформация оператора является самой сложной.

Табл. 1. Время решения формул с использованием различных моделей

Число переменных:	Число дизъюнкт:	Время решения (сек)
		varchoice	varprob	vardiv
5	40	0.00103	0.00127	0.00151
10	60	0.001	0.00110	0.00139
20	150	0.00211	0.00235	0.00361
20	150	0.00201	0.00233	0.00333
50	300	0.00497	0.00477	0.00726
100	1000	0.04302	0.03791	0.04865
100	1500	0.04921	0.04343	0.07274
200	3000	0.12928	0.10949	0.15982
1000	8000	0.37023	0.36946	0.43568
2000	10000	0.43579	0.40233	0.51633

Заключение

Эта работка - попытка предоставить новые модели для непрерывных решателей SAT. Существующие теоретические и практические данные и подходы были проанализированы. На их основе был создан алгоритм для эффективного локального поиска на основе трех разработанных моделей. Были получены данные о производительности, однако дальнейшие исследования и оптимизации необходимы для того, чтобы в полной мере раскрыть потенциал изученного подхода.

Список литературы

1. Cook S.A. The complexity of theorem-proving procedures // ACM symposium on Theory of computing. 1971. С. 151-158.

2. Davis M., Logemann G., Loveland D. A machine program for theorem-proving // Communications of the ACM, Т. 5, № 7, Jul 1962. С. 394-397.

3. Glover F. Tabu Search-Part I // ORSA Journal on Computing, Т. 1, № 3, 1989. С. 190-206.

4. Gu J., Purdom P.W., Franco J., Wah B.W. Algorithms for the Satisfiability (SAT) Problem: A Survey // DIMACS Series in Discrete Mathematics and Theoretical Computer Science. 1996. С. 19-152.

5. Gu J. Global Optimization for Satisfiability (SAT) Problem // IEEE Transactions on Knowledge and Data Engineering, Т. 6, № 3, Jun 1994. С. 361-381.

6. Hoos H.H., Tompkins D.A.D. Novelty+ and Adaptive Novelty+ // SAT Competition. 2004.

7. Hoos H.H. An adaptive noise mechanism for walkSAT // 18th National Conference on Artificial intelligence. 2002. С. 655-660.

8. Hoos H.H. On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT // 16th National Conference on Artificial intelligence. 1999. С. 661-666.

9. Huang J. The Effect of Restarts on the Efficiency of Clause Learning // International Joint Conference on Artificial Intelligence. Нью-Йорк. 2007. С. 2318-2323.

10. Johannsen J. The Complexity of Pure Literal Elimination // В кн.: SAT 2005 / ред. Giunchiglia E., Walsh T. Springer, 2005. С. 89-95.

11. Katebi H., Sakallah K.A., Marques-Silva J.P. Empirical Study of the Anatomy of Modern Sat Solvers // 14th International Conference, SAT 2011. 2011. С. 343-356.

12. Li C.M., Huang W.Q. Diversification and Determinism in Local Search for Satisfiability // 8th International Conference, SAT 2005. 2005. С. 158-172.

13. Marques-Silva J., Lynce I., Malik S. Conflict-Driven Clause Learning SAT Solvers // В кн.: Handbook of Satisfiability / ред. Biere A., Heule M., Maaren H.V., Walsch T. IOS Press, 2008. С. 127-149.

14. Marques-Silva J. Practical Applications of Boolean Satisfiability // 9th International Workshop on Discrete Event Systems. 2008. С. 74-80.

15. McAllester D., Selman B., Kautz H. Evidence for Invariants in Local Search // 14th National Conference on Artificial Intelligence. 1997. С. 321-326.

16. Moskewicz M.W., Zhao Y., Zhang L., Madigan C.F., Malik S. Chaff: Engineering an Efficient SAT Solver // 39th Design Automation Conference. Лас Вегас. 2001.

17. Pham D.N., Gretton C. gNovelty+ // SAT Competition. 2007.

18. Pham D.N., Thornton J., Gretton C., Sattar A. Combining Adaptive and Dynamic Local Search for Satisfiability // Journal on Satisfiability, Boolean Modeling and Computation, Т. 4, 2008. С. 149-172.

19. Schuurmans D., Southey F. Local search characteristics of incomplete SAT procedures // Artificial Intelligence, Т. 132, № 2, Nov 2001. С. 121-150.

20. Selman B., Kautz H.A., Cohen B. Local Search Strategies for Satisfiability Testing // DIMACS series in discrete mathematics and theoretical computer science, 1995. С. 521-532.

21. Selman B., Kautz H.A., Cohen B. Noise strategies for improving local search // 11th National Conference on Artificial Intelligence. 1994. С. 337-343.

22. Selman B., Levesque H., Mitchell D. A new method for solving hard satisfiability problems // 10th national conference on Artificial intelligence. 1992. С. 440-446.

23. Sorensson N., Een N. MiniSat v1.13 - A SAT Solver with Conflict-Clause // MiniSat. 2005.

24. Tichy R., Glase T. Clause Learning in SAT // Seminar Automatic Problem Solving. 2006.

25. Zhang L., Madigan C.F., Moskewicz M.H., Malik S. Efficient conflict driven learning in a Boolean satisfiability solver // International Conference on Computer-Aided Design. 2001. С. 279-285.

26. Левин Л.А. Универсальные задачи перебора // Пробл. передачи информ., Т. 9, № 3, 1973. С. 115-116.

Размещено на Allbest.ru