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

В теории вычислительной сложности проблема максимальной выполнимости ( 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 является 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 ^{− k} )-аппроксимацию. ^[8] Этот алгоритм можно дерандомизировать с помощью метода условных вероятностей . ^[9]

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

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

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

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

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

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

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

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

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

Это детерминированный фактор (3/4)-приближение. ^[11]

Пример

По формуле

$${\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 }}$$

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

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

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

Решатели

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

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

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

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

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

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

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

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

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

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

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

• 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. М. Крентель (1988). «Сложность задач оптимизации». Журнал компьютерных и системных наук . 36 (3): 490–509. doi :10.1016/0022-0000(88)90039-6. hdl : 1813/6559 .
2. Марк Крентель. Сложность проблем оптимизации. Труды STOC '86. 1986.
3. Христос Пападимитриу. Сложность вычислений. Addison-Wesley, 1994.
4. Коэн, Купер, Дживонс. Полная характеристика сложности задач оптимизации булевых ограничений. CP 2004.
5. Вазирани 2001, стр. 131.
6. Борчерс, Брайан; Фурман, Джудит (1998-12-01). «Двухфазный точный алгоритм для задач MAX-SAT и Weighted MAX-SAT». Журнал комбинаторной оптимизации . 2 (4): 299–306. doi :10.1023/A:1009725216438. ISSN  1382-6905. S2CID  6736614.
7. Ду, Динчжу; Гу, Цзюнь; Пардалос, Панос М. (1997-01-01). Проблема выполнимости: теория и приложения: семинар DIMACS, 11-13 марта 1996 г. Американское математическое общество. стр. 393. ISBN 9780821870808.
8. Вазирани 2001, Лемма 16.2.
9. Вазирани 2001, раздел 16.2.
10. Вазирани 2001, стр. 136.
11. Вазирани 2001, Теорема 16.9.
12. Вазирани 2001, пример 16.11.
13. Авидор, Ади; Беркович, Идо; Цвик, Ури (2006). «Улучшенные алгоритмы аппроксимации для MAX NAE-SAT и MAX SAT». Аппроксимация и онлайн-алгоритмы . Т. 3879. Берлин, Гейдельберг: Springer Berlin Heidelberg. С. 27–40. doi :10.1007/11671411_3. ISBN 978-3-540-32207-8.
14. Макарычев, Константин; Макарычев, Юрий (2017). «Алгоритмы аппроксимации для CSP». Drops-Idn/V2/Document/10.4230/Dfu.vol7.15301.287 : 39 страниц, 753340 байт. doi : 10.4230/DFU.VOL7.15301.287 . ISSN  1868-8977.
15. Баттити, Роберто; Протаси, Марко (1998). «Приближенные алгоритмы и эвристики для MAX-SAT». Справочник по комбинаторной оптимизации . стр. 77–148. doi :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 Transactions on Automatic Control . 47 (11): 1857–1864. doi :10.1109/TAC.2002.804479.

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