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

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

Пример

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

(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 является OptP-полной, ^[1] и, таким образом, NP-трудно , поскольку его решение легко приводит к решению булевой проблемы выполнимости , которая является NP-полной .

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

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

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

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

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

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

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

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

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

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

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

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

Решите линейную программу L и получите решение O
Установите для переменной x значение true с вероятностью y _x , где y _x — значение, заданное O. в

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

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

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

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

Это детерминированная факторная (3/4)-аппроксимация. ^[11]

Пример

По формуле

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 }

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

Уровень развития

Современный алгоритм создан Авидором, Берковичем и Цвиком. ^[13]^[14] а его коэффициент аппроксимации составляет 0,7968. Они также предлагают другой алгоритм, коэффициент аппроксимации которого предположительно равен 0,8353.

Решатели

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

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

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

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

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

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

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

Проблемы с решением :
- 2САТ
- 3САТ
Задачи оптимизации, целью которых является максимизация количества удовлетворяемых условий:
- MAX-SAT и соответствующая взвешенная версия Weighted MAX-SAT
- MAX- k SAT, где каждое предложение имеет ровно k переменных:
- Проблема частичной максимальной выполнимости (PMAX-SAT) требует максимального количества предложений, которое может быть удовлетворено любым назначением данного подмножества предложений. Остальные пункты должны быть соблюдены.
- Задача мягкой выполнимости (soft-SAT) с учетом набора задач SAT требует максимального количества тех задач, которые могут быть решены любым заданием. ^[16]
- Проблема минимальной выполнимости.
Задача MAX-SAT может быть расширена на случай, когда переменные задачи удовлетворения ограничений принадлежат множеству действительных чисел. Задача состоит в том, чтобы найти наименьшее q такое, чтобы q - релаксированное пересечение ограничений не было пустым. ^[17]

См. также

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

Ссылки

^ М. Крентель (1988). «Сложность задач оптимизации». Журнал компьютерных и системных наук . 36 (3): 490–509. дои : 10.1016/0022-0000(88)90039-6 . hdl : 1813/6559 .
^ Марк Крентел. Сложность задач оптимизации . Учеб. СТОК '86. 1986.
^ Христос Пападимитриу. Вычислительная сложность. Аддисон-Уэсли, 1994.
^ Коэн, Купер, Дживонс. Полная характеристика сложности задач оптимизации с логическими ограничениями . КП 2004.
^ Вазирани 2001 , с. 131.
^ Борчерс, Брайан; Фурман, Джудит (1 декабря 1998 г.). «Двухфазный точный алгоритм для решения MAX-SAT и взвешенных задач MAX-SAT». Журнал комбинаторной оптимизации . 2 (4): 299–306. дои : 10.1023/А:1009725216438 . ISSN 1382-6905 . S2CID 6736614 .
^ Ду, Динчжу; Гу, Цзюнь; Пардалос, Панос М. (1 января 1997 г.). Проблема выполнимости: теория и приложения: Семинар DIMACS, 11-13 марта 1996 г. Американское математическое соц. п. 393. ИСБН 9780821870808 .
^ Вазирани 2001 , Лемма 16.2.
^ Вазирани 2001 , раздел 16.2.
^ Вазирани 2001 , с. 136.
^ Вазирани 2001 , Теорема 16.9.
^ Вазирани 2001 , Пример 16.11.
^ Авидор, Ади; Беркович, Идо; Цвик, Ури (2006). «Улучшенные алгоритмы аппроксимации для MAX NAE-SAT и MAX SAT». Приближение и онлайн-алгоритмы . Том. 3879. Берлин, Гейдельберг: Springer Berlin Heidelberg. стр. 27–40. дои : 10.1007/11671411_3 . ISBN 978-3-540-32207-8 .
^ Макарычев Константин; Макарычев, Юрий (2017). «Алгоритмы аппроксимации CSP» . Drops-Idn/V2/Document/10.4230/Dfu.vol7.15301.287 : 39 страниц, 753340 байт. дои : 10.4230/DFU.VOL7.15301.287 . ISSN 1868-8977 .
^ Баттити, Роберто; Протаси, Марко (1998). «Приблизительные алгоритмы и эвристики для MAX-SAT» . Справочник по комбинаторной оптимизации . стр. 77–148. дои : 10.1007/978-1-4613-0303-9_2 . ISBN 978-1-4613-7987-4 .
^ Хосеп Аргелич и Фелип Манья. Точные решатели Max-SAT для задач со сверхограничениями . В журнале эвристики 12 (4), стр. 375–392. Спрингер, 2006.
^ Жолен, Л.; Уолтер, Э. (2002). «Гарантированная робастная нелинейная минимаксная оценка» (PDF) . Транзакции IEEE при автоматическом управлении . 47 (11): 1857–1864. дои : 10.1109/TAC.2002.804479 .

