Здесь цель состоит в том, чтобы свести произвольную задачу SAT к 3-SAT за полиномиальное время, используя наименьшее количество предложений и переменных. Мой вопрос мотивирован любопытством. Менее формально я хотел бы знать: «Каково« наиболее естественное »сокращение с SAT до 3-SAT?»
Теперь сокращение, которое я всегда видел в учебниках, выглядит примерно так:
Сначала возьмите свой экземпляр SAT и примените теорему Кука-Левина, чтобы свести его к схеме SAT.
Затем вы заканчиваете работу стандартным сокращением схемы SAT до 3-SAT, заменяя вентили пунктами.
Несмотря на то, что это работает, полученные 3-SAT-предложения в итоге выглядят почти не похожими на SAT-предложения, с которыми вы начинали, из-за первоначального применения теоремы Кука-Левина.
Может кто-нибудь увидеть, как сделать сокращение более непосредственно, пропуская шаг промежуточного контура и переходя непосредственно к 3-SAT? Я бы даже был рад прямому сокращению в особом случае n-SAT.
(Я бы предположил, что есть некоторые компромиссы между временем вычислений и размером выходных данных. Ясно, что вырожденное - хотя, к счастью, недопустимое, если P = NP - решение будет состоять в том, чтобы просто решить проблему SAT, а затем создать тривиальную задачу 3). -SAT экземпляр ...)
РЕДАКТИРОВАТЬ: Исходя из ответа храповика, теперь ясно, что сокращение до n-SAT несколько тривиально (и что я действительно должен был подумать, что один из них немного более тщательно, прежде чем публиковать). Я оставляю этот вопрос открытым, если кто-то знает ответ на более общую ситуацию, иначе я просто приму ответ храповика.
Ответы:
Каждое предложение SAT имеет 1, 2, 3 или более переменных. Предложение 3 переменных может быть скопировано без проблем
1 и 2 переменные предложения
{a1}
и{a1,a2}
могут быть расширены до{a1,a1,a1}
и{a1,a2,a1}
соответственно.Раздел с более чем 3 -х переменных
{a1,a2,a3,a4,a5}
может быть расширена до{a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5}
сs1
иs2
новые переменные, значение которых будет зависеть от того, какая переменная в исходном пункте верноисточник
источник
Если вам нужно сокращение от k-SAT до 3-SAT, то ответ храповика работает нормально.
Если вы хотите прямое сокращение от общей формулы высказываний до CNF (и до 3-SAT), тогда - по крайней мере, с точки зрения «SAT solvers» - я думаю, что ответ на ваш вопрос Что такое «наиболее естественное» сокращение ... ? , это: нет «естественного» сокращения !
Из выводов главы 2 - «Кодировки CNF» (очень хорошей) книги: Справочник по удовлетворенности :
...
Как правило, существует множество способов смоделировать данную проблему в CNF, и известно мало рекомендаций по их выбору. Часто существует выбор проблемных характеристик для моделирования в качестве переменных, и некоторые могут потребовать значительных усилий для их обнаружения. Кодировки Цейтина компактны и механизированы, но на практике не всегда приводят к лучшей модели, и некоторые субформулы могут быть лучше расширены. Некоторые пункты могут быть исключены из соображений полярности, и подразумевается, что могут быть добавлены нарушения симметрии или блокированные предложения. Разные кодировки могут иметь разные преимущества и недостатки, такие как размер или плотность раствора, а то, что является преимуществом для одного SAT-решателя, может быть недостатком для другого. Короче говоря, моделирование CNF - это искусство, и мы часто должны исходить из интуиции и экспериментов.
...
Наиболее известным алгоритмом является алгоритм Цейтина (Г. Цейтин. О сложности вывода в исчислении высказываний. Автоматизация рассуждений: Классические статьи в вычислительной логике, 2: 466–483, 1983. Springer-Verlag.)
Для хорошего ознакомления с кодировками CNF прочитайте предлагаемую книгу « Справочник по удовлетворенности» . Вы также можете прочитать некоторые недавние работы и посмотреть ссылки; например:
источник
Позвольте мне опубликовать другое решение, похожее на решение Рэтчела, но несколько иное. Это непосредственно взято из главы 9 второго издания «Руководства по разработке алгоритмов» Стивена Скиены
источник