Перейти к содержанию

Булевая выполнимость и оптимизация (SAT/MaxSAT)

Создание объекта модели и инициализация переменных

Как и ранее полагаем, что менеджер инициализирован с корректными для SAT/MaxSAT задач параметрами. За создание SAT/MaxSAT модели отвечает модуль optjet.md_encoder пакета optjet. Хранилищем модели является экземпляр Model, его инициализация выполняется следующим образом:

python model = enc.Model(qmng, "puzzle", False)

На следующем этапе производится декларация переменных. В задачах булевой выполнимости и оптимизации переменные могут быть только логическими (принимающими значения 0 или 1), поэтому указание типа не требуется. Для переменной задаются имя и размерности, представляющие собой верхние границы для индексов. Все индексы принимают значения от 0 до верхней границы минус единица (в соответствии со стандартной конвенцией Python):

python s = model.create_variables("s", m=cnt_m) x = model.create_variables("x", m=cnt_m, p=cnt_p, r=cnt_r, c=cnt_c)

Дополнительно к переменным могут быть заданы индексы. Индексы переменных представляют собой особые объекты, которые играют ключевую роль в автоматизации и упрощении записи модели. Как отмечалось ранее, переменные в задаче, как правило, объединяются в смысловые группы, и участие каждой группы в ограничениях, а также \"место\" переменной в модели фактически определяется индексами.

При этом ограничения также часто группируются в однотипные классы (например, единственность элемента, занимающего данную позицию в расписании, или материальный баланс в узле графа). Внутри одной группы структурно одинаковые условия применяются к различным переменным. Для упрощения описания таких условий в математической записи используется конструкция \<\<для любого индекса(ов) из диапазона выполняется ...>>. При описании ограничений указывается диапазон изменения конкретных индексов. Синтаксис описания задачи для решателя OptJet позволяет осуществлять \<\<клонирование>> ограничений по диапазону изменения индекса. Когда покрывается весь диапазон изменения, синтаксис становится простым. Для этих целей индексы переменных реализованы как специальные объекты, которые при формировании задачи используются энкодером для эффективного кодирования и клонирования блоков формул.

Для задания индексов используется метод get_indexes модели:

```python m, p, r, c = model.get_indexes(["m", "p", "r", "c"])

Краткая запись

m, p, r, c = model.get_indexes("mprc") ```

Задание ограничений

Ограничения задаются методом add_constraint объекта модели. Метод всегда содержит формулу самого ограничения, опционально диапазоны индексов, по которым эта формула должна быть размножена. Для линейных ограничений помимо обычных выражений в виде (не)равенств поддерживаются опционально аргументы lo, hi, для задания нижней и верхней границ выражения включительно.

Формула выражения может содержать значения индексов, связанные внешним лексическим контекстом, а также символы индексов (декларируемые в get_indexes), которые будут использоваться при её тиражировании по диапазонам (далее именуемым foralls). Для логических задач и их формул важно, чтобы имена итераторов и переменных, используемых вне add_constraint для индексации какой-либо переменной, не совпадали с задекларированными индексами.

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

Для булевых задач SAT/MaxSAT энкодер поддерживает смешанные булевые выражения, состоящие из булевых и допускающих множественное применение (где это имеет смысл):

  • И

  • ИЛИ

  • ИСКЛЮЧАЮЩЕЕ ИЛИ

  • ОТРИЦАНИЕ

  • ЭКВИВАЛЕНТНОСТЬ

  • ИМПЛИКАЦИЯ

  • УСЛОВНЫЙ ОПЕРАТОР

и псевдобулевых операций:

  • СЛОЖЕНИЕ

  • ВЫЧИТАНИЕ

  • УМНОЖЕНИЕ НА КОНСТАНТУ

