Средний

12 мин

8

В предыдущих работах я много писал про линейное и целочисленное программирование (PuLP, OR-Tools, pyomo), про задачи о назначениях, коммивояжёра, раскрой и генерацию столбцов. Сегодня сделаю шаг в соседнюю, но удивительно мощную область: удовлетворение булевой формулы (SAT). Это тот самый фундамент, на котором стоит вся теория NP-полноты, и одновременно крайне практичный инструмент, который иногда «уделывает» классические MIP-солверы на комбинаторных задачах.

Разберём, что такое SAT, какие алгоритмы заставляют современные солверы переваривать миллионы переменных, познакомимся с библиотекой PySAT и доступными через неё солверами, а в финале решим прикладную оптимизационную задачу с помощью MaxSAT.

Материал будет полезен специалистам по математической оптимизации и ML-инженерам, которым нужен ещё один инструмент в портфеле. А управленцы и владельцы процессов, возможно, узнают в примерах свою боль: ручное составление расписаний, конфигурирование заказов, распределение ограниченного ресурса - всё это аккуратно ложится на SAT и считается за секунды.

1. Задача SAT: о чём вообще речь

Задача о выполнимости булевой формулы (Boolean satisfiability problem, SAT) ставится предельно просто:

Дана формула логики высказываний. Существует ли набор значений переменных (True/False), при котором формула становится истинной?

Если такой набор есть, тогда формула выполнима (SAT), и солвер обязан вернуть конкретные значения переменных. Если набора нет ни одного, то формула невыполнима (UNSAT).

Историческое значение задачи трудно переоценить: именно SAT в теореме Кука-Левина (1971) стал первой задачей, для которой доказали NP-полноту. Грубо говоря, любую задачу из класса NP можно за полиномиальное время свести к SAT. Это и хорошая новость (универсальность), и плохая (в худшем случае экспонента).

Конъюнктивная нормальная форма (КНФ)

Почти все солверы работают с формулой в конъюнктивной нормальной форме (КНФ) это конъюнкция (логическое «И») клауз, где каждая клауза это дизъюнкция (логическое «ИЛИ») литералов, а литерал это переменная или её отрицание.

В программистской записи переменные нумеруют целыми числами, а отрицание - это минус. Та же формула:

[[1, -2], [-1, 3], [-2, -3]]

Клауза выполнена, если истинен хотя бы один её литерал. Формула выполнена, если выполнены все клаузы. Любую булеву формулу можно привести к КНФ (например, преобразованием Цейтина), поэтому ограничение на КНФ не сужает класс решаемых задач.

Именно отсюда растёт практическая ценность SAT для нас, «оптимизаторов»: множество дискретных ограничений естественно выражается клаузами, а булевы переменные - это те же 0/1-переменные, что и в целочисленном программировании.

И это ровно язык бизнес-решений «да/нет»: поставить сотрудника на смену или нет, совместима ли опция в комплектации, разрешён ли этот временной слот. Любое такое правило - это клауза, а вопрос «складывается ли план при всех правилах сразу» - это и есть SAT.

2. Основные алгоритмы

2.1. DPLL: каркас, на котором всё держится

Алгоритм Дэвиса-Патнема-Логемана-Лавленда (DPLL, 1962) - это поиск с возвратом (backtracking), усиленный двумя приёмами, которые радикально срезают дерево перебора:

• Распространение единичных клауз (unit propagation). Если в клаузе остался единственный неопределённый литерал, а остальные уже ложны, то этот литерал обязан быть истинным. Присваиваем и каскадно проверяем, не стали ли единичными другие клаузы.

• Чистые литералы (pure literal elimination). Если переменная встречается во всей формуле только в одной «полярности» (всегда без отрицания или всегда с отрицанием), её можно сразу зафиксировать так, чтобы удовлетворить все содержащие её клаузы.

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

Псевдокод:

function DPLL(formula):
    formula = unit_propagate(formula)
    formula = pure_literal_assign(formula)
    if formula пуста:            
      return SAT
    if есть пустая клауза:       
      return UNSAT   # конфликт
    x = выбрать переменную
    return DPLL(formula ∧ x) or DPLL(formula ∧ ¬x)

2.2. CDCL: реально работает на промышленных задачах

