Почему MAX-SAT является обобщением проблемы SAT? - PullRequest
Новая
       75

Почему MAX-SAT является обобщением проблемы SAT?

1 голос
/ 03 февраля 2020

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

Я не понимаю 2-е предложение о том, как MAX-SAT является обобщением SAT. Согласно Википедии, SAT спрашивает, могут ли переменные данной булевой формулы быть последовательно заменены значениями ИСТИНА или ЛОЖЬ таким образом, что формула оценивается как ИСТИНА.

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

1 Ответ

1 голос
/ 03 февраля 2020

Представьте себе, что хотите превратить каждое из ваших предложений в значения, добавив p -> q, где p - это переменная fre sh для каждого предложения q, с которым вы столкнулись в исходной задаче. Тогда удовлетворительным примером этой модифицированной проблемы является решение проблемы MAXSAT оригинала, когда вы выбираете те предложения, где решатель присваивает true соответствующему p. Это дает вам решатель maxsat, хотя и дурацкий.

А теперь представьте, что у вас есть система, которая гарантирует, что она делает как можно больше из этих p истинными. Эта комбинация теперь дает вам решатель maxsat, т. Е. Тот, который может оптимизировать число истинных значений p s. Таким образом, вы получаете хороший решатель maxsat для вашей исходной задачи, то есть вы можете уменьшить задачу maxsat до sat, при условии, что у вас есть что-то, что максимизирует количество истинных назначений тем p, которые вы вводите при переводе.

@ PatrickTrentin, вероятно, может объяснить гораздо лучше! Бумага vZ (механизм maxsat, связанный с z3) также очень удобна и проста для чтения по этой теме c: https://backend.orbit.dtu.dk/ws/portalfiles/portal/110977246/Bj_rner_Phan_Fleckenstein_Unknown_Z_An_Optimizing_SMT_Solver_1.pdf

...