Зміст

Вступ
. Про завдання здійсненності булевих формул
. Існуючі алгоритми вирішення SAT
.1 Сімейство DPLL
.2 Сімейство WalkSAT
.3 Модель UniSAT
. Аналіз застосовності безперервних форм до алгоритмів рішення
.1 Аналіз DPLL
.2 Аналіз WalkSAT
. Застосовані трансформації в безперервні форми
. експериментальні результати
висновок
Список літератури

Вступ

Завдання про здійсненності булевих формул (boolean satisfiability problem, або SAT) - завдання, яке полягає у відповіді на питання: чи можна для даної булевої формули знайти такі значення змінних, яку звертають цю формулу в істину? SAT є важливим завданням для теорії обчислювальної складності. У 1971 році для кон'юнктівной нормальної форми завдання була доведена приналежність до класу NP.
В даний час SAT застосовується в різних областях комп'ютерних наук. Найбільш широко ця задача використовується в автоматизації розробки мікросхем, штучний інтелект та біоінформатики. Незважаючи на великий прогрес, який був досягнутий в області за останні 20 років, безліч можливих застосувань все ще недосяжні для сучасних решателей через складність і обсягу завдань, які виникають в цих напрямках.
Вирішувачі, що використовують найбільш популярні останнім часом підходи, застосовують дискретний пошук, в той час як безперервні підходи в класичному SAT не знаходять широкого застосування. Однак безперервний підхід може дати вирішувачі більше інформації про досліджувану формулою. Метою даної роботи є створення підходу, що використовує досягнення сучасних алгоритмів і розширеного на використання безперервних моделей.
Завдання роботи:
1.Опісать існуючі методи і їх особливості;
2.Проаналізіровать можливість використання безперервних форм в цих методах;
.Разработать Розширений алгоритм, який використовує безперервні форми.
Робота вносить вклад в дослідження існуючих підходів і представляє вдосконалену версію алгоритму розв'язання задачі. Об'єктом вивчення є алгоритми вирішення проблеми булевої здійсненності, а предметом вивчення - цільові функції цих алгоритмів.
Робота розбита на кілька частин: спочатку наводиться загальна інформація про завдання здійсненності булевих формул, далі проводиться огляд існуючих методів вирішення. Ці методи проаналізовані з точки зору використання безперервних форм булевих змінних. Після цього представлені три безперервні моделі трансформації булевих операторів, а також модифікація алгоритму gNovelty +, яка використовує ці моделі.

1.Про завданню здійсненності булевих формул

