вариации SAT

14

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

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

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

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

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

Subhayan
источник
Какова будет цель этого списка?
Тайсон Уильямс
2
Во-первых, потому что я хотел выступить с речью перед некоторыми студентами. Я планировал поговорить о вариациях SAT и показать некоторые (нетривиальные) сокращения ... у них уже был вводный курс по TOC, поэтому я подумал, что это может быть хорошей идеей ... И ВТОРОЙ ПРИЧИНОЙ является тот факт, в интернете такого списка нет, этот список также послужит любопытному человеку, который хочет узнать о вариантах.
Субхайан
11
Я не уверен, как этот список поможет с вашей беседой. Вместо того, чтобы читать произвольно длинный список вариантов SAT, любопытный ум должен прочитать теорему дихотомии Шефера и обобщение Аллендера и соавт. это показывает, что каждый возможный вариант SAT завершен для одного из шести известных классов сложности.
Тайсон Уильямс
это хорошее предложение ... спасибо @TysonWilliams .. вы также можете сделать это ответом, хотя это не совсем то, что я искал, но, безусловно, это полезно.
Субхайан

Ответы:

17

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

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

  1. NP-полной
  2. P-полной
  3. NL-полной
  4. L-полной
  5. ⊕L-полной
  6. совместно NLOGTIME
Тайсон Уильямс
источник
17

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

  • PLANAR ( ) -SAT (каждое предложение содержит не менее двух и не более трех литералов, каждая переменная фигурирует ровно в трех предложениях: дважды в неотрицательной форме, один раз в отрицательной форме и двудольный график заболеваемости плоская.)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

  • КК

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

user13136
источник
4
Если вам интересен последний пункт, вам также может быть интересно узнать, что # PLANAR-NAE-3SAT (подсчет решений) также поддается обработке, тогда как другие, казалось бы, простые варианты SAT, такие как PLANAR-MONOTONE-2SAT, поддаются обработке (или даже тривиальны) как решение проблемы, но # P-трудно для подсчета. Обратите внимание, что сокращение от последней ссылки выше (сокращение PLANAR-NAE-kSAT до PLANAR-NAE-3SAT) не является экономным и что # PLANAR-NAE-4SAT является # P-hard.
Уильям Уистлер
11

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

Марцио де Биаси
источник
7

SAT(К)SATКSAT(2)LSAT(К)К3

Ян Йоханнсен
источник
1

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

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

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

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

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

Виджай Д
источник