Кодировка булевой формулы

Question

Мне интересно, сколько битов требуется для кодирования логической формулы, такой как

@(x1,x2,x3,x4) = (x1 OR x2 OR NOT(x3) OR x4) AND ((NOT)x2 OR x3) AND (x1 OR (NOT)x4)  

@ является экземпляром SAT. Я думаю, что это 4 бита, так как общее количество возможных комбинаций равно 2(power4). Это верно? Должен ли я считать OR, NOT и AND для вычисления количества битов, необходимых для кодирования? Я много искал, но ничего не мог найти по этому поводу.

Answer 1

Вы всегда можете преобразовать свое выражение в логически эквивалентный CNF с сохранением количества переменных. Однако в худшем случае это приводит к экспоненциальному числу предложений, что, по крайней мере, нецелесообразно для большинства приложений;-). Поэтому обычно в SAT используются другие кодировки, которые используют меньше (полиномиальное количество) предложений, но добавляют (полиномиальное) количество переменных. Обычно трансформация Цейтина используется для генерации этой кодировки.

Обратите внимание, что количество переменных не обязательно является мерой эффективности кодирования. В некоторых ситуациях SAT может быть значительно ускорен такими хитростями, как добавление избыточных предложений. Поэтому, когда вы хотите сгенерировать эффективную кодировку, вы должны смотреть на структуру вашего CNF, а не на количество переменных или предложений.

Хорошая статья, в которой содержится много полезных ссылок на работу, касающуюся кодирования SAT, - "Успешные методы кодирования SAT". Автор Magnus Bjiirk, 25 июля 2009 г.: http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf

Answer 2

Я действительно не знаю, что такое SAT, но из Википедии кажется, что вам нужно назначить некоторые значения для x1-x4, которые гарантируют правду. Таблица правды выглядит так (я думаю):

При значении false знак # в скобках - это условие, которое приводит к сбою AND

TTTT => T
TTTF => T
TTFT => F (2)
TTFF => F (2)
TFTT => T 
TFTF => T
TFFT => T
TFFF => T
FTTT => F (3)
FTTF => T
FTFT => F (2,3)
FTFF => F (3)
FFTT => F (3)
FFTF => F (1)
FFFT => F (3)
FFFF => T

Глядя на это, кажется, есть 4 случая, когда выражение всегда будет истинным:

x1=T,x3=T => T
x1=T,x2=F => T
FTTF => T
FFFF => T

Так что я не уверен, как вы кодируете это, но, возможно, это поможет?