Задача максимальной выполнимости - Maximum satisfiability problem

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

Пример

Формула конъюнктивной нормальной формы

невыполнимо: независимо от того, какие значения истинности присваиваются его двум переменным, по крайней мере одно из четырех его предложений будет ложным. Однако можно присвоить значения истинности таким образом, чтобы три из четырех предложений были истинными; действительно, каждое задание истины сделает это. Следовательно, если эта формула приводится как пример задачи MAX-SAT, решение проблемы - номер три.

Твердость

Задача MAX-SAT является NP-сложной , поскольку ее решение легко приводит к решению проблемы логической выполнимости , которая является NP-полной .

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

Взвешенный MAX-SAT

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

Алгоритмы аппроксимации

1/2 приближения

Случайное присвоение каждой переменной истинности с вероятностью 1/2 дает ожидаемое 2-приближение . Точнее, если в каждом предложении есть не менее k переменных, то это дает (1-2 - k ) -аппроксимацию. Этот алгоритм можно дерандомизировать с помощью метода условных вероятностей .

(1-1 / e ) -приближение

MAX-SAT также можно выразить с помощью целочисленной линейной программы (ILP). Исправление конъюнктивной нормальной формы формулы F с переменными х 1 , х 2 , ..., х п , и пусть С обозначают пункты F . Для каждого предложения c в C пусть S + c и S - c обозначают наборы переменных, которые не инвертируются в c , и те, которые инвертируются в c , соответственно. Переменные y x ILP будут соответствовать переменным формулы F , тогда как переменные z c будут соответствовать предложениям. ПДОДИ выглядит следующим образом:

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

Вышеупомянутая программа может быть преобразована в следующую линейную программу L :

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

Следующий алгоритм, использующий эту релаксацию, является ожидаемым (1-1 / e ) -приближением:

  1. Решить линейную программу L и получить решение O
  2. Установить переменные х , чтобы быть правда с вероятностью у й , где у й это значение дано в O .

Этот алгоритм также можно дерандомизировать с помощью метода условных вероятностей.

3/4 приближения

Алгоритм 1/2-приближения работает лучше, когда клозы большие, тогда как (1-1 / e ) -аппроксимация лучше, когда клозы маленькие. Их можно комбинировать следующим образом:

  1. Выполните алгоритм (derandomized) 1/2 приближения , чтобы получить задание истины X .
  2. Запуск (derandomized) (1-1 / е) -аппроксимации , чтобы получить назначение истины Y .
  3. Выведите, какой из X или Y максимизирует вес удовлетворенных предложений.

Это приближение детерминированного фактора (3/4).

Пример

По формуле

где (1-1 / e ) -аппроксимация установит каждую переменную в True с вероятностью 1/2, и поэтому будет вести себя идентично 1/2-приближению. Предполагая, что присвоение x выбирается первым во время дерандомизации, дерандомизированные алгоритмы выберут решение с общим весом , тогда как оптимальное решение имеет вес .

Решатели

За последние годы было разработано множество точных решателей для MAX-SAT, и многие из них были представлены на известной конференции по проблеме логической выполнимости и связанных с ней проблемах, SAT Conference. В 2006 году на конференции SAT была проведена первая оценка MAX-SAT, в которой сравнивалась производительность практических решателей для MAX-SAT, как это делалось в прошлом для проблемы псевдобулевой выполнимости и проблемы с количественной булевой формулой . Из-за своей NP-сложности экземпляры MAX-SAT большого размера, как правило, не могут быть решены точно, и часто приходится прибегать к алгоритмам аппроксимации и эвристикам.

На последнюю оценку Max-SAT было отправлено несколько решателей:

  • На основе ветвей и границ: Clone, MaxSatz (на основе Satz ), IncMaxSatz, IUT_MaxSatz, WBO, GIDSHSat.
  • На основе выполнимости: SAT4J, QMaxSat.
  • На основании неудовлетворенности: msuncore, WPM1, PM2.

Особые случаи

MAX-SAT - одно из оптимизационных расширений проблемы логической выполнимости , которая представляет собой проблему определения того, могут ли переменные данной логической формулы быть присвоены таким образом, чтобы формула оценивалась как ИСТИНА. Если в предложениях должно быть не более 2 литералов, как в случае 2-выполнимости , мы получаем проблему MAX-2SAT . Если они ограничены максимум 3 литералами на предложение, как в случае 3-выполнимости , мы получаем проблему MAX-3SAT .

Связанные проблемы

Есть много проблем, связанных с выполнимостью булевых формул конъюнктивной нормальной формы.

  • Проблемы с решением :
  • Задачи оптимизации, цель которых - максимизировать количество удовлетворяемых пунктов:
    • MAX-SAT и соответствующая взвешенная версия Weighted MAX-SAT
    • MAX- k SAT, где каждое предложение имеет ровно k переменных:
    • Задача частичной максимальной выполнимости (PMAX-SAT) требует максимального количества пунктов, которое может быть удовлетворено любым назначением данного подмножества пунктов. Остальные пункты должны быть выполнены.
    • Задача мягкой выполнимости (soft-SAT), заданная для набора задач SAT, требует максимального количества тех проблем, которые могут быть решены с помощью любого задания.
    • Проблема минимальной выполнимости.
  • Задача MAX-SAT может быть расширена до случая, когда переменные задачи удовлетворения ограничений принадлежат множеству вещественных чисел. Задача сводится к нахождению наименьшего д такой , что д - расслаблены пересечение из ограничений не является пустым.

Смотрите также

Внешние ссылки

Рекомендации

  1. ^ Марк Крентель. Сложность задач оптимизации . Proc. СТОК '86. 1986 г.
  2. ^ Христос Пападимитриу. Вычислительная сложность. Аддисон-Уэсли, 1994.
  3. ^ Коэн, Купер, Дживонс. Полная характеристика сложности для задач оптимизации логических ограничений . CP 2004.
  4. ^ Вазирани 2001 , стр. 131.
  5. ^ Борчерс, Брайан; Фурман, Юдифь (1998-12-01). «Двухфазный точный алгоритм для задач MAX-SAT и взвешенных MAX-SAT». Журнал комбинаторной оптимизации . 2 (4): 299–306. DOI : 10,1023 / A: 1009725216438 . ISSN  1382-6905 .
  6. ^ Ду, Динчжу; Гу, Цзюнь; Пардалос, Панос М. (1 января 1997 г.). Выполнимости задачи: теория и приложения: DIMACS Workshop, 11-13 марта, 1996 . American Mathematical Soc. п. 393. ISBN. 9780821870808.
  7. ^ Вазирани 2001 , лемма 16.2.
  8. ^ Вазирани 2001 , раздел 16.2.
  9. ^ Вазирани , стр. 136.
  10. ^ Вазирани 2001 , теорема 16.9.
  11. ^ Вазирани 2001 , Пример 16.11.
  12. ^ Р. Баттити и М. Протаси. Приближенные алгоритмы и эвристики для MAX-SAT Справочник комбинаторной оптимизации, Том 1, 1998, 77-148, Kluwer Academic Publishers.
  13. ^ Хосеп Argelich и Felip Маня. Точные решатели Max-SAT для задач с чрезмерными ограничениями . В Journal of Heuristics 12 (4) pp. 375-392. Спрингер, 2006.
  14. ^ Jaulin, L .; Уолтер, Э. (2002). «Гарантированная робастная нелинейная минимаксная оценка» (PDF) . IEEE Transactions по автоматическому контролю . 47 .