SAT-решатель: распространение единиц и ветвление

Если ты объяснишь распространение единиц, запишешь раскраску графа в КНФ (хотя бы один цвет, не больше одного, у соседей разные) и знаешь, где у случайного 3-SAT самые трудные формулы, листай до «Теперь сам».

Как думаешь, когда перебор узнает о тупике

Формула из скобок по три литерала, переменных восемь. Перебор с возвратом ставит значения по очереди: x₁ = истина, x₂ = истина, … и после каждого шага проверяет, не стала ли какая-нибудь скобка ложной целиком. Скобка (x₁ ∨ ¬x₅ ∨ x₇) станет ложной, только когда все три её переменные уже получат значения.

Ответь себе до чтения: что можно понять раньше? Пусть x₁ ложна и x₅ истинна. Скобка ещё не ложна - x₇ свободна. Но выбора у x₇ уже нет: если поставить её ложной, скобка погибнет. Перебор этого не знает и честно попробует оба значения. Решатель знает и ставит x₇ = истина сразу.

На что это похоже

Судоку. Новичок ставит в клетку цифру наугад и смотрит, не сломалось ли что-нибудь. Опытный сначала ищет клетки, где возможна единственная цифра, ставит их - и от этого в соседних клетках тоже остаётся по одной возможности. Цепочка вынужденных ходов иногда решает всю головоломку без единой догадки, а если нет - догадка нужна в одной-двух клетках, а не в каждой.

Распространение единиц - это и есть «единственная возможная цифра», только для скобок формулы.

Механизм: DPLL

Формула в КНФ (из раздела о сложности): скобки соединены «и», внутри скобки литералы соединены «или», литерал - переменная или её отрицание. Запись числами: 3 - это x₃, −3 - это ¬x₃.

DPLL(значения):
    распространить единицы:
        пока есть скобка, где все литералы ложны,
        кроме одного свободного, - сделать его истинным
        если какая-то скобка ложна целиком - вернуть «тупик»
    если свободных переменных нет - вернуть «выполнимо»
    взять свободную переменную v
    попробовать v = истина; если тупик - попробовать v = ложь

Алгоритм назван по авторам - Дэвис, Патнэм, Логеман, Лавленд, 1960-1962. Перебор с возвратом из раздела о переборе плюс одно правило, но правило меняет всё: каждое ветвление тянет за собой цепочку вынужденных значений, и тупик обнаруживается на несколько уровней раньше.

Кодирование задач. Решатель ничего не знает о графах и расписаниях - ему нужна КНФ. Раскраска графа в три цвета: переменная x(v, c) - «вершина v покрашена в цвет c». Три вида скобок:

хотя бы один цвет у вершины v    ( x(v,1) ∨ x(v,2) ∨ x(v,3) )
не больше одного цвета           (¬x(v,1) ∨ ¬x(v,2)),
                                 (¬x(v,1) ∨ ¬x(v,3)),
                                 (¬x(v,2) ∨ ¬x(v,3))
у соседей u, v разные цвета      (¬x(u,c) ∨ ¬x(v,c)) для каждого c

На каждую вершину четыре скобки, на каждое ребро - три.

Правило

DPLL - перебор с возвратом по переменным КНФ, где после каждого выбора распространяются единицы: скобка с единственным свободным литералом и остальными ложными делает этот литерал истинным, скобка со всеми ложными - тупик. Чтобы решить задачу решателем, её кодируют в КНФ: переменные «объект в состоянии», скобки «хотя бы один», «не больше одного», запреты.

Разбор: единицы против голого перебора

sluchajnaya_formula строит случайную формулу с тремя литералами в скобке; скобок 4,3 · n - около этого отношения случайные формулы самые трудные. dpll с флагом s_edinicami = False - перебор с возвратом, который замечает только целиком ложные скобки; с True - настоящий DPLL.

import random

