вариации SAT

Я посмотрел в Интернете, но не смог найти «большой список» вариантов проблемы SAT.

Помимо (общего)

• СИДЕЛ,
• к-СБ,
• MAX-КСАТ,
• Half-СБ,
• XOR-СБ,
• НАЗ-СБ

какие еще варианты есть?

(также будет очень полезно, если есть классы сложности (где это возможно))

(Сделать комментарий ответом по запросу и немного расширить.)

«Любопытный ум» следует читать теорему дихотомии Шефера и обобщение на Allender и др. это показывает, что каждый возможный вариант SAT является либо тривиальным, либо одним из шести известных классов сложности:

1. NP-полной
2. P-полной
3. NL-полной
4. L-полной
5. ⊕L-полной
6. совместно NLOGTIME

Этот список будет очень длинным;) Вот некоторые из моих любимых (NP-complete) вариантов SAT:

• PLANAR ( ) -SAT (каждое предложение содержит не менее двух и не более трех литералов, каждая переменная фигурирует ровно в трех предложениях: дважды в неотрицательной форме, один раз в отрицательной форме и двудольный график заболеваемости плоская.)$\le 3, 3$

  См .: Дальхаус, Джонсон, Пападимитриу, Сеймур, Яннакакис, Сложность многотерминальных сокращений, SIAM Journal of Computing 23 (1994) 864-894

• 4-КОМНАТНЫЙ ПЛАНАР 3-СОЕДИНЕННЫЙ 3SAT (каждое предложение содержит ровно 3 различные переменные, каждая переменная появляется не более чем в 4 предложениях, график инцидентности с бипатитом является плоским и 3-связным)

  См .: Кратохвиль, Специальная плоская проблема выполнимости и следствие ее NP-полноты, Discrete Applied Math. 52 (1994) 233-252

• MONOTONE CUBIC 1-IN-3SAT (MONOTONE-1-IN-3SAT, в котором каждая переменная появляется ровно 3 раза)

  См .: Мур и Робсен, Проблема жестких углов с простыми плитками, Дискретные вычисления. Геом. 26 (2001) 573-590

• $k$$k$

  Смотрите этот пост .

На «NP-полной стороне» я сталкивался с этими вариантами (я тоже задавал похожий вопрос на cs.stackexchange):

• Планар 3-САТ;
• Планарная SAT 1-в-3 и положительная планарная SAT 1-в-3 (см. Mulzer и Rote );
• NAE 3-SAT;
• 2/2/4-SAT (см. « Найти кратчайшее решение для расширения NxN в 15-Puzzle» неразрешимо Д. Ратнер и М. Вармут (1986) );
• XSAT, NAE-SAT для линейных монотонных формул, XSAT для точных линейных формул (см. Прекрасную работу Эвальда Спекенмейера по линейным задачам XSAT: вычислительная сложность SAT, XSAT и NAE-SAT для линейных и смешанных формул Горна CNF );
• k-окрашиваемый монотон NAE-3SAT (см. P Jain, «О варианте монотона NAE-3SAT и проблеме разреза без треугольников», 2010 ).

$\mathrm{SAT}(k)$$\mathrm{SAT}$$k$$\mathrm{SAT}(2)$$\mathsf{L}$$\mathrm{SAT}(k)$$k\geq 3$

Помимо списка выше, есть также:

• #SAT: подсчет моделей
• All-SAT: модель перечисления

Существует очень классическая связь между логикой и алгеброй, которая восходит к происхождению современной логики и работ Джорджа Буля. Формула в логике высказываний может быть интерпретирована как элемент булевой алгебры. Логические константы true и false становятся алгебраическими понятиями верхнего и нижнего элементов решетки. Логические операции соединения, дизъюнкции и отрицания станут алгебраическими операциями встречи, соединения и дополнения в булевой алгебре. Эта связь менее подчеркивается в современных трактовках логики, но особенно интересна в контексте вашего вопроса. Алгебра позволяет нам отойти от многих специфических для проблемы деталей и найти обобщения проблемы, которые будут применяться ко многим различным ситуациям.

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

Другим обобщением является логика первого порядка без кванторов, где возникает вопрос об удовлетворенности по модулю теории. Это означает, что в дополнение к булевым переменным у вас также есть переменные первого порядка и символы функций, и вы хотите знать, выполнима ли формула. На этом этапе вы можете задавать вопросы о формулах в арифметике, теориях строк или массивов и т. Д. Таким образом, мы получаем строгое и очень полезное обобщение SAT, которое имеет множество приложений в системах, компьютерной безопасности, языках программирования, верификации программ, планировании искусственный интеллект и др.