math - 布尔公式编码

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 中使用其他编码，它们使用较少（多项式）子句，但添加（多项式）变量数。通常使用Tseitin 转换来生成这种编码。

请注意，变量的数量不一定是衡量编码有效性的标准。在某些情况下，SAT 可以通过添加冗余子句等技巧极大地加快速度。因此，当您想要生成有效的编码时，您应该查看 CNF 的结构，而不是变量或子句的数量。

Magnus Bjiirk 于 2009 年 7 月 25 日撰写的“Successful SAT Encoding Techniques”是一篇很好的论文，其中包含许多关于 SAT 编码工作的有用参考：http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf ‎< / p>

Answer 2

我真的不知道 SAT 是什么，但从 Wikipedia 看来，您似乎需要为 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

所以我不确定你是如何编码的，但也许这有帮助？