Современные солверы представляют собой не «голый» DPLL, а CDCL (Conflict-Driven Clause Learning). Главная идея: каждый конфликт это не просто повод откатиться, а информация, из которой можно «выучить» новую клаузу и больше никогда не наступать на те же грабли.

Ключевые механизмы:

• Анализ конфликта и обучение клауз (clause learning). При конфликте солвер по графу импликаций находит его причину и добавляет в формулу новую «выученную» клаузу, запрещающую повторение этой комбинации присваиваний.

• Нехронологический откат (backjumping). Вместо отката на один шаг солвер прыгает сразу к тому уровню принятия решений, который действительно вызвал конфликт.

• Two-watched literals. Хитрая структура данных: в каждой клаузе «следят» только за двумя литералами, поэтому unit propagation обходится дёшево даже на миллионах клауз.

• VSIDS (Variable State Independent Decaying Sum) - эвристика выбора переменной для ветвления: приоритет получают переменные, часто участвующие в свежих конфликтах.

• Рестарты. Периодический сброс дерева поиска (с сохранением выученных клауз) помогает выбраться из «невезучих» областей.

Именно связка «clause learning + watched literals + VSIDS + рестарты» превратила SAT из теоретической страшилки в инструмент, который на практике решает задачи с сотнями тысяч переменных за секунды.

2.3. Локальный поиск

Отдельная ветвь - стохастический локальный поиск (GSAT, WalkSAT): стартуем со случайного выбора значения переменной и итеративно переворачиваем значения переменных так, чтобы уменьшать число невыполненных клауз. Такие методы неполны (не доказывают UNSAT), но иногда очень быстро находят решение для выполнимых формул. На практике для бизнес-задач почти всегда используется полный CDCL. Предсказуемость важнее.

3. От разрешимости к оптимизации: MaxSAT

«Классический» SAT отвечает только «да/нет». Но нас, как специалистов по оптимизации, интересует лучшее решение, а не любое допустимое. Здесь на сцену выходит MaxSAT.

• MaxSAT: найти значения переменных, максимизирующее число выполненных клауз.

• Weighted Partial MaxSAT - самый практичный вариант. Клаузы делятся на два типа:

  • жёсткие (hard) - обязаны быть выполнены (это наши ограничения модели);

  • мягкие (soft) - каждая имеет вес; солвер старается выполнить как можно более «дорогой» их набор.

Солвер минимизирует суммарный вес нарушенных мягких клауз, эту величину принято называть cost. По сути это уже полноценная целевая функция, и аналогия с MIP становится прямой: жёсткие клаузы ≈ ограничения, веса мягких клауз ≈ коэффициенты целевой функции.

Формат хранения такой модели: WCNF (взвешенная КНФ).

Ограничения мощности (cardinality) и псевдобулевы ограничения

Отдельная боль при кодировании в SAT это ограничения вида «выбрать не более k из набора» или «ровно один». Наивное «не более одного» через попарные запреты даёт клауз. Существуют экономные кодировки:

• sequential counter / totalizer для cardinality-ограничений () имеет линейный или размер;

• псевдобулевы ограничения (pseudo-Boolean, ) используется для взвешенных сумм.

В PySAT всё это уже реализовано (модули pysat.card и pysat.pb), и кодировать вручную не придётся.

4. PySAT и солверы

PySAT это Python-обвязка вокруг целого зоопарка состязательных SAT-солверов плюс набор утилит для кодирования. Под капотом доступны, в частности: Glucose, MiniSat, CaDiCaL, Lingeling, MapleSAT, MergeSat, MiniCard и другие. Сменить решатель можно через замену аргумента.

Основные модули, которые нам понадобятся:

Возможности MaxSAT расширяют спектор применения SAT на задачи оптимизации. Здесь уже две категории клауз: жесткие (hard) и мягкие (soft). Такое расслоение по типам клауз позволяет некоторые из них невыполнять (мягкие) с определенным весом, а задача сводится к минимизации взвешенных нарушений. Об этом чуть подробнее в разделе 6.

«Hello, SAT»

Решим формулу из раздела 1:

# Установка
!pip install python-sat[pblib,aiger]

from pysat.solvers import Solver