У задачі про здійсненності дана булева формула?, Яка складається з N змінних x1, x2, ..., xn, операторів кон'юнкції (), диз'юнкції (і заперечення (), а також дужок. Завдання полягає в пошуку відповіді на питання, чи можна присвоїти такі значення змінним, щоб формула стала справжньою.

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

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

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

.1 Сімейство DPLL

Повні алгоритми, як правило, засновані на алгоритмі Девіса-Патнема-Логемана-Лавленд (DPLL). Цей алгоритм полягає в привласненні деякої змінної значення істина, спрощення формули і рекурсивної перевірки здійсненності спрощеної формули. На кожному кроці використовуються два правила:
· Виключення чистих литералов (pure literal elimination) - буквальний називається «чистим» якщо у формулі зустрічається або змінна, або її заперечення. У разі зустрічі чистого литерала можна привласнити значення таким чином, щоб виконати диз'юнкт, до складу яких він входить.
· Поширення змінної (Unit propagation або Boolean Constraint Propagation) - якщо у формулі зустрічається диз'юнкт з тільки одним літералом, то обов'язково потрібно присвоїти таке значення змінної, яке виконає цей диз'юнкт.
Після виконання цих правил може послідувати каскад спрощень, що робить DPLL набагато швидшим в порівнянні з простим перебором.
Формула вважається здійсненним, коли все диз'юнкт рівні істини, а нездійсненним - коли в процесі вирішення виникає порожній диз'юнкт, що означає, що всім ЛІТЕРАЛЬ в цій формулі були присвоєні такі значення, які не призводять до здійсненності цього диз'юнкт. Псевдокод алгоритму:
function DPLL (F): F здійсненна: SAT;
if F містить порожній диз'юнкт:
return UNSAT;
виключити чисті літерали;
поширити чисті змінні;
if зустрінутий конфлікт:
проаналізувати конфлікт;
додати вчинений диз'юнкт в F;
відкотити рішення до рівня конфлікту;
вибрати змінну x і значення для присвоєння;
return DPLL (F з присвоєним x);

На кожному кроці проводиться вибір «змінної розгалуження». Швидкість рішення залежить від цього вибору і різні вирішувачі використовують різні евристики для того, щоб вибрати змінну, яка призведе до найбільш ефективному вирішенню.
Подальшим розвитком алгоритму DPLL стало додавання навчання диз'юнкт, засноване на конфліктах (Conflict-Driven Clause Learning, CDCL). CDCL додає дві основні оптимізації:
· Нехронологічні відкат (non-chronological backtracking)
· Отримання і запам'ятовування диз'юнктів для запобігання повторення конфліктів
Ключовим етапом в алгоритмі є аналіз конфлікту. Конфлікт виникає тоді, коли необхідно привласнення змінної значень істина (1) і брехня (0) одночасно. Для аналізу будується граф імплікацій. У графі імплікацій з конфліктом присутній одночасно дві вершини для змінної, що містять привласнення протилежних значень.

Граф імплікацій показує, як присвоєння значень одних змінних призвело до зміни значень інших. Вершиною графа виступає привласнення значення змінної, назва вершини -x12 (7) означає, що змінної x12 був привласнений 0 на 7 рівні рішення. В даному випадку змінної розгалуження з'явилася x2, після чого стався каскад спрощень формули, яка призвела до конфлікту диз'юнкт і.
У графі вершина xa домінує над вершиною xb тоді, коли всі шляхи від змінної розгалуження на даному рівні рішення до xb проходять через xa. Точкою одиничної імплікації (Unique Implication Point, UIP) в графі імплікацій називається вершина, яка домінує над обома вершин, що відносяться до конфліктної змінної. Мінлива розгалуження завжди є точкою одиничної імплікації. Для аналізу конфлікту і створення диз'юнкт конфлікту використовується розбиття графа на дві частини: сторону конфлікту і сторону причини. Сторона причини включає в себе змінні розгалуження, а сторона конфлікту - конфліктні літерали. Далі знаходиться розріз графа по точці імплікації. Змінні, ребра від яких перетинають кордон, додаються в формулу як диз'юнкт конфлікту.

Різні схеми навчання використовують різні розрізи, наприклад, в схемі 1UIP використовується перша точка одиничної імплікації від конфлікту, в наведеному прикладі це -x4, і, таким чином, буде запомнен новий диз'юнкт. У схемі last-UIP буде використана остання точка одиничної імплікації, тобто змінна розгалуження, і доданим диз'юнкт конфлікту буде. 1UIP була знайдена найбільш ефективною завдяки тому, що запомненний диз'юнкт містить найбільш близьку до конфлікту інформацію (Zhang L. та ін. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. 2001).
Далі проводиться повернення решателя на попередній рівень рішення. У простих версіях DPLL вирішувач повертається на один рівень вгору, проте в CDCL повернення відбувається на максимальний рівень вирішення вище поточного в змінних, що входять в диз'юнкт конфлікту. В даному прикладі це 5 рівень, до якого належить присвоєння x9. Відкат на цей рівень змушує змінну поміняти своє значення і таким чином виконати диз'юнкт конфлікту.
Багато вирішувачі застосовують перезапуск рішення. Це допомагає уникнути витрати часу на частини простору рішень, в яких немає корисних результатів. Завдяки вченням диз'юнкт вирішувач не зустрічав такі ж конфлікти знову, тому перезапуски не шкодять процесу рішення навіть для нездійсненних формул.

.2 Сімейство WalkSAT

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

function GSAT (F): try = 0 to max_tries:
створити випадкове присвоєння змінних A;
for step = 0 to max_steps: A виконує F: SAT;
вибрати змінну x відповідно до цільової функцією;
звернути значення x; 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 вибирається друга за оцінкою змінна;
.Якщо І n = 1, вибирається друга за оцінкою змінна;
.Якщо І 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 з варіантом табу-пошуку. В алгоритмі G2WSAT 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_stepsA виконує F SAT;
else
з ймовірністю випадкового блукання wp
вибрати випадкову змінну x з невиконаного диз'юнкт;
else if існує перспективна змінна
жадібно вибрати перспективну змінну x, вибираючи давніше змінену, якщо оцінка однакова;
else
вибрати змінну x відповідно до зваженої евристикою AdaptNovelty;
збільшити вагу невиполенних диз'юнкт на 1;
з ймовірністю sp згладити вага всіх диз'юнкт;
звернути значення x в A;
return UNSAT;

Імовірність випадкового блукання контролює ступінь випадковості алгоритму, допомагаючи йому уникнути локальних мінімумів.
В якості цільової функції використовується зниження ваги невиконаних диз'юнкт. Перспективною змінної в даному випадку називається змінна, зміна якої веде до суворого зниження ваги.
У локальних мінімумах, якщо неможливо зробити крок з поліпшенням свідчення цільової функції використовується зважений алгоритм вибору змінної AdaptNovelty. Цей алгоритм вибирає випадкову диз'юнкт і вибирає кращу змінну (щодо цільової функції) і, якщо це не сама недавно змінена змінна, вибирає її для зміни. Якщо це сама недавно змінена змінна, то вона вибирається з ймовірністю 1-p, а з ймовірністю p вибирається друга найкраща змінна. Параметр шуму p при цьому адаптивно настроюється - якщо зроблені кроки не призводять до покращення значення цільової функції, то він збільшується, а якщо навпаки, то зменшується.

.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.

Важливою характеристикою моделей є той факт, що якщо вирішувач робить вибір тільки між двома значеннями - 0 і 1, вони ведуть себе аналогічно дискретного варіанту. Така поведінка гарантує, що застосування цих моделей до існуючих дискретним алгоритмам буде саме розширенням процесу рішення, а не його зміною.
Також всі моделі надають інформацію про те, чи виконується формула. Так як моделі ведуть себе так само, як і булеві оператори на дискретних значеннях, результат обчислення моделі на формулі F з присвоєнням X дає оцінку, наскільки здійсненна формула:
· При формула є невиконаною;
· При є шанс, що формула є виконаною;
· При формула виконується;
Варто зауважити, що значення, відмінне від нуля і менше одиниці саме по собі не гарантує, що формула здійсненна, наприклад, для очевидно нездійсненного випадку, з присвоєнням, значення S дорівнюватиме 0,25.
Розглянемо можливу зміну цільової функції. У WalkSAT в якості цільової функції використовується число невиконаних диз'юнкт. Можна уявити цю функцію у вигляді наступних формул для випадку з n змінних і m диз'юнктів:

Тут - вектор присвоєння змінних, а - оцінка для деякого диз'юнкт.
Для алгоритмів, що використовують зважену цільову функцію, таких як gNovelty +, в цільову функцію додається вектор ваг диз'юнктів і вона приймає наступний вигляд:

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

Відзначимо, що в цільової функції не використовується безперервна оцінка для всієї формули. Цю оцінку ми будемо використовувати як джерело додаткової інформації про формулу. Хоча, як було показано вище, оцінка не дозволяє визначити, чи здійсненна формула, її можна використовувати для того, щоб направити вирішувач в більш перспективні галузі вирішення. У розширеному алгоритмі, S використовується для того, щоб зробити вибір між змінними з однаковим значенням цільової функції. Якщо ж S для двох змінних збігаються, то використовується змінна, значення якої змінювалося давніше.
Псеводокод кроку отриманого алгоритму, gNovelty + c:

if оцінка формули дорівнює 1:
return SAT;
з ймовірністю випадкового блукання wp:
вибрати випадкову змінну x з невиконаного диз'юнкт;
виставити x в значення, яке виконує цей диз'юнкт; if існує перспективна змінна:
жадібно вибрати перспективну змінну x і її значення, між двох однакових вибираючи ту, у якій більш висока оцінка S, а при рівних S давніше змінену;
вибрати змінну x і її значення відповідно до зваженої евристикою AdaptNovelty з безперервною цільовою функцією;
збільшити вагу невиполенних диз'юнкт на 1;
з ймовірністю sp згладити вага всіх диз'юнкт;
виставити x в знайдене значення

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

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

Було з'ясовано, що оптимальним підходом є varprob. Хоча дана модель показує себе гірше, ніж varchoice на маленьких формулах, вона працює за кращий час на великих завданнях, що є несподіваним результатом, так як очікувалося, що varchoice буде найшвидшою моделлю через простоту реалізації. Швидше за все, оптимізовані арифметичні функції показують кращу продуктивність.
Модель vardiv є найповільнішої. Це не дивно з огляду на те, що її трансформація оператора є найскладнішою.

Табл. 1. Час рішення формул з використанням різних моделей
Число змінних: Число диз'юнкт: Час рішення (сек) varchoicevarprobvardiv5400.001030.001270.0015110600.0010.001100.00139201500.002110.002350.00361201500.002010.002330.00333503000.004970.004770.0072610010000.043020.037910.0486510015000.049210.043430.0727420030000.129280.109490.15982100080000.370230.369460.435682000100000.435790.402330.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.
. Glover F. Tabu Search-Part I // ORSA Journal on Computing, Т. 1, № 3, 1989. С. 190-206.
. 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.
. Gu J. Global Optimization for Satisfiability (SAT) Problem // IEEE Transactions on Knowledge and Data Engineering, Т. 6, № 3, Jun 1994. С. 361-381.
. Hoos H.H., Tompkins D.A.D. Novelty + and Adaptive Novelty + // SAT Competition. 2004.
. Hoos H.H. An adaptive noise mechanism for walkSAT // 18th National Conference on Artificial intelligence. 2002. С. 655-660.
. Hoos H.H. On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT // 16th National Conference on Artificial intelligence. 1999. С. 661-666.
. Huang J. The Effect of Restarts on the Efficiency of Clause Learning // International Joint Conference on Artificial Intelligence. Нью Йорк. 2007. С. 2318-2323.
. Johannsen J. The Complexity of Pure Literal Elimination // В кн .: SAT 2005 / ред. Giunchiglia E., Walsh T. Springer, 2005. С. 89-95.
. 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.
. Li C.M., Huang W.Q. Diversification and Determinism in Local Search for Satisfiability // 8th International Conference, SAT 2005. 2005. С. 158-172.
. 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.
. Marques-Silva J. Practical Applications of Boolean Satisfiability // 9th International Workshop on Discrete Event Systems. 2008. С. 74-80.
. McAllester D., Selman B., Kautz H. Evidence for Invariants in Local Search // 14th National Conference on Artificial Intelligence. 1997. С. 321-326.
. Moskewicz M.W., Zhao Y., Zhang L., Madigan C.F., Malik S. Chaff: Engineering an Efficient SAT Solver // 39th Design Automation Conference. Лас-Вегас. 2001.
. Pham D.N., Gretton C. gNovelty + // SAT Competition. 2007.
. 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.
. Schuurmans D., Southey F. Local search characteristics of incomplete SAT procedures // Artificial Intelligence, Т. 132, № 2, Nov 2001. С. 121-150.
. 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.
. Selman B., Kautz H.A., Cohen B. Noise strategies for improving local search // 11th National Conference on Artificial Intelligence. 1994. С. 337-343.
. Selman B., Levesque H., Mitchell D. A new method for solving hard satisfiability problems // 10th national conference on Artificial intelligence. 1992. С. 440-446.
. Sorensson N., Een N. MiniSat v1.13 - A SAT Solver with Conflict-Clause // MiniSat. 2005.
. Tichy R., Glase T. Clause Learning in SAT // Seminar Automatic Problem Solving. 2006.
. 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.
. Левін Л.А. Універсальні завдання перебору // Пробл. передачі інформ., Т. 9, № 3, 1973. С. 115-116.