Приведем синтаксис для каждой их них

  • first_expression + \ - second_expression - бинарная операция сложения или вычитания для псевдобулева выражения, expression - допустимая комбинация переменных

  • const * expression - умножение на константу для псевдобулева выражения, expression - допустимая комбинация переменных, const - целая константа. Она может быть целым числом или выражением вида: pow_expression(base, exp), где base - целое положительное число, exp - доступный индекс или целое число, что необходимо для задания натуральных чисел в виде \(\sum_l 2^l x_l\).

  • Sum(expression, indexes) - суммирование по индексу для псевдобулева выражения, expression - допустимая комбинация переменных, indexes - набор индексов, по которым проводится суммирование (каждый задается как итерируемая последовательность в языке Python).

  • SumIt(expressions) - суммирование последовательности псевдобулевых выражений,\ expressions - итерируемая последовательность допустимых комбинаций переменных.

  • expression <= \ == \ >= const - сравнение для псевдобулева выражения, expression - допустимая комбинация переменных, const - константа (целое число). Сравнение обязательно должно быть использовано при применении псевдобулевых выражений (любое выражение, содержащее выше приведенные операции).

  • first_expression & \ | \ ^ second_expression - бинарная операция (И \ ИЛИ \ ИСКЛЮЧАЮЩЕЕ ИЛИ) для булевого выражения, expression - допустимая комбинация переменных

  • expression - унарная операция, отрицание для булевого выражения.

  • And(expression, indexes) - логическое умножение по индексу для булевого выражения, expression - допустимая комбинация переменных, indexes - набор индексов, по которым проводится умножение (каждый задается как итерируемая последовательность в языке Python).

  • AndIt(expressions) - логическое умножение последовательности булевых выражений,\ expressions - итерируемая последовательность допустимых комбинаций переменных.

  • Or(expression, indexes) - логическое сложение по индексу для булевого выражения, expression - допустимая комбинация переменных, indexes - набор индексов, по которым проводится сложение (каждый задается как итерируемая последовательность в языке Python).

  • OrIt(expressions) - логическое сложение последовательности булевых выражений,\ expressions - итерируемая последовательность допустимых комбинаций переменных.

  • Xor(expression, indexes) - исключающее ИЛИ по индексу для булевого выражения, expression - допустимая комбинация переменных, indexes - набор индексов, по которым проводится операция (каждый задается как итерируемая последовательность в языке Python). Задает выражение по форме схожее с полиномом Жегалкина, в котором вместо конъюнкций произвольное булево выражение.

  • XorIt(expressions) - исключающее ИЛИ для последовательности булевых выражений,\ expressions - итерируемая последовательность допустимых комбинаций переменных.

  • Equiv(expressions) - эквивалентность для булевого выражения, expressions - допустимые комбинации переменных.

  • Implication(if_expression, then_expression) - импликация, if_expression - достаточное условие для выполнения then_expression, then_expression - необходимое условие для выполнения if_expression.

  • IfThenElse(if_expression, then_expression, else_expression) - условный оператор, if_expression - проверяемая допустимая комбинация переменных, then_expression - верная допустимая комбинация переменных, если проверяемая верна, else_expression - верная допустимая комбинация переменных, если проверяемая неверна

  • Zero - константа, соответствующая булевому False, в псевдобулевых выражениях необходимо использовать 0.

  • One - константа, соответствующая булевому True, в псевдобулевых выражениях необходимо использовать 1.

Синтаксис логических условий помимо логических операций допускает ограниченное использование линейных равенств и неравенств внутри формул.

Рассмотрим некоторые примеры:

python model.add_constraint(Sum(x[m, p, r, c], p=range(cnt_p)) == 1, m=range(cnt_m), r=range(1, cnt_r - 1), c=range(1, cnt_c - 1))

Данный пример иллюстрирует псевдобулево условие: все переменные являются булевыми, все коэффициенты и правая часть --- целыми числами. Это условие равенства единице суммы переменных тиражируется для всех комбинаций индексов из части foralls m=range(cnt_m).... Данная запись соответствует математическому выражению:

\[\forall m \in \{0..cnt_m-1\}, \forall r \in \{1..cnt_r-2\}, \forall c \in \{1..cnt_c-2\}, \, \sum_{p=0}^{cnt_p-1} x_{mprc} = 1.\]

python for ri in range(1, cnt_r - 1): for ci in range(1, cnt_c - 1): model.add_constraint(x[0, table[ri - 1][ci - 1], ri, ci])

Это пример простейшего условия вида \(x_{0,t_{r-1,c-1},r,x} == True\). При задании логических условий всегда подразумевается, что они должны быть истинными, поэтому явно равенство логической константе не пишется. При необходимости использования значений истины и лжи внутри выражений используются встроенные константы \(One\) и \(Zero\).