# (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3)
clauses = [[1, 2], [-1, 3], [-2, -3]]

with Solver(name='glucose3', bootstrap_with=clauses) as s:
    if s.solve():
        print('SAT:', s.get_model())   # напр. [1, -2, 3]  ->  x1=True, x2=False, x3=True
    else:
        print('UNSAT')

Менеджер переменных IDPool

В реальных задачах переменные удобнее адресовать не «магическими числами», а осмысленными ключами. IDPool отображает любой Python-объект в уникальный целочисленный id и обратно:

from pysat.formula import IDPool

vpool = IDPool()
v = vpool.id(('x', 2, 3))   # вернёт целое; повторный вызов вернёт то же число
print(vpool.obj(v))         # -> ('x', 2, 3)

Cardinality-ограничения «из коробки»

Кодировка «ровно один из списка литералов» масштабируемым способом. Для больших наборов вместо EncType.pairwise (даёт клауз) берут EncType.seqcounter или EncType.totalizer:

from pysat.card import CardEnc, EncType
from pysat.formula import CNF, IDPool

vpool = IDPool()
lits = [vpool.id(('x', c)) for c in range(5)]

cnf = CNF()
cnf.append(lits)                                          # хотя бы один
am1 = CardEnc.atmost(lits=lits, bound=1,
                     vpool=vpool, encoding=EncType.pairwise)
cnf.extend(am1.clauses)                                   # не более одного

5. Практика I: раскраска графа как задача SAT (разрешимость)

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

Можно ли раскрасить вершины графа в k цветов так, чтобы концы любого ребра имели разные цвета?

Кодирование переменных (one-hot). Введём булевы переменные - «вершина покрашена в цвет ».

Ограничения:

1. У каждой вершины ровно один цвет. Моделируем через 2 ограничения: «хотя бы один» (клауза-дизъюнкция) и «не более одного» (попарные запреты).

2. Для каждого ребра и каждого цвета концы не могут делить цвет: .

from pysat.solvers import Glucose3
from pysat.formula import IDPool

def color_graph(edges, n_vertices, k_colors):
    vpool = IDPool()
    x = lambda v, c: vpool.id(('x', v, c))   # вершине v назначен цвет c

    solver = Glucose3()
    for v in range(n_vertices):
        solver.add_clause([x(v, c) for c in range(k_colors)])        # >= 1 цвет
        for c1 in range(k_colors):                                   # <= 1 цвет
            for c2 in range(c1 + 1, k_colors):
                solver.add_clause([-x(v, c1), -x(v, c2)])
    for (u, v) in edges:
        for c in range(k_colors):
            solver.add_clause([-x(u, c), -x(v, c)])                  # разные цвета

    if not solver.solve():
        solver.delete()
        return None

    model = set(solver.get_model())
    coloring = {v: c for v in range(n_vertices)
                     for c in range(k_colors) if x(v, c) in model}
    solver.delete()
    return coloring


# Цикл из 5 вершин C5 (нечётный цикл)
edges = [(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)]

print(color_graph(edges, 5, 2))   # -> None  (UNSAT)
print(color_graph(edges, 5, 3))   # -> {0: 0, 1: 1, 2: 0, 3: 1, 4: 2}  (SAT)

Результат поучителен: нечётный цикл нельзя раскрасить в 2 цвета (солвер честно возвращает UNSAT), а в 3 цвета можно. Так, перебирая k от меньшего к большему и ловя первый SAT, мы по сути находим хроматическое число, а это уже мостик к оптимизации через серию вызовов SAT.

6. Практика II: распределение каналов как Weighted Partial MaxSAT (оптимизация)

Теперь полноценная оптимизация. Возьмём прикладной сюжет, близкий к сетевым задачам из моих прошлых статей про размещение хабов.

Есть набор передатчиков. Близкие передатчики интерферируют, если работают на одном канале, и каждой такой паре сопоставлен вес (величина помех). Доступно всего k каналов, но их может не хватить, чтобы развести всех. Нужно назначить каждому передатчику канал так, чтобы минимизировать суммарный вес интерференции.

Это, по сути, взвешенная раскраска при недостатке цветов. Прямой раскраской (decision) задачу не решить, так как допустимого решения может не быть вовсе. Зато она идеально ложится на Weighted Partial MaxSAT:

