Перевод SAT в HornSAT

26

Можно ли перевести булеву формулу B в эквивалентное соединение выражений Хорна? Статья в Википедии о HornSAT, похоже, подразумевает, что это так, но я не смог найти какую-либо ссылку.

Обратите внимание, что я имею в виду не «за полиномиальное время», а скорее «вообще».

Евгений Торстенсен
источник
1
Что вы подразумеваете под "переводить"? Очевидно, есть экземпляры SAT, которые нельзя записать в виде формулы HornSAT. Например, пункт (p или q). Но, возможно, вы имеете в виду, что вы хотите получить такое сокращение, чтобы входная формула SAT была удовлетворительной, если бы выходная формула HornSAT была удовлетворительной? В этом случае, конечно, есть тривиальное снижение, так как вы не заботитесь об эффективности ...
Арнаб
Я не имею в виду равнодушных, поскольку это действительно тривиально без ограничений на эффективность. Я имею в виду эквивалент, как в «иметь одинаковые удовлетворяющие назначения», когда мы рассматриваем переменные, общие как для экземпляра SAT, так и для соответствующего экземпляра HornSAT (если нам нужно было добавить некоторые вспомогательные переменные, мы их спроектируем). Я согласен, что это не должно быть возможно, именно для примера (P v Q), но я не знаю, как это доказать. Вы имеете в виду эскиз доказательства?
Евгений Торстенсен
3
Вопрос по-прежнему неоднозначен. Можете ли вы объяснить, что вы подразумеваете под «проецировать их»? Вы имеете в виду, что «назначение A удовлетворяет экземпляру SAT F, если существует присваивание B вспомогательным переменным таким образом, что (A, B) удовлетворяет экземпляру HornSAT F '»? Если так, то я думаю, что вы можете сделать это, просто используя P-полноту HornSAT.
Райан Уильямс

Ответы:

24

Нет. Конъюнкции клаузор Рога допускают наименьшее количество моделей Гербранда, чего не допускают дизъюнкции положительных литералов. Ср Ллойд, 1987, Основы логического программирования .

Наименее модели Гербранда обладают свойством, что они находятся на пересечении всех получателей. Модели Эрбрановы для являются { { } , { Ь } , { , Ь } } , который не содержит его пересечение, так что, как говорит Арнаб, ( б ) является примером формулы который не может быть выражен как совокупность клаузул Рога.(ab){{a},{b},{a,b}}(ab)

Неверный ответ перезаписан

Чарльз Стюарт
источник
Умно, но предложение -a_1 & ... & -a_n -> # не является предложением Хорна.
Евгений Торстенсен
@ Евгений: это так.
Раду GRIGore
4
Роговое предложение - это дизъюнкция литералов с не более чем одним положительным литералом. Преобразуя вышеприведенное в дизъюнкцию литералов, мы получаем a_1 v ... v a_n со всеми положительными литералами. Вышеупомянутое предложение - двойной Рог, но это не помогает моему интересу.
Евгений Торстенсен
@ rgrig: нет, я был сбит с толку. @ Евгений: Ответ исправлен.
Чарльз Стюарт
5

Выравнивание может быть достигнуто следующим образом (снижение с 2SAT до HornSAT). Таким образом, также может быть сведен к формуле Хорна таким образом. Спасибо Джошуа Горхову за указание на это сокращение.(pq)

Входные данные: формула 2-SAT с предложениями C 1 , ..., C k для переменных x 1 , ..., x n .ϕC1Ckx1xn

Построим формулу Рога следующим образом:Q

Будет 4 ( n выбирать 2 ) + 2 n + 1 новых переменных, по одной на каждое возможное предложение 2-cnf для переменных x, содержащее не более 2 литералов ( не только предложения C i в ϕ ) - это в том числе единичных статей и пустой п .. новый переменный , соответствующая п D будет обозначать г D .×n2+2n+1xCiϕDzD

4 ( n выберите 2 ) происходит из того факта, что каждая пара ( x i , x j ) порождает четыре предложения 2-cnf. 2 п исходит из того , что каждый х я могу создать 2 единицы положения. И, наконец, «один» происходит из пустого предложения. Таким образом, общее количество возможных предложений 2-cnf равно = 4 × ( n выберите 2 ) + 2 n + 1 .×n2(xi, xj)2nxi=×n2+2n+1

Если 2-cnf-предложение следует из двух других 2-cnf-предложений D и E на одном шаге разрешения, то мы добавляем предложение Horn ( z Dz Ez F ) к Q ... Снова, мы делаем это для всех возможных 2-CNF положений - все 4 × ( п выбрать 2 ) + 2 п + 1 из них - не только в с я .FDE(zDzEzF)Q×n2+2n+1Ci

Затем мы добавим блок пункты к Q , для каждого п С я появляющимся во входной ф ... Наконец, мы добавим пункт блока ( ¬ г е т р т у ) на Q .zCiQCiϕ(¬zempty)Q

Формула Рога теперь завершена. Заметим, что переменные, используемые в Q , полностью отличаются от переменных, используемых в ϕ .QQϕ

Мартин Сеймур
источник
Кто-нибудь знает об алгоритме в другом направлении? Учитывая формулу Хорна , существует ли способ получить эквивалентное выражение 2SAT (2CNF) ϕ 2 , так что ϕ 1 выполнимо тогда и только тогда, когда ϕ 2 равно? Использование того же набора переменных, или использование дополнительных переменных, или использование совершенно другого набора переменных (как сделано в ответе выше)? Или доказательство того, что это невозможно? ϕ1ϕ2ϕ1ϕ2
Мартин Сеймур
2

Я не думаю, что это возможно. Там нет никакого способа, например, для записи в виде конъюнкции роговых положений , поскольку ф только Outlaws одной уступки истины, а именно 0011. Любого положения рога с менее чем 4 литерала будут запрещать более 1 присваивания правды, а клаксоны с 4 литералами могут ставить вне закона только правду с максимум одним 0.ϕ=(X1X2¬X3¬X4)ϕ

Редактировать: ой не заметил, что на этот вопрос уже ответили


источник