Второе замечание по примеру - так как второй индекс переменной \(x\) вычисляется по табличному соответствию (массиву) исходя из значений третьего и четвёртого индексов, то задекларированные символы индексов тут не используются. Вместо них в локальной области видимости вводятся обычные вспомогательные переменные и связывание значений индексов происходит снаружи add_constraint, для каждого конкретного ограничения (параметризуемого конкретным значением индексов) оно задаётся независимо, не используя механизм тиражирования.

Дополнительно отметим несколько существенных моментов:

  • Псевдобулевы выражения могут находиться только на самом низком уровне вложенности логического условия; это означает, что внутри линейных формул могут использоваться только переменные без логических операций. Если требуется включить в псевдобулево выражение результат логической операции над переменными, вводятся дополнительные переменные, значения которых связываются с необходимым вычислением через Equiv;

  • Индексы ограниченно поддерживают арифметические операции - можно писать \(m+1\) или \(m-1\) используя символ индекса;

  • Для сокращения записи можно использовать списочные варианты конструкторов выражений, имена которых заканчиваются на It (от Iterator, фактически поддерживаются любые объекты, возвращающие итератор выражений). Так как внутри находится list comprehension из Python, то условия на соответствия значений индексов можно задавать в привычном синтаксисе. Пример записи для линейной задачи был приведён выше, для логической задачи формулы ограничений задаются аналогично.

Эффективное кодирование псевдобулевых выражений в представления для задачи выполнимости представляет известную открытую задачу. Наилучшие способы для суммы из \(k\) слагаемых формируют порядка \(k \cdot log(k)\) дизъюнктов и дополнительных технических переменных с \<\<неудобной>> для решателя структурой, а \<\<удобная>> структура даёт ещё более громоздкое и неприменимое на больших задачах представление, поэтому \<\<длинные>> суммы более нескольких тысяч слагаемых в постановку по возможности не стоит включать, заменяя другими представлениями.

Использование длинных сумм

Кодирование псевдобулевых неравенств с большим числом слагаемых (более сотен) порождает большое количество вспомогательных переменных и дизъюнктов во внутреннем представлении решателя. Для частных ситуаций \(\sum x_i = 1\) (поднят только один флаг, Xor, only one - встречаются разные названия), \(\sum x_i \leq k\) (ограничение на количество - cardinality constraint) существуют и автоматически выбираются наиболее оптимальные специальные способы трансляции в КНФ, но они всё равно тяжелы в случае большого количества слагаемых.

В случае появления длинных сумм и при невозможности переформулировать задачу, используются следующие приёмы:

  • Разбить сумму на отдельные группы слагаемых, которые приравниваются дополнительным натуральным переменным

  • Используя информацию с этапа предобработки данных для задачи при генерации выражения не включать слагаемые с заведомо нулевыми коэффициентами

Использование импликации

Для задач булевой выполнимости и оптимизации решатель использует внутри представление задачи в виде КНФ. Ключевым моментом является то, что КНФ состоит из дизъюнктов (clauses) - формул, где логическое ИЛИ применяется к группе переменных \(x_1 \vee x_2 \vee ... \vee x_n\). Чем больше таких формул возникает и чем больше вспомогательных переменных необходимо для представления задачи в виде КНФ тем она обычно сложнее.

Наиболее простой ситуацией, когда трансляция ограничения пользователя во внутреннее представление не порождает лишних дизъюнктов и переменных, является, очевидно, когда само ограничение - дизъюнкт, не требующий никаких преобразований. Частым частным случаем является ситуация вида \(formula = \bigwedge_{j-1}^n y_j \rightarrow \bigvee_{i=1}^n x_i\), то есть импликациия из конъюнкции в дизъюнкцию.

Из логики известно, что \((a \rightarrow b) \leftrightarrow (\neg{a} \vee b)\), то есть \(formula = \bigvee_{j-1}^n \neg{y_j} \vee \bigvee_{i=1}^n x_i\) - дизъюнкт.

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

Задание целевой функции

Для задач булевой выполнимости цель оптимизации не ставится, поэтому задание целевой функции не применимо. Для задач булевой оптимизации можно задавать условия оптимума. Следует отметить, что полное наименование наименование булевой оптимизации --- взвешенная (weighted, опционально) частичная (partial, также опционально, но обычно включаемое) максимизация булевой выполнимости --- (W)(P)MaxSAT.