• Жёсткие клаузы: каждый передатчик получает ровно один канал (структурное ограничение, нарушать нельзя).

• Мягкие клаузы: для каждой интерферирующей пары и каждого канала добавляем с весом, равным весу пары. Если пара всё же оказалась на общем канале, ровно одна такая клауза нарушится и даст в cost штраф этой пары.

Отдельно стоит представить RC2 (название от Relaxable Cardinality Constraints) - точный MaxSAT-солвер из PySAT и победитель основного трека MaxSAT Evaluation 2018. Он не перебирает решения наугад, а работает «снизу вверх»: многократно зовёт обычный SAT-солвер и получает на невыполнимом запросе конфликтующее ядро unsat core (набор мягких клауз), которые нельзя удовлетворить разом. Далее «отпускает» ровно столько из них, сколько неизбежно, поднимая нижнюю оценку cost. Как только запрос становится выполнимым, накопленный cost уже доказанно минимален, то есть первое же допустимое решение оказывается оптимальным.

Минимизируя cost, RC2 находит именно глобальный минимум суммарной интерференции.

from pysat.formula import WCNF, IDPool
from pysat.examples.rc2 import RC2

def assign_channels(n_tx, k_ch, interference):
    vpool = IDPool()
    x = lambda t, c: vpool.id(('x', t, c))   # передатчику t назначен канал c

    wcnf = WCNF()
    # HARD: ровно один канал на передатчик
    for t in range(n_tx):
        wcnf.append([x(t, c) for c in range(k_ch)])              # >= 1
        for c1 in range(k_ch):
            for c2 in range(c1 + 1, k_ch):
                wcnf.append([-x(t, c1), -x(t, c2)])              # <= 1
    # SOFT: интерферирующая пара не должна делить канал; штраф = вес пары
    for (u, v, w) in interference:
        for c in range(k_ch):
            wcnf.append([-x(u, c), -x(v, c)], weight=w)

    with RC2(wcnf) as rc2:
        model = set(rc2.compute())
        cost = rc2.cost

    assignment = {t: c for t in range(n_tx)
                       for c in range(k_ch) if x(t, c) in model}
    return assignment, "cost: " + str(cost)


# 6 передатчиков; две 'тесные' группы 0-1-2 и 3-4-5 связаны слабым ребром (1,4)
interference = [
    (0, 1, 4), (1, 2, 3), (2, 0, 2),     # треугольник 0-1-2
    (2, 3, 5),                            # перемычка
    (3, 4, 4), (4, 5, 3), (5, 3, 2)     # треугольник 3-4-5
]

print(assign_channels(6, 2, interference))   # -> ({...}, 4)   при 2 каналах
print(assign_channels(6, 3, interference))   # -> ({...}, 0)   при 3 каналах

Что получаем. При k = 2 минимальная суммарная интерференция равна 4: два нечётных треугольника физически невозможно полностью «развести» двумя каналами, и оптимум жертвует двумя самыми дешёвыми конфликтами (веса 2 + 2). При k = 3 каналов уже хватает и cost = 0, интерференции нет вовсе.

Это типичный управленческий вывод оптимизационной модели: расчёт показывает, что добавление одного третьего канала полностью снимает помехи, а значит можно осмысленно сравнить стоимость лицензии на третий канал с ценой остаточной интерференции при двух.

7. Чем SAT и MaxSAT полезны бизнесу

За академической формулировкой скрывается очень «приземлённый» класс задач. Где это регулярно окупается:

• Расписания и графики смен. Жёсткие правила (трудовой кодекс, квалификации, недопустимые сочетания обязанностей) моделируются с помощью hard-клауз; пожелания сотрудников и приоритеты через soft-клаузы с весами. Тот же каркас, что в примере с каналами.

• Конфигурирование продуктов и комплектаций. «Можно ли вообще собрать такой заказ из совместимых опций?» — чистый SAT. «А если нельзя, какая ближайшая допустимая комплектация?» — MaxSAT.

• Распределение ограниченного ресурса без конфликтов: частоты, слоты, причалы, дорожки, лицензии, переговорные, в общем, как в задаче из раздела 6.

