Ивановский Дмитрий | МФТИ, сложность вычислений | 2014
Задача SAT представляет собой наглядный пример задачи, которая очень легко формулируется, но в то же время не имеет простого решения. В [1] доказано, что задача SAT или ВЫПОЛНИМОСТЬ записанная в конъюнктивной нормальной форме является NP-полной. Но в тоже время задача SAT имеет большое практическое применение, из-за своей простой структуры эта задача часто применяется для доказательства результатов об NP-полноте. Так например существует SAT@home — российский проект добровольных распределенных вычислений. Научной целью проекта является решение задач дискретной математики путем сведения их к задаче о выполнимости булевых формул. Быстрые алгоритмы позволяющие решать задачу SAT являются стратегическим преимуществом.
В работе мы рассмотрим один из самых простых вероятностных алгоритмов решения задачи 3-SAT, но тем не менее этот алгоритм является одним из самых быстрых. Реализация алгоритма будет представлена на языке python2, в работе будет интерактивная вставка, позволяющая проверить корректность работы алгоритма на собственных тестах.
В общем виде задача выполнимости ставится так. Нам дана булева формула, стостоящая из скобок, $ \And, \wedge, x_1 ... x_n $ и $ \bar{x_1} ... \bar{x_n} $ Необходимо ответить, существует ли такой набор значений переменных(выполняющий набор) $ x = x_1 ... x_n \in \{0, 1\}^n $, что формула $ \varphi(x) $ принимает истинное значение. Мы ограничимся рассмотрением только формул записанных в конъюнктивной нормальной форме внутри каждой скобки которых не более 3-х переменных или их отрицаний.
$$ \varphi(x) = \prod \limits_{t=1}^N (x_i \vee \bar{x_j} \vee x_k) $$Мы будем использовать вероятностный алгоритм, который будет всегда решать задачу 3-SAT правильно, если формула не имеет выполняющего набора. И ошибаться с некоторой контролируемой вероятностью, если формула имеет выполняющий набор. Контроль вероятности ошибки осуществляется путем выполнения независимых повторений проверки $ \varphi(x) $ на некоторые условия.
На каждой итерации мы будем проверять $ \varphi(x) $ на выполнимость на фиксированном наборе значений $ x_1 .. x_n $. Обозначим вероятность того, что случайный набор $ x_1 ... x_n $ окажется для $ \varphi(x) $ выполняющим за $ p $. Тогда вероятность того, что мы после $ t $ шагов всё еще не найдём выполняющий набор равна
$ (1-p)^t \le e^{-pt} $
тогда, если приемлимой вероятностью ошибки мы считаем $ e^{-20} \approx 2 \times 10^{-9} $, то достаточно сделать $ t = \frac{20}{p} $ итераций.
Тем не менее обычно в вероятностных алгоритмах количество итераций ограничивают математическим ожиданием количества итераций, необходимых для нахождения решения. Можно считать, что все итерации независимы поэтому примем $ t = \frac{1}{p} $, для справки математическое ожидание геометрического распределения
Забегая вперёд скажем, что наш алгоритм гарантирует, что $ p \ge (\frac{3}{4})^n $ и каждая итерация работает за $ O(n) $, где $ n $ - это длина входа алгоритма, поэтому $ t = (\frac{4}{3})^n $ и общая сложность $ O((\frac{4}{3})^n \times n) = O(2^{0.415 \times n} \times n)$.
Для сравнения, один из лучших алгоритмов решения проблемы 3-SAT PPSZ работает за $ O(2^{0.386 \times n}) $ [2]
$ n $ | $ (\frac{4}{3})^n \times n $ | $ 2^{0.386 \times n} $ |
---|---|---|
10 | 178 | 15 |
50 | 88,289,049 | 645,475 |
100 | 311,798,241,020,793 | 416,636,997,323 |
Опишем на псевдокоде итерацию алгоритма:
"""
# input - формула в 3-КНФ с n переменными
Решить_КНФ_задачу(input):
x = Сгенирировать_случайный_набор(n)
Повторить 3*n раз:
Если набор выполняющий:
Напечатать x
Вернуть True
Пусть в формуле есть скобка, которая равна False:
Меняем значение случайной переменной в x, входящей в эту скобку
Вернуть False
"""
Эту функцию мы вызовем $ t $ раз, если она хоть раз вернет $ True $ выполнение завершится. Иначе мы скажем, что выполняющего набора не существует
Оценим вероятность $ p $, того что функция Решить_КНФ_задачу вернет $ True $
Предположим, что существует выполняющий набор $ x^{*} $ размера $ n $, зафиксируем его.
Функция Сгенирировать_случайный_набор возвращает $ x $. Введём случайную величину $ \xi $, равную количеству бит в которых $ x $ и $ x^* $ отличаются. В литературе для этой величины часто используют термин расстояние Хэмминга.
$ P(\xi = j) = {\Large \frac{C^j_n}{2^n} }$ для $ j = 0,1,...,n $
После того, как определено $ j $, то есть начальное расстояние Хэмминга, и оно не равно нулю, мы можем считать, что каждая итерация цикла изменяет один бит в наборе $ x $. В каждой скобке 3 переменных, и одна из них принимает неверное значение, так как скобка ложна, то $ P($мы поменяли бит на правильный$) \ge \frac{1}{3} $. Значит наш цикл эквивалентен случайному блужданию на прямой из точки $ j $, где $P($пойти налево$) \ge \frac{1}{3}$. При этом, если мы достигаем точку 0, то цикл завершается, значит нас интересуют только блуждания выше нуля, которые только на последнем шаге принимают значение 0.
Количество таких путей и вероятность такого блуждания - это классическая задача из теории веройтностей и может быть решена методом отражений.
Если обозначить за $ i $ количество шагов вправо, то вероятность такого блуждания не меньше чем
$$ q_j = \sum \limits_{i=0}^j C_{j+2i}^i \times \frac{j}{j+2i} \times (\frac{2}{3})^i \times (\frac{1}{3})^{i+j} \ge \frac{1}{3} \times \sum \limits_{i=0}^j C_{j+2i}^i \times (\frac{2}{3})^i \times (\frac{1}{3})^{i+j} $$Воспользуемся асиптотикой количества сочетаний $ C_n^{\alpha n} \sim ((\frac{1}{\alpha})^{\alpha} \times (\frac{1}{1-\alpha})^{1-\alpha})^n $
$$ n = j + 2i, i = j, \alpha = \frac{1}{3}, C_{3j}^j \sim (\frac{27}{4})^j $$$$ q_j \ge \frac{1}{3} \times \sum \limits_{i=0}^j C_{j+2i}^i \times (\frac{2}{3})^i \times (\frac{1}{3})^{i+j} \ge (\frac{27}{4})^j \times (\frac{2}{3})^j \times (\frac{1}{3})^{2j} = (\frac{1}{2})^j $$Тогда по формуле полной вероятности и биному Ньютона
$$ p \ge (\frac{1}{2})^n \times \sum_{j=0}^{n} C_n^j \times (\frac{1}{2})^j = (\frac{1}{2} \times (1 + \frac{1}{2}))^n = (\frac{3}{4})^n $$Ниже приводиться реализация описанного выше алгоритма на языке python2.
Опишем формат входных данных.
Чтобы в качестве входных данных ввести $ (x_1 \vee \bar{x_2} \vee x_3) \wedge (\bar{x_2} \vee x_3 \vee \bar{x_4}) $, нужно писать $ (1+2'+3)*(2'+3+4') $ без пробелов и других лишних символов. Так же следует следить за корректностью ввода формулы.
То есть переменные заменяются своим номером, отрицание обозначается штрихом справа от номера, конъюнкция и дизъюнкция заменены на умножение и сложение соответственно.
Результат работы алгоритма следует интерпретировать так:
Если ответ это список типа $ [False, True, ...] $, значит $ x_1 = False, x_2 = True, ... $
Если ответ это $ \text{"There is no good assigment"} $, значит выполняющего набора нет
from random import randint
def isGoodAssignment(x, sat):
"""
x = [True, False, True, ...] is mean x1 == True, x2 == False, x3 == True, ...
Check on True SAT on assigment x
If SAT is True return (True, -1)
else return (False, number error clause)
"""
for i, clause in enumerate(sat):
resClause = False
for var in clause:
resClause = resClause or (x[var[0]] == var[1])
if resClause:
break
if not resClause:
return (False, i)
return (True, -1)
def get_SAT_struct(seq):
"""
return SAT struct is list of list of pair
[[(1, False), (2, True), (4, False)], [...], ...] is mean
(1' + 2 + 4') * (...) * ...
"""
numberClause = 0
maxVar = -1
sat_struct = []
for clause in seq.split('*'):
sat_struct.append([])
cl = clause[1:-1] # clause without brackets
for literal in cl.split('+'):
if literal[-1] == "'":
num = int(literal[:-1]) - 1 # numerate from 0 in memory
sat_struct[numberClause].append([num, False])
else:
num = int(literal) - 1 # numerate from 0 in memory
sat_struct[numberClause].append([num, True])
maxVar = max(maxVar, num)
numberClause += 1
return sat_struct, maxVar + 1
def generateRandomAssigment(numberVar):
return [bool(randint(0,1)) for i in range(numberVar)]
def flipRandomVar(sat, numErrorClause, x):
i = randint(0, len(sat[numErrorClause]) - 1)
var = sat[numErrorClause][i][0]
x[var] = not x[var]
def oneStep(sat, numberVar):
for i in range(numberVar * 3):
x = generateRandomAssigment(numberVar)
isGood, numErrorClause = isGoodAssignment(x, sat)
if isGood:
print x
return True
else:
flipRandomVar(sat, numErrorClause, x)
return False
def solve_SAT_problem(seq="(1+2)*(1'+2')*(1'+2)*(1+2')"):
"""
k = 3, 3-SAT
p = (0.5 * (1 + 1/(k-1))) ** n = (0.75)**n
If we accept probability error exp(-20)
We need do 20/p operations oneStep
"""
sat, numberVar = get_SAT_struct(seq)
error = 20 # mean real error is exp(-error)
t = int(error/((0.75)**numberVar))
for i in range(t):
if oneStep(sat, numberVar):
return
print "There is no good assigment"
solve_SAT_problem()
solve_SAT_problem("(1+2)")
[False, True]
solve_SAT_problem("(1+2)*(1'+2)*(1+2')*(1'+2')")
There is no good assigment
solve_SAT_problem("(1+2+3)*(1'+2'+3)*(2+3'+5)*(2'+3+4')")
[False, False, True, True, True]
Ниже приводится тот же самый алгоритм, но благодаря технологии Skulpt его можно тестировать прямо в браузере при просмотре. Скорость выполнения зависит только от мощности устройства, с которого производится запуск.
Напомним, что алгоритм вероятностный и вероятность его ошибки ненулевая, поэтому не стоит удивляться отсутствию выполняющего набора на выполнимых формулах. Однако вероятность такого события настолько мала, что если вам посчастливиться найти формулу на которой алгоритм работает неверно и дожить до завершения его работы, обязательно свяжитесь с автором ivanovskiy.dmitriy@gmail.com
from IPython.display import HTML
javascript = """
<script src="js/skulpt.min.js" type="text/javascript"></script>
<script src="js/skulpt-stdlib.js" type="text/javascript"></script>
<script type="text/javascript">
function outf(text) {
var mypre = document.getElementById("output");
mypre.innerHTML = mypre.innerHTML + text;
}
function builtinRead(x) {
if (Sk.builtinFiles === undefined || Sk.builtinFiles["files"][x] === undefined)
throw "File not found: '" + x + "'";
return Sk.builtinFiles["files"][x];
}
function runit() {
var prog = document.getElementById("yourcode").innerHTML;
var input = document.getElementById("code_input").value;
prog = prog.split("input_data_js").join(input);
var mypre = document.getElementById("output");
mypre.innerHTML = '';
Sk.canvas = "mycanvas";
Sk.pre = "output";
Sk.configure({output:outf, read:builtinRead});
try {
eval(Sk.importMainWithBody("<stdin>", false, prog));
}
catch(e) {
outf(e.toString())
}
}
</script>
"""
input_form = """
<form>
<textarea style="display:none;" id="yourcode">
from random import randint
def isGoodAssignment(x, sat):
for i, clause in enumerate(sat):
resClause = False
for var in clause:
resClause = resClause or (x[var[0]] == var[1])
if resClause:
break
if not resClause:
return (False, i)
return (True, -1)
def get_SAT_struct(seq):
numberClause = 0
maxVar = -1
sat_struct = []
for clause in seq.split('*'):
sat_struct.append([])
cl = clause[1:-1] # clause without brackets
for literal in cl.split('+'):
if literal[-1] == "'":
num = int(literal[:-1]) - 1 # numerate from 0 in memory
sat_struct[numberClause].append([num, False])
else:
num = int(literal) - 1 # numerate from 0 in memory
sat_struct[numberClause].append([num, True])
maxVar = max(maxVar, num)
numberClause += 1
return sat_struct, maxVar + 1
def generateRandomAssigment(numberVar):
return [bool(randint(0,1)) for i in range(numberVar)]
def flipRandomVar(sat, numErrorClause, x):
i = randint(0, len(sat[numErrorClause]) - 1)
var = sat[numErrorClause][i][0]
x[var] = not x[var]
def oneStep(sat, numberVar):
for i in range(numberVar * 3):
x = generateRandomAssigment(numberVar)
isGood, numErrorClause = isGoodAssignment(x, sat)
if isGood:
print x
return True
else:
flipRandomVar(sat, numErrorClause, x)
return False
def solve_SAT_problem(seq="(1+2)*(1'+2')*(1'+2)*(1+2')"):
sat, numberVar = get_SAT_struct(seq)
error = 20 # mean real error is exp(-error)
t = int(error/((0.75)**numberVar))
for i in range(t):
if oneStep(sat, numberVar):
return
print "There is no good assigment"
solve_SAT_problem("input_data_js")
</textarea>
<table style="border:0px"><tr style="border:0px">
<td style="border:0px">CalcSome(<input type="text" id="code_input" size="50" height="2" value="(1+2)*(1+2')">) == </td>
<td style="border:0px"> <pre id="output" ></pre></td>
</tr></table>
<button type="button" onclick="runit()">Run</button>
</form>
"""
HTML(input_form + javascript)
[1] "Вычислительные машины и труднорешаемые задачи", М.Гэри, Д.Джонсон
[2] "An improved exponential-time algorithm for k-SAT", Paturi, Pudlak, Saks, Zani
[3] "Engineering an Efficient SAT Solver", Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S.
[4] "A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems", Schöning, Uwe