Введем некоторые определения at() множество атомов в формуле

• Название: Введем некоторые определения at() множество атомов в формуле
• Дата: 06.11.2021
• Размер: 85.78 Kb.
• Имя файла: lecture_notes.pdf
• Тип: Документы; #264832

Введем некоторые определения:
• at(φ) - множество атомов в формуле φ
• at i
(φ)
- некоторый заданный порядок этих атомов
• Атом a сопоставим с булевой переменной e(a) (такую процедуру будем называть булевское кодирование)
• e(t) - булева формула, полученную булевым кодированием каждо- го атома формулы t (такую формулу будем называть пропозици- онным скилетом формулы t)
Рассмотрим следующий пример: φ := x = y ∨ x = z. Тогда at(φ) =
{at
1
, at
2
}
, at
1
:= x = y
, at
2
:= x = z
. Сопоставим x = y булеву перемен- ную e(x = y) = b
1
и x = z булеву переменную e(x = z) = b
2
. Получаем e(φ) = b
1
∨ b
2
Пусть α - некоторая (возможно, частичная) оценка формулы e(φ), напри- мер для формулы выше пусть α = {e(at
1
) → F ALSE, e(at
2
) → T RU E}
T h(at i
, α) =
(
at i
если α(at i
) = T RU E
¬at i
иначе
T h(α) = {T h(at i
, α)|e(at i
), α}
, T h(α) - конъюнкция всех элементов их
T h(α)
Пусть нам данн алгоритм (назовём его Deduction), который может ре- шить T h(α). Опишем алгоритм решение SMT-формул, имея Deduction:
• Вычислим B = e(φ)
• Отправим B SAT-решателю
• Если получили "UNSAT то возвращаем "UNSAT"
• Если получили "UNKNOWN то возвращаем "UNKNOWN"
• Если получили некоторую α, то вычисляем Deduction от T h(α)
• Если получили "SAT то возвращаем "SAT"
• Если получили "UNKNOWN то возвращаем "UNKNOWN"
• Если получили "UNSAT то B = B∧ "блокирующий дизюнкт"t и начинаем со второго пункта
1

Опишем подробнее свойства "блокирующего дизюнкта"(так же называ- ют леммой):
• t - тавтология в T
• t - состоит только из атомов из φ
• t - "блокирует"α, т.е. при отправлении B SAT-решателю мы не смо- жем снова получить α
Предположим, что в предыдущем примере оценка оказалась "UNSAT то- гда можно привести такой "блокирующий дизюнкт": t := e(at
1
) ∨ ¬e(at
2
)
(т.е. мы просто взяли дизъюнкцию отрицаний атомов). Есть и другие способы найти блокирующий дизюнкт, например, часто можно взять дизъюнкцию части отрицаний атомов, если они "UNSAT"в данной тео- рии.
Есть более эффективные алгоритмы решения SMT задач, но для это- го нам нужно изучить, как работает SAT решатель. В процессе работы ленивого алгоритма может возникнуть много блокирующих дизюнктов.
Многие теории можно свести к SAT задаче, но обычно существуют более эффективные алгоритмы решения теорий.
Решим с помощью SMT-решателя задачу с прошлой лекции: задача о расскарске графа. Имеется граф G = (V, E). Можно ли его вершини расскрасить в k цветов так, чтобы никакие соседние вершины не были раскрашены в один и тот же цвет? Постороим следующую систему урав- нений:
• x i
- целые
• 1 ≤ x i
≤ c
• x i
6= x j
для (x i
, x j
) ∈ E
Для решения такой системы нам понадобится SMT-решатель, умеющий разрешать теорию равенства.
В качестве упражнения предоставляются следующие задачи:
• Судоку (заполнить поле числами)
• Сапер (указать, на какую клетку можно "кликнуть")
2

В конце лекции разбрем следующую задачу - даны две программы, a и b:
Программа a:
int i, out_a = in;
for (int i = 0; i < 2; ++i) out_a = out_a * i;
return out_a;
Программа b:
int out_b = (in * in) * in;
return out_b;
Нужно проверить, являются ли они эквивалентными друг другу. Для этого построим формулы, описывающие связь между входом и выходом программ:
φ
a
:= (out
_a
0
= in
_a
0
) ∧ (out
_a
1
= out
_a
0
∗ in
_a
0
) ∧ (out
_a
2
= out
_a
1
∗
in
_a
0
)
φ
b
:= out
_b
0
= (in
_b
0
∗ in
_b
0
) ∗ in
_b
0
Чтобы программы были эквивалентны, должно выполняться:
(in
_a
0
= in
_b
0
) ∧ φ
a
∧ φ
b
→ out
_a
2
= out
_b
0
Проверку такой формулы на выполнимость может осуществить SMT- решатель, умеющий разрешать теорию равенства.
3