def sluchajnaya_formula(n, m, zerno):
    random.seed(zerno)
    skobki = []
    for i in range(m):
        skobka = []
        while len(skobka) < 3:
            v = random.randint(1, n)
            if v not in skobka and -v not in skobka:
                skobka.append(random.choice([v, -v]))
        skobki.append(skobka)
    return skobki

def edinicy(skobki, znach):
    izmenilos = True
    while izmenilos:
        izmenilos = False
        for s in skobki:
            svobodnyh = 0
            poslednij = 0
            vypolnena = False
            for lit in s:
                z = znach[abs(lit)]
                if z == 0:
                    svobodnyh = svobodnyh + 1
                    poslednij = lit
                elif (z == 1) == (lit > 0):
                    vypolnena = True
            if not vypolnena:
                if svobodnyh == 0:
                    return False
                if svobodnyh == 1:
                    if poslednij > 0:
                        znach[poslednij] = 1
                    else:
                        znach[-poslednij] = -1
                    izmenilos = True
    return True

def dpll(skobki, znach, n, schet, s_edinicami):
    schet[0] = schet[0] + 1
    znach = znach[:]
    if s_edinicami:
        if not edinicy(skobki, znach):
            return False
    else:
        for s in skobki:
            lozhnyh = 0
            for lit in s:
                z = znach[abs(lit)]
                if z != 0 and (z == 1) != (lit > 0):
                    lozhnyh = lozhnyh + 1
            if lozhnyh == len(s):
                return False
    v = 1
    while v <= n and znach[v] != 0:
        v = v + 1
    if v > n:
        return True
    for z in [1, -1]:
        znach[v] = z
        if dpll(skobki, znach, n, schet, s_edinicami):
            return True
    return False

for n in [8, 10, 12]:
    f = sluchajnaya_formula(n, round(4.3 * n), n)
    a = [0]
    b = [0]
    print(n, 2 ** n, dpll(f, [0] * (n + 1), n, a, False), a[0],
          dpll(f, [0] * (n + 1), n, b, True), b[0])

8 256 False 129 False 11
10 1024 True 292 True 16
12 4096 True 119 True 11

Столбцы: n, число наборов значений, ответ и вызовы перебора, ответ и вызовы DPLL. Ответы совпадают. Самая показательная строка - первая: формула невыполнима, и доказать это можно только обойдя всё дерево. Перебору понадобилось 129 вызовов, DPLL - 11: противоречия вскрываются цепочками вынужденных значений на глубине двух-трёх решений.

Про число скобок. При малом их числе формула почти наверняка выполнима, и найти набор легко; при большом - почти наверняка невыполнима, и противоречие находится быстро. Самые трудные случайные формулы - около 4,27 скобки на переменную (опытный порог для больших n; при малых переход размыт), где выполнимые и невыполнимые встречаются примерно поровну. Поэтому замеры решателей делают именно там.

Разбор: раскраска через решатель

raskraska кодирует граф в КНФ по трём правилам из механизма и отдаёт её тому же DPLL. Переменная x(v, c) получила номер 3v + c. Два графа: граф Петерсена (десять вершин, три цвета хватает) и полный граф на четырёх вершинах, где каждая вершина соединена с каждой.

def edinicy(skobki, znach):
    izmenilos = True
    while izmenilos:
        izmenilos = False
        for s in skobki:
            svobodnyh = 0
            poslednij = 0
            vypolnena = False
            for lit in s:
                z = znach[abs(lit)]
                if z == 0:
                    svobodnyh = svobodnyh + 1
                    poslednij = lit
                elif (z == 1) == (lit > 0):
                    vypolnena = True
            if not vypolnena:
                if svobodnyh == 0:
                    return False
                if svobodnyh == 1:
                    if poslednij > 0:
                        znach[poslednij] = 1
                    else:
                        znach[-poslednij] = -1
                    izmenilos = True
    return True

