Проблема максимальной выполнимости - Maximum satisfiability problem

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

Пример

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

${\displaystyle (x_{0}\lor x_{1})\land (x_{0}\lor \lnot x_{1})\land (\lnot x_{0}\lor x_{1})\land (\lnot x_{0}\lor \lnot x_{1})}$

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

Твердость

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

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

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

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

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

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

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

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

MAX-SAT также можно выразить с помощью целочисленная линейная программа (ILP). Зафиксируем формулу конъюнктивной нормальной формы F с переменными Икс₁, Икс₂, ..., Икс_п, и разреши C обозначают пункты F. По каждому пункту c в C, позволять S⁺_c и S⁻_c обозначают множества переменных, которые не отрицаются в c, и те, которые отрицаются в c, соответственно. Переменные у_Икс ИЛП будет соответствовать переменным формулы F, а переменные z_c будет соответствовать пунктам. ПДОДИ выглядит следующим образом:

максимизировать	${\displaystyle \sum _{c\in C}w_{c}\cdot z_{c}}$		(максимизируйте вес выполненных пунктов)
при условии	${\displaystyle z_{c}\leq \sum _{x\in S_{c}^{+}}y_{x}+\sum _{x\in S_{c}^{-}}(1-y_{x})}$	для всех ${\displaystyle c\in C}$	(пункт верен если только у него есть истинная неотрицательная переменная или ложная отрицательная)
	${\displaystyle z_{c}\in \{0,1\}}$	для всех ${\displaystyle c\in C}$.	(каждое предложение либо выполнено, либо нет)
	${\displaystyle y_{x}\in \{0,1\}}$	для всех ${\displaystyle x\in F}$.	(каждая переменная либо истинна, либо ложна)

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

максимизировать	${\displaystyle \sum _{c\in C}w_{c}\cdot z_{c}}$		(максимизируйте вес выполненных пунктов)
при условии	${\displaystyle z_{c}\leq \sum _{x\in S_{c}^{+}}y_{x}+\sum _{x\in S_{c}^{-}}(1-y_{x})}$	для всех ${\displaystyle c\in C}$	(пункт верен если только у него есть истинная неотрицательная переменная или ложная отрицательная)
	${\displaystyle 0\leq z_{c}\leq 1}$	для всех ${\displaystyle c\in C}$.
	${\displaystyle 0\leq y_{x}\leq 1}$	для всех ${\displaystyle x\in F}$.

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

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

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

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

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

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

Это детерминированное (3/4) приближение множителя.^[10]

Пример

По формуле

$${\displaystyle F=\underbrace {(x\lor y)} _{{\text{weight }}1}\land \underbrace {(x\lor \lnot y)} _{{\text{weight }}1}\land \underbrace {(\lnot x\lor z)} _{{\text{weight }}2+\epsilon }}$$

куда ${\displaystyle \epsilon >0}$, (1-1 /е) -approximation установит для каждой переменной значение True с вероятностью 1/2, и поэтому будет вести себя идентично 1/2-приближению. Предполагая, что присвоение Икс выбирается первым во время дерандомизации, дерандомизированные алгоритмы выберут решение с общим весом ${\displaystyle 3+\epsilon }$, а оптимальное решение имеет вес ${\displaystyle 4+\epsilon }$.^[11]

Решатели

Многие точные решатели для MAX-SAT были разработаны за последние годы, и многие из них были представлены на известной конференции по проблеме логической выполнимости и связанных с ней проблемах, SAT Conference. В 2006 году на конференции SAT состоялась первая Оценка MAX-SAT сравнивая производительность практических решателей для MAX-SAT, как это делалось в прошлом для псевдобулевская выполнимость проблема и количественная логическая формула Проблема: из-за своей NP-сложности экземпляры MAX-SAT большого размера в целом не могут быть решены точно, и часто приходится прибегать к аппроксимационные алгоритмы и эвристика ^[12]

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

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

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

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

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

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

• Проблемы с решением:
  • 2СБ
  • 3СБ
• Задачи оптимизации, цель которых - максимизировать количество удовлетворяемых пунктов:
  • MAX-SAT и соответствующая взвешенная версия Взвешенный MAX-SAT
  • МАКСИМУМ-kSAT, где в каждом пункте ровно k переменные:
    • МАКС-2САТ
    • МАКС-3САТ
    • МАКСЭКСАТ
  • Задача частичной максимальной выполнимости (PMAX-SAT) требует максимального количества пунктов, которое может быть удовлетворено любым назначением данного подмножества пунктов. Остальные пункты должны быть выполнены.
  • Задача мягкой выполнимости (soft-SAT), учитывая набор задач SAT, требует максимального количества тех проблем, которые могут быть решены с помощью любого задания.^[13]
  • Проблема минимальной выполнимости.
• Задачу MAX-SAT можно распространить на случай, когда переменные проблема удовлетворения ограничений принадлежат к набору реалов. Проблема сводится к поиску наименьшего q так что q-расслабленное пересечение из ограничений не пусто.^[14]

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

• Проблема логической выполнимости
• Удовлетворение ограничений
• Выполнимость по модулю теорий

внешняя ссылка

• http://www.satisfiability.org/
• https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/
• http://www.maxsat.udl.cat
• Взвешенные тесты Max-2-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. Дои:10.1023 / А: 1009725216438. ISSN  1382-6905.
6. Ду, Динчжу; Гу, Цзюнь; Пардалос, Панос М. (1 января 1997 г.). Проблема выполнимости: теория и приложения: семинар DIMACS, 11-13 марта 1996 г.. American Mathematical Soc. п. 393. ISBN  9780821870808.
7. Вазирани 2001, Лемма 16.2.
8. Вазирани 2001, Раздел 16.2.
9. Вазирани, п. 136. ошибка sfn: цель отсутствует: CITEREFVazirani (помощь)
10. Вазирани 2001, Теорема 16.9.
11. Вазирани 2001, Пример 16.11.
12. Р. Баттити и М. Протаси.Приближенные алгоритмы и эвристика для MAX-SAT Справочник по комбинаторной оптимизации, Том 1, 1998, 77-148, Kluwer Academic Publishers.
13. Хосеп Аргелих и Фелип Манья. Точные решатели Max-SAT для задач с чрезмерными ограничениями. В Journal of Heuristics 12 (4) pp. 375-392. Спрингер, 2006.
14. Jaulin, L .; Уолтер, Э. (2002). «Гарантированная робастная нелинейная минимаксная оценка» (PDF). IEEE Transactions по автоматическому контролю. 47.

• Вазирани, Виджай В. (2001), Алгоритмы аппроксимации (PDF), Springer-Verlag, ISBN  978-3-540-65367-7