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.
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 Bjork, 25th July 2009: Link to pdf