• Назначение исполнителей на заявки и маршруты с правилами совместимости и приоритетами.

А вот ради чего всё затевалось! Ниже привел четыре эффекта, которые видно не в логах солвера, а в бюджете и в нервах того, кто отвечает за план:

• Жёсткие правила соблюдаются гарантированно, а не «на глаз». Ручное планирование на масштабе ошибается; модель либо выдаёт корректный план, либо честно сообщает, что его не существует.

• Измеримый оптимум вместо просто «приемлемого» решения. На больших объёмах разница между «оптимально» и «нормально» может быть значимо положительной.

• Быстрые what-if расчёты. Как в примере с третьим каналом: модель за секунды отвечает на «а что, если добавить смену/станок/канал?» и переводит вопрос на язык затрат.

• Объяснение невозможности. Если требования противоречивы, солвер находит минимальное конфликтующее ядро (unsat core), т.е. какие именно правила несовместимы. Спор «почему расписание не складывается» превращается в конкретный список ограничений, которые надо ослабить.

Честная оговорка: SAT — не «серебряная пуля». Польза появляется там, где решения дискретны, правил много и они переплетены, а ручное планирование уже не справляется. Если задача про непрерывные объёмы и потоки — смотрите в сторону линейного и целочисленного программирования (об этом рассказываю в цикле публикаций проекта Make Optimization Simple).

8. Заметки на полях: SAT/MaxSAT или MIP?

Несколько практических наблюдений из опыта, чтобы понимать, когда тянуться за SAT-солвером, а когда оставаться в привычном MIP.

• Размер кодировки решает. Попарная кодировка «ровно один» - это клауз; на сотнях значений она раздувает модель. Для масштаба берите seqcounter/totalizer из pysat.card. Хорошая модель в SAT - ровно та же дисциплина, о которой я писал в статье про эффективные мат. модели: лишние переменные и клаузы напрямую бьют по времени поиска.

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

• MIP силён там, где много линейной арифметики над непрерывными величинами и плотная числовая целевая функция. Чистый SAT не умеет дробные переменные; для них либо дискретизация, либо гибрид (SMT, лениво добавляемые ограничения).

• MaxSAT - это полноценная дискретная оптимизация. Если ваша задача целиком 0/1, а «арифметика» сводится к взвешенным суммам, связка WCNF + RC2 - серьёзный конкурент целочисленному солверу, и часто более быстрый.

• Менять решатель - дёшево. В PySAT можно прогнать одну и ту же КНФ через несколько движков (glucose3, cadical153, minisat22) и выбрать лучший под ваш профиль задач, мини-benchmark пишется в десяток строк.

Заключение

SAT - это та самая «база», которую полезно держать в портфеле моделей рядом с линейным и целочисленным программированием. Сама задача проста до аскетизма (булевы переменные и клаузы), но за счёт CDCL-солверов и надстройки MaxSAT превращается в практичный инструмент дискретной оптимизации. А PySAT снимает почти весь порог входа: кодирование через IDPool и CardEnc, готовый MaxSAT-солвер RC2 и десяток сменных движков под капотом.

Мы прошли путь от определения и КНФ через DPLL и CDCL к рабочему коду: сначала проверили выполнимость (раскраска графа), затем решили настоящую оптимизационную задачу (распределение каналов) с жёсткими и мягкими взвешенными ограничениями.

Если материал зайдёт - в следующих частях «Make optimization simple» могу разобрать кодировку cardinality-ограничений «под капотом», сравнение SAT и CP-SAT из OR-Tools на одной и той же задаче расписаний или гибрид SMT для смешанных моделей.

А если в вашем процессе узнаётся одна из задач выше - напишите в комментариях, разберём постановку. По опыту, такая модель нередко окупается уже на первом пересчёте графика или загрузки ресурса.

Что почитать дальше

• Biere, Heule, van Maaren, Walsh «Handbook of Satisfiability» (фундаментальный справочник).

• Документация PySAT: pysathq.github.io

• Marques-Silva, Lynce, Malik - обзорная глава про CDCL.

• Описание состязательного MaxSAT-солвера RC2 (MaxSAT Evaluation).

Спасибо за внимание, буду рад вопросам и замечаниям в комментариях.