# SAT polynomial time

Hi I understood it is not currently possible to solve SAT in polynomial time. Does this mean we can not currently solve an expression with n different boolean variables or with m different symbols in the expression in polynomial time with respect to n?

For example :

( A or B ) and ( not not A and B )

The different number of boolean variables here n is 2 but the number of symbols m is 13.

• It is known that the 3-SAT problem is as hard as m-SAT so the expression length is unimportant.
– user16034
May 5 at 11:48
• @Yves Daoust Yeah I am afraid I dont know either of those :), you can stil formulate an answer and I will upvote you. It might help other noobs alike me. May 5 at 14:32
• This is not an answer, just a comment about $m$.
– user16034
May 5 at 14:52

However, SAT is tractable in the special case that the number of unique variables is low. That is, it's Fixed Parameter Tractable with respect to that parameter. Indeed, we can try each assignment to the variables (of which there are an exponential amount w.r.t. the number of unique variables) and verify whether they satisfy the whole formula (which is linear in the size of the formula). Thus with $$n$$ unique variables and $$m$$ total symbols, SAT is solvable in O($$2^n$$m).