布爾式編碼

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，還是計算編碼所需的位數？我搜查了很多，但無法找到任何東西。

Answer 1

您始終可以將表達式轉換爲邏輯等效的CNF並保留變量數量。但是，在最壞的情況下，這會產生指數數量的子句，這對大多數應用來說至少是不切實際的;-)。因此，SAT中通常會使用其他編碼，它們使用較少（多項式數）的子句，但會添加（多項式）個變量。通常使用Tseitin Transformation來產生這種編碼。

請注意，變量的數量並不一定是衡量編碼效率的一個指標。在某些情況下，SAT可以通過諸如添加冗餘子句等技巧來加速。所以當你想要生成一個有效的編碼時，你應該看看你的CNF的結構，而不是變量或子句的數量。

一個很好的文件，它包含了很多的工作有關SAT編碼是「成功的SAT編碼技術」由Magnus Bjiirk有益的參考，25日2009年7月： http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf

Answer 2

我真的不知道SAT是什麼，但從維基百科看來，您似乎需要給x1-x4分配一些值來保證真實性。事實表看起來像這樣（我認爲）：

假時，在括號中＃是導致與失敗

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 

所以我不知道你如何編碼這一點，但也許這會有所幫助？