Классификация неразрешимых / послушных вариантов проблемы выполнимости

20

Недавно я нашел в статье [1] специальную симметричную версию SAT, называемую 2/2/4-SAT . Но есть много завершенных вариантов, например: MONOTONE NAE-3SAT , MONOTONE 1-IN-3-SATNP , ...

Есть и другие варианты: - SAT , Planar-NAE- SAT2SATSAT , ...

Существуют ли обзорные документы (или веб-страницы), которые классифицируют все (странные) варианты , которые оказались NP- полными (или в P )?SATNPP


  1. NNД. Ратнер и М. Вармут (1986) находят кратчайшее решение для расширения N x N в 15-Puzzle.
Вор
источник
@mrm: спасибо, я не знаю бумаги Шефер ( dl.acm.org/citation.cfm?doid=800133.804350 )
Вор
1
Я удалил «опубликовать свой любимый», потому что это пример из учебника о том, чего не следует спрашивать в Stack Exchange . (Да, в некоторой степени это работает в области теоретической информатики , но это особый случай из-за крайне нетипичной аудитории.)
Жиль: «Так, перестань быть злым»

Ответы:

18

Классические, известные результаты

Как упомянула Standa Zivny по связанному с CSTheory вопросу, какие проблемы SAT являются простыми? есть известный результат Шефера от 1978 года (цитируя ответ Зивного):

Если SAT параметризован набором отношений, разрешенных в любом случае, то существует только 6 возможных вариантов: 2-SAT (т. Е. Каждое предложение является двоичным), Horn-SAT, dual-Horn-SAT, affine-SAT (решения линейного уравнения в GF (2)), 0-действительные (отношения, удовлетворяемые назначением all-0) и 1-действительные (отношения, удовлетворяемые назначением all-1).

Planar-3SAT означает, что планарная версия 3SAT известна какNпNп -полных проблем.

Nпп .

Более свежие и / или "странные" варианты

К -цветный монотон NAE-3SAT

К

φграмм(φ)φ

грамм(φ)φφграмм , и две вершины имеют ребро между ними, если они появляются в некотором предложении вместе.

Кзнак равно4пКзнак равно5Nп .

Линейные варианты CNF

Хотя это, возможно, не экзотично или странно, некоторые известные варианты, а именно NAE-SAT (не все-равные SAT) и XSAT (Exact SAT; ровно по одному литералу в каждом предложении, равном 1, и всем другим литералам, равным 0) Проблема выполнимости была исследована в линейной постановке. Пары линейной формулы попарно имеют не более одной общей переменной. Интересно, что статус сложности не следует из теоремы Шефера.

NпNпКК3Nп является полиномиальным временем, разрешимым на точных линейных формулах, где каждая пара различных предложений имеет ровно одну общую переменную.

Некоторые дополнительные аспекты, касающиеся сложности NAE-SAT и XSAT при определенных допущениях, вероятно, все еще остаются открытыми. Дополнительные подробности см., Например, Porschen и Schmidt, О некоторых SAT-вариантах по линейным формулам, 2009 и Porschen и др., Результаты сложности для линейных XSAT-проблем, 2010 .

Юхо
источник