4488
правок
Irina (обсуждение | вклад) м (→Нотация) |
Irina (обсуждение | вклад) |
||
Строка 55: | Строка 55: | ||
== Основные результаты == | == Основные результаты == | ||
Алгоритм ResolveSat | Алгоритм '''ResolveSat''' | ||
Алгоритм ResolveSat по сути очень прост. Получив на вход формулу в k-КНФ, он вначале генерирует дизъюнкты, которые могут быть получены путем разложения, длина которых не превышает некоторой величины. Затем он устанавливает некоторый случайный порядок переменных и последовательно присваивает им значения согласно этому порядку. Если рассматриваемая в текущий момент переменная встречается в виде единичного дизъюнкта, ей присваивается единственное значение, при котором этот дизъюнкт выполним. Если она встречается в двух противоречащих друг другу единичных дизъюнктах, алгоритм начинает работу заново. На каждом этапе алгоритм также проверяет, выполнима ли формула. Если выполнима, то входной набор принимается. Процедура повторяется до тех пор, пока не будет найдено присваивание, приводящее к выполнимости формулы, либо пока не истечет выделенное время. | Алгоритм '''ResolveSat''' по сути очень прост. Получив на вход формулу в k-КНФ, он вначале генерирует дизъюнкты, которые могут быть получены путем разложения, длина которых не превышает некоторой величины. Затем он устанавливает некоторый случайный порядок переменных и последовательно присваивает им значения согласно этому порядку. Если рассматриваемая в текущий момент переменная встречается в виде единичного дизъюнкта, ей присваивается единственное значение, при котором этот дизъюнкт выполним. Если она встречается в двух противоречащих друг другу единичных дизъюнктах, алгоритм начинает работу заново. На каждом этапе алгоритм также проверяет, выполнима ли формула. Если выполнима, то входной набор принимается. Процедура повторяется до тех пор, пока не будет найдено присваивание, приводящее к выполнимости формулы, либо пока не истечет выделенное время. | ||
'''ResolveSat''' использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку <math>\pi \;</math> и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном <math>\pi \;</math>, и изменении их значений в попытке обеспечить выполнимость формулы F. | |||
Процедура '''Modify'''(КНФ-формула <math>G(x_1, x_2, ..., x_n) \;</math>, перестановка <math>\pi \;</math> = ({1, 2, ..., n}, присваивание y) <math>\to</math> (присваивание u) | |||
<math>G_0 = G</math>. | <math>G_0 = G</math>. |
правок