A bite on SAT and proving programs

What’s “SAT?” SAT is a shorthand for a well-known computer science program: the Boolean satisfiability problem. It’s simple: given a formula of Booleans like this:

(A' + B) \cdot (C \cdot D)

…can we figure out an assignment to all the variables to make the entire expression true?

Well, the answer is “yes:” All you have to do is try everything! But, er, that’s a bit much: if you have 4 variables, it’s 4! = 4*3*2*1 = 24 possible configurations of variables. Of course, factorials are fast-growing: 5! is 120 and 10! is 3,628,800.

The other fascinating thing about SAT is that different versions of it are P and NP. 2-SAT, which has product of sums of clauses with only 2 terms, is P while 3-SAT is considered NP. But why is 2-SAT NP? Because we can use the implication relationship that can be encoded as a pair of Booleans in order to determine this specifically because implication can be isolated in a 2-Boolean variable process.

SAT may have applications in other places. If we consider the variables to be, say, input conditions to your program, and the satisfying condition is your program crashing, being able to solve this problem in polynomial time might be helpful rather than having to solve it using an NP algorithm.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s