Обучение на конфликтах: почему решатели справляются с миллионами переменных

Если ты разберёшь конфликт по графу следствий, получишь из него выученную скобку, скажешь, куда решатель прыгнет назад, и знаешь, как записать «не больше одного» за линейное число скобок, листай до «Теперь сам».

Как думаешь, что DPLL сделает после тупика

DPLL принял три решения: x₁ = 1, потом x₂ = 1, потом x₃ = 1. Распространение единиц вывело ещё несколько значений и наткнулось на ложную скобку. DPLL отступает к последнему решению и пробует x₃ = 0. Если и там тупик - отступает к x₂ и пробует x₂ = 0, а потом снова x₃ = 1.

Ответь себе до чтения: что, если тупик вообще не зависел от x₂? Тогда в ветке x₂ = 0 решатель снова поставит x₃ = 1 и снова упрётся в то же противоречие - повторит работу, которую уже сделал. На формуле с тысячами переменных такие повторы складываются в экспоненту. CDCL от них избавляется.

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

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

И второе: найдя причину, не нужно отменять все решения с утра. Если пробка зависела только от времени выезда и маршрута, выбор кафе на обед здесь ни при чём - его не пересматривают.

Механизм: граф следствий и выученная скобка

У каждого значения на пути решателя есть уровень - номер решения, после которого оно появилось, - и причина: решение или скобка, которая его вынудила. Вместе это граф следствий. Пусть формула:

c1: (¬x1 ∨ x4)          c3: (¬x3 ∨ x6)
c2: (¬x3 ∨ ¬x4 ∨ x5)    c4: (¬x5 ∨ ¬x6)

Анализ конфликта. Начинаем с нарушенной скобки и заменяем значения текущего уровня их причинами, пока на текущем уровне не останется одно значение. Формально каждая замена - резолюция: из скобок (A ∨ x) и (B ∨ ¬x) следует (A ∨ B). Получается выученная скобка - она следует из формулы, так что добавить её можно всегда, и решений от этого не убудет.

Прыжок назад. Выученная скобка содержит одно значение текущего уровня и какие-то значения прежних уровней. Решатель отступает на наибольший из этих прежних уровней - там скобка становится единичной и сразу даёт новое значение. Уровни между ним и текущим, со всеми их решениями, отбрасываются.

Что ещё в настоящем решателе. Два наблюдаемых литерала в каждой скобке - распространение единиц трогает скобку, только когда её наблюдаемый литерал стал ложным, а не на каждом шаге. Активность переменных: ветвиться по тем, что чаще участвуют в конфликтах (эвристика VSIDS из решателя Chaff, 2001). Перезапуски: время от времени бросить дерево и начать заново, сохранив выученные скобки. Удаление бесполезных выученных скобок, чтобы база не разрасталась.

Правило

CDCL - это DPLL, который на каждом конфликте строит по графу следствий выученную скобку (заменяя значения текущего уровня их причинами, пока там не останется одно) и прыгает назад на наибольший уровень среди остальных литералов скобки. Выученная скобка следует из формулы, работает в распространении единиц и не даёт повторить тот же тупик.

Разбор: конфликт по шагам

Формула - четыре скобки из механизма плюс скобки с другими переменными, которые выполнены при x₂ = 1 и никак не связаны с x₁, x₃…x₆.

уровень 1  решение x1 = 1      c1 вынуждает x4 = 1
уровень 2  решение x2 = 1      ничего не вынуждает
уровень 3  решение x3 = 1      c3 вынуждает x6 = 1
                                c2 (x3, x4 истинны) вынуждает x5 = 1
           c4 = (¬x5 ∨ ¬x6) ложна целиком - конфликт

анализ:    (¬x5 ∨ ¬x6)                     на уровне 3: x5, x6
  с c2 по x5:  (¬x6 ∨ ¬x3 ∨ ¬x4)           на уровне 3: x6, x3
  с c3 по x6:  (¬x3 ∨ ¬x4)                 на уровне 3: только x3
выучено:   (¬x3 ∨ ¬x4);  второй литерал ¬x4 - с уровня 1
прыжок:    на уровень 1; x2 отменено вместе с уровнем 2
там:       x4 = 1, значит, скобка вынуждает x3 = 0

DPLL на этом месте отступил бы на уровень 3 и поставил x₃ = 0 - и ровно это и вышло. Разница обнаружится позже: когда DPLL вернётся пересматривать x₂ и в ветке x₂ = 0 снова поставит x₃ = 1, он снова пройдёт весь путь до конфликта. CDCL туда не пойдёт: скобка (¬x₃ ∨ ¬x₄) при x₄ = 1 сразу вынуждает x₃ = 0, на любом уровне и в любой ветке.

Главное в выученной скобке - что в ней нет x₂ и нет x₁. Решение x₁ повлияло только через x₄, и скобка говорит о причине, а не о пути: «x₃ и x₄ вместе невозможны». Значит, она сработает и там, где x₄ станет истинной по совсем другой причине.

