The Satisfiability Problem

The Satisfiability Problem of Propositional Logic, short SAT, is an NP-complete problem. Thus, a solution algorithm for SAT that is in P would prove P = NP. However, it is unlikely that such an algorithm will ever be found as probably P = NP does not hold.

Written by Claus Volko
Vienna, Austria, Europe

Contact: cdvolko (at) gmail (dot) com
Homepage: www.cdvolko.net

The Satisfiability Problem of Propositional Logic (SAT) is about finding a set of assignments to variables in a propositional logic that prove that this formula is satisfiable. If such a set does not exist the program is supposed to print out that the formula is not satisfiable. While it may be sufficient to test a single assignment to discover that a formula is satisfiable, it is necessary to test all possible assignments to prove the opposite - which is 2^n, n being the number of variables, i. e. an exponential number. That is why SAT is in NP but probably not in P.

However, if there is an algorithm with polynomial runtime in respect to the number of variables which is capable of solving SAT, SAT and any other problem in NP will also be in P - i. e., P = NP. This is rather unlikely to be the case as it would suffice to find a polynomial algorithm for a single NP-complete problem to prove that P = NP, but nobody has found such an algorithm in decades.

Could it be possible that SAT could be used to show that P = NP is not true, i. e. P is not equal to NP? Take a look at this reasoning: The solution space has size 2^n. What matters however is not the size of the solution space but the size of the search space. Is there an algorithm which, even if the solution space has an exponential size, only needs to scan a polynomial number of possible solutions? If so, P = NP; otherwise, P is not equal to NP.

The fact that it is possible that the search spacing is polynomial or even less complex even if the solution space is exponential can be shown by the problem 2-COL which is about whether a graph can be colorized with only two colors in such a way that there is no pair of two nodes connected by an edge both of which are assigned the same color. Here, each node can be assigned one of two possible colors, so the solution space is sized 2^n. But it is enough to consider a single solution, so the search space has a constant size of 1. The reason: It is enough to start with a random node and then colorize the neighbor nodes; each node needs to be colorized only at most once, and to determine the color it is enough to check each of its neighbor nodes only once, which implies a maximum complexity of n^2. If all nodes can be colorized this way, the graph is colorizable with two colors; if there is a node that cannot be assigned either color as it already has neighbors of both colors, we have proven that the graph cannot be colored with just two colors.

In theory, it is thus possible that a problem with an exponential solution space can be solved in polynomial time. The question is just whether this also applies to SAT - and most of all: how to prove that it does not apply to SAT (which is likely to be the case)? It is much harder to prove that something does not apply than to prove that it does!

I leave it to you as an exercise to prove that 2-COL is not NP-complete, i. e. SAT cannot be reduced to 2-COL (while it is possible the other way round!).

Claus Volko

This article is a translation of an article from MATHEMATIQ #10.