Vazirani, Vijay V. (2001), Approximation Algorithms (PDF) , Springer-Verlag, ISBN 978-3-540-65367-7

[1] М. Крентель (1988). «Сложность задач оптимизации». Журнал компьютерных и системных наук . 36 (3): 490–509. дои : 10.1016/0022-0000(88)90039-6 . hdl : 1813/6559 .

[2] Марк Крентел. Сложность задач оптимизации . Учеб. СТОК '86. 1986.

[3] Христос Пападимитриу. Вычислительная сложность. Аддисон-Уэсли, 1994.

[4] Коэн, Купер, Дживонс. Полная характеристика сложности задач оптимизации с логическими ограничениями . КП 2004.

[FOOTNOTEVazirani2001131-5] Вазирани 2001 , с. 131.

[6] Борчерс, Брайан; Фурман, Джудит (1 декабря 1998 г.). «Двухфазный точный алгоритм для решения MAX-SAT и взвешенных задач MAX-SAT». Журнал комбинаторной оптимизации . 2 (4): 299–306. дои : 10.1023/А:1009725216438 . ISSN 1382-6905 . S2CID 6736614 .

[7] Ду, Динчжу; Гу, Цзюнь; Пардалос, Панос М. (1 января 1997 г.). Проблема выполнимости: теория и приложения: Семинар DIMACS, 11-13 марта 1996 г. Американское математическое соц. п. 393. ИСБН 9780821870808 .

[FOOTNOTEVazirani2001Lemma_16.2-8] Вазирани 2001 , Лемма 16.2.

[FOOTNOTEVazirani2001Section_16.2-9] Вазирани 2001 , раздел 16.2.

[FOOTNOTEVazirani2001136-10] Вазирани 2001 , с. 136.

[FOOTNOTEVazirani2001Theorem_16.9-11] Вазирани 2001 , Теорема 16.9.

[FOOTNOTEVazirani2001Example_16.11-12] Вазирани 2001 , Пример 16.11.

[13] Авидор, Ади; Беркович, Идо; Цвик, Ури (2006). «Улучшенные алгоритмы аппроксимации для MAX NAE-SAT и MAX SAT». Приближение и онлайн-алгоритмы . Том. 3879. Берлин, Гейдельберг: Springer Berlin Heidelberg. стр. 27–40. дои : 10.1007/11671411_3 . ISBN 978-3-540-32207-8 .

[t481-14] Макарычев Константин; Макарычев, Юрий (2017). «Алгоритмы аппроксимации CSP» . Drops-Idn/V2/Document/10.4230/Dfu.vol7.15301.287 : 39 страниц, 753340 байт. дои : 10.4230/DFU.VOL7.15301.287 . ISSN 1868-8977 .

[15] Баттити, Роберто; Протаси, Марко (1998). «Приблизительные алгоритмы и эвристики для MAX-SAT» . Справочник по комбинаторной оптимизации . стр. 77–148. дои : 10.1007/978-1-4613-0303-9_2 . ISBN 978-1-4613-7987-4 .

[16] Хосеп Аргелич и Фелип Манья. Точные решатели Max-SAT для задач со сверхограничениями . В журнале эвристики 12 (4), стр. 375–392. Спрингер, 2006.

[17] Жолен, Л.; Уолтер, Э. (2002). «Гарантированная робастная нелинейная минимаксная оценка» (PDF) . Транзакции IEEE при автоматическом управлении . 47 (11): 1857–1864. дои : 10.1109/TAC.2002.804479 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]