Концептуально это означает, что задача включает два набора условий --- жестких ограничений задачи (в общем случае могут отсутствовать, тогда задача не частичная) и мягких. Жесткие ограничения эквивалентны ранее рассмотренным ограничениям и задаются также через add_constraint. Мягкие же условия задаются форме дизъюнктов (clauses) --- логических выражений, представляющих собой группы переменных с весами (опционально, определяют сумму выигрыша, если они разные, то задача называется взвешенной), объединенных операцией логического ИЛИ.

Необходимо не нарушая жёстких условий найти такие значения переменных задачи (логическая модель, технически - witness), при которых сумма весов выполненных мягких условий максимальна.

На практике это означает, что целевая функция вида \({\sum_{i\in I} c_i z_i \to \max}\) кодируется в виде:

python for i in I: model.add_soft_constraint(z[i] if c[i] > 0 else ~z[i], abs(c[i]))

То есть для каждого слагаемого (элементарный дизъюнкт из одной переменной, т.н. однолитеральный) пишется его вес - модуль коэффициента, и если коэффициент был отрицательным, то отрицание навешивается на саму переменную. Действует простое правило - все веса делаем положительными, если перед слагаемым стоит знак минус, то он превращается в отрицание, навешенное на соответствующую переменную.

Метод add_soft_constraint поддерживает последний опционально логический аргумент minimization, чтобы не проставлять вручную отрицания и не запутаться:

python for i in I: model.add_soft_constraint(z[i], abs(c[i]), minimization=c[i] < 0)

Динамическая генерация модели

Методы декларации переменных принимают размерности как словарь с параметрами. Индексы также получаются вызовом метода модели со строкой в качестве имени, который можно вызывать несколько раз. Таким образом, переменные и индексы можно генерировать на лету, не опираясь на заранее заданные имена и размерности.

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

Таким образом можно сгенерировать любую формулу для использования в ограничениях.

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

Ускорение построения модели

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

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

Для задач булевой оптимизации, помимо обычных неформализуемых рекомендаций относительно сокращения числа переменных и условий есть частные варианты сокращения времени построения задачи:

  • Убедиться, что формулы транслируются без создания избыточных переменных и дизъюнктов

  • По возможности свести максимальное число ограничений к виду импликаций, сводящихся к одному дизъюнкту.

  • Провести эксперименты и сократить часть КНФ, получающуюся из генерации длинных сумм.

  • Рассмотреть отдельные группы ограничений и по возможности закодировать их с помощью неитераторных версий конструкторов (And вместо AndIt, Sum вместо SumIt). Это обычно требует аккуратного анализа необходимости вычисления конкретных значений индексов в формулах.

Горячий старт

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

Для задачи булевой оптимизации:

python qparams_ext = { "msat.algorithm_enable": "true", "msat.core_g_linear_strategy": "2", "msat.iter_exp_time_factor": "0", "msat.witness_in_file": "false", "msat.witness_in_result_file": "false", "msat.witness_binary_format": "false", "msat.prefatory_use": "true", # Необходимо задать для горячего старта "msat.prefatory_phase_use": "true", # Необходимо задать для горячего старта }

Далее, после формирования модели, но до вызова решателя

python rc = qmng.run()

необходимо выставить значения (части) переменных, которые являются известными и предположительно правильными. Допустимы два формата:

python formula_model.add_preliminary_var_value(sv)

где \(sv\) - номер переменной в хранилище (пользовательские переменные заводятся первыми, согласно порядку вызова \(get\_variables\)). Такой метод подходит для простых задач, либо для случаев нестандартной отладки.

После декларации переменной (как массива numpy) номер её представителя для данных значений индексов можно узнать, вызвав переменную как функцию с целыми аргументами, равными значениям индексов:

python ... q = model.create_variables("q", i = 10) i = model.get_indexes("i") print(f'Variable q with index 0 number is {q(0)}') # Напечатает 1

Соответственно, есть более простой способ задания значения переменной:

python model.add_preliminary_var_value(q(ii)) # Если q(ii) истинно при горячем старте model.add_preliminary_var_value(-q(ii+1)) # Если q(ii+1) ложно при горячем старте