Разбор: «не больше одного» за линейное число скобок

Решатель быстр, но не бесконечно, и размер формулы на него влияет. Самое частое условие - «не больше одного из k». Парами - k(k − 1) / 2 скобок. Последовательный счётчик (Синц, 2005) заводит k − 1 вспомогательных переменных s_i - «если среди первых i есть истинная, то s_i истинна» (скобки задают только это направление, и его хватает) - и обходится 3k − 4 скобками. posledovatelno строит его, программа перебирает все наборы четырёх переменных и проверяет, что формула выполнима ровно тогда, когда истинных не больше одной.

def poparno(x):
    skobki = []
    for i in range(len(x)):
        for j in range(i + 1, len(x)):
            skobki.append([-x[i], -x[j]])
    return skobki

def posledovatelno(x, pervaya_svobodnaya):
    k = len(x)
    s = []
    for i in range(k - 1):
        s.append(pervaya_svobodnaya + i)
    skobki = [[-x[0], s[0]]]
    for i in range(1, k - 1):
        skobki.append([-x[i], s[i]])
        skobki.append([-s[i - 1], s[i]])
        skobki.append([-x[i], -s[i - 1]])
    skobki.append([-x[k - 1], -s[k - 2]])
    return skobki

def vypolnena(skobki, znach):
    for s in skobki:
        ok = False
        for lit in s:
            if (znach[abs(lit)] == 1) == (lit > 0):
                ok = True
        if not ok:
            return False
    return True

k = 4
f = posledovatelno([1, 2, 3, 4], 5)
oshibok = 0
for maska in range(2 ** k):
    edinic = 0
    for i in range(k):
        edinic = edinic + (maska >> i & 1)
    est = False
    for dop in range(2 ** (k - 1)):
        znach = [0]
        for i in range(k):
            znach.append(maska >> i & 1)
        for i in range(k - 1):
            znach.append(dop >> i & 1)
        if vypolnena(f, znach):
            est = True
    if est != (edinic <= 1):
        oshibok = oshibok + 1
print(len(f), oshibok)
for k in [3, 4, 10, 100]:
    x = list(range(1, k + 1))
    print(k, len(poparno(x)), len(posledovatelno(x, k + 1)))

8 0
3 3 5
4 6 8
10 45 26
100 4950 296

Для k = 4 счётчик - 8 скобок, ошибок 0: на всех шестнадцати наборах формула выполнима ровно при одной или ни одной истинной. Таблица: при трёх и четырёх переменных пары короче, с десяти счётчик выигрывает, при ста - 296 скобок против 4950. На тысяче - около трёх тысяч против полумиллиона.

Как устроен счётчик: x_i истинна - значит, s_i истинна («среди первых i есть истинная»); s_{i-1} истинна - значит, и s_i; и главное - x_i и s_{i-1} вместе запрещены: если среди первых i − 1 истинная уже была, x_i должна быть ложной. Три скобки на переменную вместо скобки на каждую пару.

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

Ждут, что решатель справится с чем угодно. Есть формулы, на которых любой CDCL тратит экспоненциальное время: принцип Дирихле «n + 1 голубь в n клетках» в обычной записи требует экспоненциально длинного доказательства невыполнимости методом резолюций (Хакен, 1985), а CDCL - это резолюция. Симметричные задачи - его слабое место.

Раздувают формулу. Парная запись «не больше одного» для тысячи вариантов - полмиллиона скобок, и решатель тратит время на их чтение и распространение.

Удивляются разному времени на одной формуле. Перестановка скобок или переменных меняет эвристики, и время работы может отличаться в разы. Замер делают на нескольких перестановках.

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

Решатели CDCL проверяют схемы процессоров перед выпуском, ищут ошибки в программах (может ли этот assert нарушиться), разрешают зависимости пакетов, подбирают конфигурации и расписания. Решатели Kissat и CaDiCaL - открытые, на соревновании SAT 2024 года Kissat взял первые места во всех категориях основного зачёта. Формат входа у всех один - DIMACS: строка p cnf <переменных> <скобок> и скобки числами с нулём в конце. Из Python их зовут через пакет PySAT. Твоя часть работы - кодирование, и от него зависит больше, чем от выбора решателя.

Теперь сам

1. Скобки (¬a ∨ b), (¬a ∨ c), (¬b ∨ ¬c). Решение a = 1 на уровне 1. Что выведет распространение единиц и какую скобку выучит анализ конфликта?
2. Выученная скобка (¬x₇ ∨ x₂ ∨ ¬x₉): x₇ с уровня 8 (текущего), x₂ с уровня 3, x₉ с уровня 5. Куда прыгнет решатель и что там станет известно?
3. Сколько скобок у последовательного счётчика для k = 50 и сколько у парной записи?