Boolean formula encoding

Question

i am wondering how many bits required to encode a boolean formula like

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

@ is an instance of SAT. I think it is 4 bits since total number of possible combinations are 2(power4). Is that correct? Should i count OR, NOT, AND to calculate number of bits needed for encoding? I searched a lot but couldn't find anything on this.

Answer 1

You can always convert your expression into a logically equivalent CNF with preserving the number of variables. However, in the worst case this yields an exponential number of clauses, which is at least impractical for most applications ;-). Therefore usually other encodings are used in SAT that use fewer (polynomial number of) clauses but adds a (polynomial) number of variables. Usually a Tseitin Transformation is used to generate this encoding.

Note that the number of variables is not necessarily a measure of how effective an encoding is. In some situations SAT can be sped up immensely by tricks like adding redundant clauses. So when you want to generate an effective encoding, you should look at the structure of your CNF rather than the number of variables or clauses.

A nice paper that contains a lot of useful references to work regarding SAT encoding is "Successful SAT Encoding Techniques" by Magnus Bjiirk, 25th July 2009: http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf‎

Answer 2

I don't really know what SAT is, but from Wikipedia it seems like you need to assign some values to x1-x4 that guarantee truth. The truth table looks like this (I think):

When false, the # in parens is the clause that causes the AND to fail

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

Looking at it, it seems there are 4 cases where the expression will always be true:

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

So I'm not sure how you encode this, but perhaps this helps?