Содержание
Постановка задачи…………………………………………………..………….….3
1. Точный алгоритм.………………………………….……………….…………...4
2. Приближенный алгоритм………………………….…….…………………..…8
2.1 Алгоритм WalkSAT……………………………………………………...9
2.2 Алгоритм GSAT…………………………………………………………14
Выводы…………………………………………………………………………….15
Список литературы …………………………………………………..……...........16
Постановка задачи
В данной курсовой работе рассматривается задача о выполнимости. Целью курсовой работы является решение задачи полным методом, и не полным методом, также ее программная реализация на одном из языков программирования. Задача проектирования состоит в том, чтобы максимально просто добиться результата поставленной задачи.
Проблема выполнимости (ВЫП или SAT) – для данной булевой формулы определить, существует ли набор, на котором она обращается в единицу. Такой набор называется выполняющим. Если она существует, то формула называется выполнимой.
Дальше проблема выполнимости будет рассматриваться только для формул специального вида: конъюнктивных нормальных форм (КНФ).
Вообще, если говорить о терминологии, то в современной литературе выделяют более широкую проблему: CSP (Constraint Satisfaction Problem) – выполнимость при ограничениях (могут ли выполняться одновременно ограничения, накладываемые на переменные). Однако, именно задача выполнимости является центральной в этой проблеме, кроме того имеет много хорошо разработанных и исследованных методов решения (достаточно общих и специализированных).
Проблема выполнимости является NP-полной, потому не существует полиномиального алгоритма для её решения. Тем не менее, существует достаточно много алгоритмов для решения проблемы выполнимости за приемлемое время на реальных данных.
Современные программные реализации алгоритмов, предназначенные для решения прикладных задач и оценки эффективности алгоритмов путём сравнения с другими программами (SAT-солверы) могут определять выполнимость КНФ от 1000 переменных за несколько минут. КНФ, выполнимость которых надо определять на практике (их часто называют индустриальными: industrial) имеют специальный вид. Случайные КНФ (сгенерированные с помощью специальных программ, использующих датчики псевдослучайных чисел) имеют более сложную структуру. Для них проблема выполнимости для КНФ, в каждой скобке которых содержится не более трёх литералов (3SAT-проблема) не удаётся решить при числе переменных более 700.
ТочНый Алгоритм
Алгоритмы, которые выполняют полный перебор. Как правило, базируются
на DPLL-методе. Часто выделяют две основные категории полных алгоритмов:
- Алгоритмы, основанные на резолюциях.
- Алгоритмы, основанные на «переборе дерева».
Заметим, что именно доказательство невыполнимости (не всегда это доказательство эффективно представляется в аналитическом виде), которое осуществляют полные алгоритмы, имеет важное прикладное значение при автоматическом доказательстве теорем в ИИ (automated theorem proving) и верификации схем (circuit verification).
Дэвис (Davis) и Путнэм (Putnam) предложили алгоритм для решения проблемы выполнимости в 1960 году.. Однако у него имелся существенный недостаток: переполнение памяти. Модифицированная версия Дэвиса, Логемана (Logemann) и Ловелэнда (Loveland) появилась в 1962 году. В этой версии вместо резолюций использовался поиск. Этот алгоритм часто называют DLL или DPLL, а первый – DP. Подробнее о резолюциях и поиске будет сказано ниже. Заметим, что несмотря на недостатки резолюционных алгоритмов как таковых, минимальные резолюционные решения проблемы экспоненциально короче DPLL-решений.
Часто солверы, в которых реализован алгоритм DPLL, делят на две группы:
- Conflict-driven (minisat, vallst, zChaff).
- Look-ahead (kcnfs, march, OKsolver).
Отметим, что солверы, основанные на локальном поиске, показывают хорошие результаты на случайных выполнимых 3-КНФ. Conict-driven-солверы – на индустриальных КНФ. Look-ahead-солверы – на невыполнимых КНФ. Переборные алгоритмы, основанные на других идеях, значительно уступают этим.
Описание DPLL
1. Применить юнит-резолюцию и удалить все поглощаемые клаузы (BCP).
2. Если найдена пустая клауза, то вернуть НЕВЫПОЛНИМА.
3. Найти переменную, которая входит в КНФ только с отрицанием или без
отрицания.
4. Удалить все клаузы, в которые входит эта переменная (удаление чистых
литералов).
5. Если нет клауз, то вернуть ВЫПОЛНИМА.
6. Выбрать переменную x (она входит как с отрицанием, так и без).
7. Рекурсивно вызвать DPLL на текущей КНФ с добавленной клаузой (x).
8. Рекурсивно вызвать DPLL на текущей КНФ с добавленной клаузой (! x).
9. Если один из рекурсивных вызовов вернул ВЫПОЛНИМА, то вернуть
ВЫПОЛНИМА.
10.Вернуть НЕВЫПОЛНИМА.
Реализация:
public static class DPLL
{
public static bool Solve(Expression e)
{
if (IsSat(e))
{
return true;
}
if (ContainEmptyDisunkt(e))
return false;
List<List<ILiteral>> oneLitDis = OneLitDis(e);
foreach (var dis in oneLitDis)
{
e = UnitPropagade(e, dis);
}
Literal l = ChooseLiteral(e);
if (l == null)
{
return IsSat(e);
}
return Solve(e.Add(l)) || Solve(e.Add(Not(l)));
}
Тест:
В качестве примера возьмем выражение (x V y) ^ z, которое является выполнимым и выражение (a) ^ (!a), которое не выполнимо.
Результаты:
Исследование T(n)
| N | DPLL | ||
| 0,002 | |||
| 0,000667 | |||
| 0,0156 | |||
| 0,0052 | |||
| 1,48 | 1,43 | 1,41 | |
| 1,44 | |||
| 31,54 | 31,43 | 31,46 | |
| 31,48 | |||
| 116,132 | 115,84 | 115,68 | |
| 115,88 | |||
| >1800 | >1800 | >1800 | |
T(max) = 1800, при N=30.
ПРИБЛИЖЕННЫЙ АЛГОРИТМ.
Алгоритмы, которые осуществляют поиск выполняющего набора неполным
перебором пространства возможных решений. Как правило, используют локальный поиск (local search) для нахождения решения. Если алгоритм не находит решения, то это не означает, что его не существует. Таким образом, неполные алгоритмы могут доказать только выполнимость (и то не всегда) и не могут доказать невыполнимость. В последнее время разрабатывают также полные алгоритмы, основанные на локальном поиске (точнее: алгоритмы, доказывающие невыполнимость). Часто для этих алгоритмов исходная задача записывается в других терминах («переформулируется»). При этом основная проблема – компактная запись новой переформулированной задачи. Подобные алгоритмы пока применимы только для «очень маленьких» задач. Основное достоинство такихалгоритмов – быстрая скорость работы.
GSAT стал первым солвером, основанном на стохастическом локальном поиске (Stochastic Local Search), который решал сложные задачи с большим числом
переменных и клауз.
Дальше появился WalkSAT предложенный МакАлесторомо, Селманомом и Каутсомом в 1997 году. Отличие от GSAT в выборе переменной. В WalkSAT рейтинг переменной равен числу клауз, которые перестанут быть выполнимы при её изменении. Если текущий набор не является искомым, выбирается невыполнимая клауза (случайно). Меняется значение одной из её переменных с
учётом рейтинга (например, если в ней есть переменная с нулевым рейтингом,
то меняется её значение).
В настоящее время существует множество модернизаций этих алгоритмов.
Основная их цель – избежать «застревания» алгоритма в локальных минимумах функционала качества решения. Его можно определить как число невыполненных клауз на данном наборе.
Основная причина – их эвристическая природа, подробное описание в литературе по смежным областям, отсутствие «универсальных подходов». Это «очень знакомые методы»: метод отжига, метод случайных блужданий, генетические алгоритмы и т.д.
Основное достоинство неполных методов – их приложение и к другим задачам, тесно связанным с SAT. Например, MAXSAT (найти набор, который выполняет максимальное число клауз в заданной КНФ). Вообще, почти все эти методы пытаются минимизировать некоторый функционал (часто даже не учитывая его структуру).
WalkSAT
Реализация:
public static bool Solve(Expression e, int MaxTries,int MaxFlips)
{
for (int i = 0; i < MaxTries; i++)
{
SetRandomValues(e);
for (int flip = 0; flip < MaxFlips; flip++)
{
List<Literal> c = RandomUnsatClause(e);
Literal l = GetRandomLiteral(c);
if (l!= null)
{
Flip(l);
}
if (IsSat(e))
return true;
}
}
return false;
}
Где MaxTries – максимальное количество подграфов, MaxFlips – максимальное количество изменяемых литералов.
Тест:
В качестве примера возьмем выражение (x V y) ^ z, которое является выполнимым и выражение (a) ^ (!a), которое не выполнимо.
Результаты:
Исследование T(n).
| T(с) | ||||||
| N | DPLL | WalkSAT | ||||
| 0,002 | 0,002 | |||||
| 0,000667 | 0,000667 | |||||
| 0,0156 | 0,0156 | |||||
| 0,0052 | 0,0052 | |||||
| 1,48 | 1,43 | 1,41 | 0,046 | |||
| 1,44 | 0,0156 | |||||
| 31,54 | 31,43 | 31,46 | 0,08 | |||
| 31,48 | 0,026 | |||||
| 116,132 | 115,84 | 115,68 | 0,06 | 0,047 | 0,036 | |
| 115,88 | 0,048 | |||||
| >1800 | >1800 | >1800 | 0,42 | 0,36 | 0,6 | |
| 0,46 | ||||||
| 0,97 | 0,8 | 0,96 | ||||
| 0,91 | ||||||
| 4,95 | 4,97 | 4,93 | ||||
| 4,95 | ||||||
| >1800 | ||||||
T(max) = 1800, max = 1000.
СРАВНЕНИЕ.
| T(с) | Результат | |||||||
| N | DPLL | WalkSAT | DPLL | WalkSAT | ||||
| 0,002 | 0,002 | True | True | |||||
| 0,000667 | 0,000667 | |||||||
| 0,0156 | 0,0156 | True | True | |||||
| 0,0052 | 0,0052 | |||||||
| 1,48 | 1,43 | 1,41 | 0,046 | True | True | |||
| 1,44 | 0,0156 | |||||||
| 31,54 | 31,43 | 31,46 | 0,08 | True | True | |||
| 31,48 | 0,026 | |||||||
| 116,132 | 115,84 | 115,68 | 0,06 | 0,047 | 0,036 | True | False | |
| 115,88 | 0,048 | |||||||
| >1800 | >1800 | >1800 | 0,42 | 0,36 | 0,6 | True | False | |
| 0,46 | ||||||||
| 0,97 | 0,8 | 0,96 | False | |||||
| 0,91 | ||||||||
| 4,95 | 4,97 | 4,93 | False | |||||
| 4,95 | ||||||||
| False | ||||||||
| >1800 | False | |||||||
По результатам тестов видно, что алгоритм DPLL выполняется за не полиномиальное время. Алгоритм WalkSAT в наилучшем случае выполнялся за линейное время, в наихудшем же случае время равно n4.
Точность решения для разных N
ε=100l(St - Sp)l/St
| Точность решения | |
Время решения для разных N
ε=100l(Tt - Tp)l/Tt
| Время решения | |
| 98,91667 | |
| 99,91741 | |
| 99,95858 | |
| 99,97444 |
Скриншоты программы.
Алгоритм GSAT
Алгоритм работает на внутренних формулах. Он начинает задавать случайно подобранные значения ко всем переменным. Если значение удовлетворяет все, то алгоритм останавливается и возвращает значение. В противном случае, значение переменной изменяется, и процесс повторяется. Переменную, которую нужно изменить одним уменьшает число неудовлетворенных клаузул в новом назначении в GSAT. Если никакое назначение не было найдено правильно, то после установки количества итерирований, то алгоритм начинается снова с новым случайным значением. Алгоритм прекращается тогда, когда была найдена модель формулы или когда число рестартов превышает установленное количество (например, 10).
Реализация:
public static class GSat
{
public static bool Solve(Expression e, int MaxTries, int MaxFlips)
{
for (int i = 0; i < MaxTries; i++)
{
SetRandomValues(e);
for (int flip = 0; flip < MaxFlips; flip++)
{
List<Literal> c = RandomUnsatClause(e);
Literal l = GetLiteralGreedily(e, c);
if (l!= null)
{
Flip(l);
}
if (IsSat(e))
return true;
}
}
return false;
}
private static void Flip(Literal l)
{
l.Value =!l.Value;
}
private static List<Literal> RandomUnsatClause(Expression e)
{
List<List<Literal>> clauses = new List<List<Literal>>();
foreach (var clause in e.Clauses)
{
bool temp = false;
foreach (var lit in clause)
{
temp = temp || (lit.Not)?!lit.Value.Value: lit.Value.Value;
}
if (!temp)
clauses.Add(clause);
}
if (clauses.Count > 0)
return clauses[(new Random()).Next(clauses.Count)];
else
return null;
}
private static void SetRandomValues(Expression e)
{
Random r = new Random();
foreach (var l in e.Literals)
{
if (e.Literals.Where(lit => lit.Name == l.Name).Count() == 1)
l.Value = r.NextDouble() > 0.5;
else
{
bool value = r.NextDouble() > 0.5;
foreach (var literal in e.Literals.Where(lit => lit.Name == l.Name))
{
literal.Value = value;
}
}
}
}
private static Literal GetLiteralGreedily(Expression e, List<Literal> clause)
{
Dictionary<int, Literal> raitingLiteral = new Dictionary<int, Literal>();
foreach (var literal in clause)
{
int currentNumberUnsatClauses = CountUnsatClauses(e);
Flip(literal);
int flippedNumber = CountUnsatClauses(e);
if (flippedNumber < currentNumberUnsatClauses)
try
{
raitingLiteral.Add(currentNumberUnsatClauses - flippedNumber, literal);
}
catch { }
Flip(literal);
}
if (raitingLiteral.Count > 0)
{
int maxScore = raitingLiteral.Keys.Max();
return raitingLiteral[maxScore];
}
return null;
}
private static int CountUnsatClauses(Expression e)
{
List<List<Literal>> clauses = new List<List<Literal>>();
foreach (var clause in e.Clauses)
{
bool temp = false;
foreach (var lit in clause)
{
temp = temp || (lit.Not)?!lit.Value.Value: lit.Value.Value;
}
if (!temp)
clauses.Add(clause);
}
return clauses.Count;
}
private static bool IsSat(Expression e)
{
List<bool> temp = new List<bool>();
temp.Add(true);
foreach (var list in e.Clauses)
{
foreach (Literal l in e.Literals)
{
if (l.Value == null)
return false;
}
bool result = list[0].Not?!list[0].Value.Value: list[0].Value.Value;
for (int i = 1; i < list.Count; i++)
{
bool intermed = list[i].Not?!list[i].Value.Value: list[i].Value.Value;
result = result || intermed;
}
temp.Add(result);
}
bool res = temp[0];
for (int i = 1; i < temp.Count; i++)
res = res && temp[i];
return res;
}
}
Тест:
Для наглядного примера возьмем простое выражение (а) ^ (a), которое является выполнимым и выражение (a) ^ (!a), которое является не выполнимым.
Результаты:
Исследование T(n).
| T(n) | ||||||
| N | DPLL | GSAT | ||||
| 190010,6667 | 156675,3333 | |||||
| 170009,6667 | ||||||
| 486691,3333 | ||||||
| 1336860,333 | ||||||
| 316371,6667 | ||||||
| 8627163,667 | ||||||
| 773503,3333 | ||||||
| 1246732,333 | ||||||
| 2056784,333 |
T(max) = 2056784,333, max = 1000.
СРАВНЕНИЕ.
| T(n) | Результаты | |||||||
| N | DPLL | GSAT | DPLL | GSAT | ||||
| True | True | |||||||
| 190010,6667 | 156675,3333 | |||||||
| True | True | |||||||
| 170009,6667 | ||||||||
| False | True | |||||||
| 486691,3333 | ||||||||
| False | True | |||||||
| 1336860,333 | ||||||||
| False | True | |||||||
| 316371,6667 | ||||||||
| False | True | |||||||
| 8627163,667 | ||||||||
| False | True | |||||||
| False | True | |||||||
| 773503,3333 | ||||||||
| False | True | |||||||
| 1246732,333 | ||||||||
| False | True | |||||||
| 2056784,333 |
По результатам тестов видно, что алгоритм DPLL выполняется за не полиномиальное время. Алгоритм GSAT в наилучшем случае выполнялся за линейное время, в наихудшем же случае время равно n3.
Точность решения для разных N
ε=100l(St - Sp)l/St
| Точность решения | |