def dpll(skobki, znach, n, schet):
    schet[0] = schet[0] + 1
    znach = znach[:]
    if not edinicy(skobki, znach):
        return []
    v = 1
    while v <= n and znach[v] != 0:
        v = v + 1
    if v > n:
        return znach
    for z in [1, -1]:
        znach[v] = z
        otvet = dpll(skobki, znach, n, schet)
        if len(otvet) > 0:
            return otvet
    return []

def raskraska(vershin, rebra):
    skobki = []
    for v in range(vershin):
        skobki.append([3 * v + 1, 3 * v + 2, 3 * v + 3])
        for a in range(1, 4):
            for b in range(a + 1, 4):
                skobki.append([-(3 * v + a), -(3 * v + b)])
    for r in rebra:
        for c in range(1, 4):
            skobki.append([-(3 * r[0] + c), -(3 * r[1] + c)])
    schet = [0]
    znach = dpll(skobki, [0] * (3 * vershin + 1), 3 * vershin, schet)
    cveta = []
    if len(znach) > 0:
        for v in range(vershin):
            for c in range(1, 4):
                if znach[3 * v + c] == 1:
                    cveta.append(c)
    return [len(skobki), schet[0], cveta]

peterson = [[0, 1], [1, 2], [2, 3], [3, 4], [4, 0],
            [5, 7], [7, 9], [9, 6], [6, 8], [8, 5],
            [0, 5], [1, 6], [2, 7], [3, 8], [4, 9]]
print(raskraska(10, peterson))
k4 = [[0, 1], [0, 2], [0, 3], [1, 2], [1, 3], [2, 3]]
print(raskraska(4, k4))

[85, 7, [1, 2, 1, 2, 3, 2, 1, 3, 3, 2]]
[34, 11, []]

Петерсен: 85 скобок (10 · 4 + 15 · 3), семь вызовов - и раскраска. Проверь любое ребро: 0-1 - цвета 1 и 2, 2-7 - 1 и 3, 4-9 - 3 и 2. Полный граф на четырёх вершинах: 34 скобки, 11 вызовов, ответ пустой - трёх цветов не хватает, и решатель это доказал, обойдя дерево.

Обрати внимание, что код решателя не изменился ни на строку. Вся работа по задаче - в двадцати строках кодирования. Это и есть способ работы с решателями: доказывать трудность и писать алгоритм не нужно, нужно правильно перевести задачу.

Что ломается без этого

Забывают скобки «хотя бы один цвет». Без них решатель вправе не покрасить вершину вовсе - все её переменные ложны, запреты на рёбрах выполнены, и раскраска «найдётся» для любого графа, даже для полного на четырёх вершинах. Каждое скрытое в словах условие должно стать скобкой.

Кодируют неэкономно. «Не больше одного из k» парами - это k(k − 1) / 2 скобок, для k = 1000 - полмиллиона. Существуют записи с дополнительными переменными, где скобок O(k); решатели к этому чувствительны.

Ждут от DPLL чудес на трудных формулах. Распространение единиц не меняет экспоненту в худшем случае: задача остаётся NP-полной. Меняет оно реальные входы, где цепочки длинные.

Читают «невыполнимо» как ошибку программы. Пустой ответ на полном графе - не баг, а доказательство: трёх цветов мало. Часто именно этот ответ и нужен: «расписания с такими ограничениями не существует».

Зачем это в работе

Проверка конфигураций (можно ли включить эти опции вместе), разрешение зависимостей пакетов (библиотека libsolv, на которой стоят DNF и zypper, решает его как задачу выполнимости), проверка схем и программ (может ли утверждение нарушиться), составление расписаний. Во всех этих случаях путь один: перевести задачу в КНФ и отдать решателю. Как устроены современные решатели и почему они справляются с миллионами переменных, - следующий урок.

Теперь сам

1. Скобки (x₁ ∨ x₂), (¬x₁ ∨ x₃), (¬x₃). Что сделает распространение единиц до первого ветвления?
2. Сколько скобок в кодировке раскраски в три цвета графа из 20 вершин и 30 рёбер?
3. Как закодировать «вершина v покрашена не в первый цвет»?