All right, so SAT is a cool problem, sure; possibly even useful. But why is it given so much importance? The short answer is that many other problems, often "difficult" problems, can be reduced to SAT. Let's consider an example first, and then look at Stephen Cook's result that established SAT as the first NP-complete problem, to get a sense of both practical applications of SAT, and its theoretical importance.

clauses, where e e e is the number of edges. Since e = O ( n 2 ) e = O(n^2) e=O(n2) (in fact, e = O ( n ) e = O(n) e=O(n) for planar graphs), the number of variables and clauses in our construction above are polynomials in n n n and k k k . Hence we have a polynomial-time reduction to SAT. The significance of this is discussed further in the next section.

In general, the decision problem of the above example is known as graph colouring, or GT4 in Garey-Johnson's naming, where given a graph and a number k k k the decision problem is to determine if a k k k -colouring for the graph exists. In the above, we had k = 4. k=4. k=4. In this more general definition, with n n n regions, our reduction to SAT involves introducing k ⋅ n k\cdot n k⋅n variables and

In the next section, we see that a much broader set of problems can be reduced to SAT.

As you can see, there are many possible solutions, since in such a simple case we have a valid colouring as long as we assign a different colour to each region, which can be done in 4 ⋅ 3 = 12 4 \cdot 3 = 12 4⋅3=12 ways, corresponding precisely to the 12 12 12 solutions given by our SAT solver.

Let's look at a very simple example. Suppose our map has only two regions, regions 1 1 1 and 2 2 2 and that they are neighbours. Then our SAT input would be:

Next, we need to construct the right set of clauses such that if all of them are satisfied, then we have a proper colouring of the map. Specifically, we need every region to be coloured, and we need no two neighbouring regions to be the same colour. First, let us construct the clauses that will make sure every region has one and only one colour assigned to it. For this, we need to make sure only one of R i R_i Ri​ , B i B_i Bi​ , G i G_i Gi​ or Y i Y_i Yi​ is picked for our assignment at a time. We can express this in terms of K K K clauses for each region i i i . First, we add R i ∨ B i ∨ G i ∨ Y i R_i \vee B_i \vee G_i \vee Y_i Ri​∨Bi​∨Gi​∨Yi​ as a clause, which ensures that region i i i gets at least one colour assigned to it. Then for pair of colours, say R R R and B B B , we add the clause ∼ R i ∨ ∼ B i \sim R_i \vee \sim B_i ∼Ri​∨∼Bi​ which basically says "not both of R i R_i Ri​ and B i B_i Bi​ can be picked at the same time", effectively making sure that exactly one colour is assigned to each region. Finally, for any two neighbouring regions, say i i i and j j j , and each colour, say R R R , we add the clause ∼ R i ∨ ∼ R j \sim R_i \vee \sim R_j ∼Ri​∨∼Rj​ which says not both of i i i and j j j can be coloured red.

This lends itself to a simple decision problem: given a map, is it possible to colour it using 4 or less colours such that no two neighbouring regions are the same colour? The four colour theorem is then true if and only if the answer to this decision problem is always true (provided the input map meets the requirements of a planar graph, a detail we are not too concerned with here). As input, we will take the number of regions n n n , and assume the regions are labelled using numbers 1 1 1 to n n n , and a list of neighbouring regions of the form { i , j } \{i, j\} {i,j} with i ̸ = j i

e j i̸=j , indicating regions i i i and j j j are neighbours. Let us use colours red (R), blue (B), green (G), and yellow (Y) to colour the regions. Our variables are going to be R i R_i Ri​ , B i B_i Bi​ , G i G_i Gi​ and Y i Y_i Yi​ , for 1 ≤ i ≤ n 1 \le i \le n 1≤i≤n , indicating that region i i i is coloured red, blue, green, or yellow, respectively.

You might have heard of the "four colour theorem". In simplest terms, it states that the regions in any map can be coloured using at most four colours such that no two neighbouring regions are coloured the same. See the Wikipedia page on it for more details.

NP-Completeness Of SAT *

In previous section we saw how a problem regarding colouring of regions in a map can be reduced to SAT. This can be further generalized to much larger class of problems: any decision problem that can be decided in polynomial time using a non-deterministic Turing machine can be reduced in polynomial time to SAT. This was first proved in Stephen Cook's paper "The Complexity of Theorem-Proving Procedures", which is the paper that introduced the famous P = NP question as well. Let's go over the basic idea in the paper very briefly here. If you are interested in more details, make sure you have a look at the paper, as it is rather short and a pleasure to read.

But before we go into detail, let us take a moment to discuss why it is of such importance. First, nobody has yet come up with an efficient (polynomial time) algorithm to solve SAT in its generality. (SAT with some restrictions, e.g. 2-SAT, can be solved efficiently though.) Showing that a problem can be reduced to SAT means that if we find an efficient algorithm for SAT then we have found an efficient algorithm for that problem as well. For example, if we find a polynomial-time algorithm for SAT then we immediately have a polynomial-time algorithm for the graph colouring problem given above.

Now, the class of decision problems that can be solved in polynomial-time using a non-deterministic Turing machine is known as NP (which stands for Non-deterministic Polynomial). This is a very large class of problems, since Turing machines are one of the most general computational models we have, and even though we are limited to polynomial-time Turing machines, the fact that the Turing machine does not have to be deterministic allows us much more freedom. Some examples of problems that are in NP are:

all problems in P, e.g. determining if a number is prime or not (PRIMES), and decision versions of shortest path, network flow, etc.,

integer factorization,

graph colouring,

SAT,

and all NP-complete problems (see here for a rather large list of examples).

A problem is said to be NP-complete if it, in addition to being in NP, also has the property that any other problem in NP can be reduced to it in polynomial-time. Cook's paper proved SAT to be NP-complete. In fact, since that paper introduced the concept of NP-completeness, SAT was the first problem to be proved NP-complete. Since then, many other problems have been shown to be NP-complete, often by showing that SAT (or 3-SAT) can be reduced in polynomial-time to those problems (converse of what we proved earlier for graph colouring).

Now, as promised, let's briefly look at why SAT is NP-complete. For this, we need to know more precisely what a Turing machine is. Unfortunately, this would involve a bit more detail than I want to include in this section. So instead, I am going to show that if a problem can be solved using a finite-state machine (FSM) then it be reduced in polynomial-time to SAT. The case for Turing machines, which are a generalizations of finite-state machines (Turing machines are basically FSM's with the addition of a tape that they can read from and write to), is quite similar, just more complicated. I encourage you to read Cook's original paper for details of the proof with Turing machines.

First, let's define what an FSM is. In simplest terms, an FSM is a program that has a finite number of states, and that when fed an input character, moves to another state (or possibly stays in the same state) based on a fixed set of rules. Also, some states are taken as "accepting" states. Given an input string, we feed the string character by character into the FSM, and if at the end the FSM is in an accepting state, the answer to our decision problem is yes. If not, the answer is no.

The below code shows how an FSM could can be implemented in Python. Note that in this implementation, we are forced to have a deterministic FSM. Let's ignore this detail for now though. This particular example implements an FSM that accepts input strings that contain an even number of ones.

from __future__ import print_function def even_ones ( s ): # Two states: # - 0 (even number of ones seen so far) # - 1 (odd number of ones seen so far) rules = {( 0 , '0' ): 0 , ( 0 , '1' ): 1 , ( 1 , '0' ): 1 , ( 1 , '1' ): 0 } # There are 0 (which is an even number) ones in the empty # string so we start with state = 0. state = 0 for c in s : state = rules [ state , c ] return state == 0 # Example usage: s = "001100110" print ( 'Output for {} = {}' . format ( s , even_ones ( s )))

So the core of an FSM is a list of rules of the form ( S , c ) → T (S, c) \rightarrow T (S,c)→T which says if the FSM is in state S S S and receives input character c c c then it goes to state T T T . If for any unique pair of ( S , c ) (S, c) (S,c) there is only one rule ( S , c ) → T (S, c) \rightarrow T (S,c)→T then the FSM is said to be deterministic. This is because the FSM will never need to make a "choice" as to which of the rules to apply. With non-deterministic FSM's, the definition of acceptance needs to be modified a bit: if any set of choices of rules would get us to an accepting state given an input then the input is said to be accepted. It is a well-established result in Automata theory that deterministic and non-deterministic FSM's are computationally equally powerful, because any non-deterministic FSM can be translated to an equivalent deterministic one by the "powerset construction" method. The equivalent deterministic FSM might have an exponentially larger number of states compared to the non-deterministic one, however.

It is also well-known that FSM's can solve a class of problems known as "regular" problems. What this means, in very simple terms, is that if you can write a regular expression that would accept the "yes" instances of your decision problem, then you can solve the problem using an FSM. In fact, regular expressions are often implemented using FSM-like structures. The "compile" phase of using regular expression is precisely when the regular expression engine builds the FSM-like structure from your regular expression. (Exercise: Find a regular expression that accepts the above language, namely binary strings with an even number of ones.)

All right, so let's say a decision problem can be solved using an FSM with states numbered 1 1 1 to n n n . For simplicity, let's assume that our input will be binary (character set is { 0 , 1 } \{0, 1\} {0,1} ). Suppose the FSM has k k k rules given by ( S i , c i ) → T i (S_i, c_i) \rightarrow T_i (Si​,ci​)→Ti​ , for 1 ≤ i ≤ k 1 \le i \le k 1≤i≤k . And assume the input characters are given by s 1 s_1 s1​ to s m s_m sm​ . So our input is of length m m m . Finally, assume that the initial state is 1 1 1 and accepting states are a 1 a_1 a1​ to a q a_q aq​ , where q q q is the number of accepting states.

Following Cook's footsteps, we will introduce the following variables for our SAT reduction:

P t P_t P t ​ which is true iff s t = 1 s_t = 1 s t ​ = 1 ,

which is true iff , and Q t i Q^i_t Q t i ​ which is true iff the FSM is in state i i i after input character s t s_t s t ​ has been fed into the FSM, for 1 ≤ i < j ≤ n 1 \le i < j \le n 1 ≤ i < j ≤ n and 0 ≤ t ≤ m 0 \le t \le m 0 ≤ t ≤ m . We will take t = 0 t=0 t = 0 to be the starting step, before anything has been fed into the FSM.

With these definitions, we proceed to translate the question of whether the input is accepted by the FSM into an instance of SAT. The goal is to produce a set of clauses that are satisfiable iff the FSM ends in an accepting state given the particular input. The clauses that will accomplish this are:

P t P_t P t ​ for 0 ≤ t ≤ m 0 \le t \le m 0 ≤ t ≤ m such that s t = 1 s_t = 1 s t ​ = 1 and ∼ P t \sim P_t ∼ P t ​ for all other 1 ≤ t ≤ m 1 \le t \le m 1 ≤ t ≤ m . These will be the first m m m clauses, each consisting of a single literal.

for such that and for all other . These will be the first clauses, each consisting of a single literal. Q m a j Q^{a_j}_{m} Q m a j ​ ​ for 1 ≤ j ≤ q 1 \le j \le q 1 ≤ j ≤ q . This says that after the last character is fed into the FSM, we want to be in one of the accepting states.

for . This says that after the last character is fed into the FSM, we want to be in one of the accepting states. ∼ Q t i ∨ ∼ Q t j \sim Q^i_t \vee \sim Q^j_t ∼ Q t i ​ ∨ ∼ Q t j ​ for any 1 ≤ i < j ≤ n 1 \le i < j \le n 1 ≤ i < j ≤ n and 1 ≤ t ≤ m 1 \le t \le m 1 ≤ t ≤ m , which effectively says that the FSM can not be in both states i i i and j j j at step t t t . Collectively, these clauses will ensure that the FSM is not in more than one state at a time.

for any and , which effectively says that the FSM can not be in both states and at step . Collectively, these clauses will ensure that the FSM is not in more than one state at a time. Q t 1 ∨ … ∨ Q t n Q^1_t \vee \ldots \vee Q^n_t Q t 1 ​ ∨ … ∨ Q t n ​ for 1 ≤ t ≤ m 1 \le t \le m 1 ≤ t ≤ m . This says that the FSM needs to be in at least one state at any step. Together with the last set of clauses, we ensure that the FSM is in exactly one state at any step.

for . This says that the FSM needs to be in at least one state at any step. Together with the last set of clauses, we ensure that the FSM is in exactly one state at any step. ∼ Q t − 1 S i ∨ P t ∨ Q t T i \sim Q^{S_i}_{t-1} \vee P_t \vee Q^{T_i}_{t} ∼ Q t − 1 S i ​ ​ ∨ P t ​ ∨ Q t T i ​ ​ for all rules ( S i , 0 ) → T i (S_i, 0) \rightarrow T_i ( S i ​ , 0 ) → T i ​ and ∼ Q t − 1 S i ∨ ∼ P t ∨ Q t T i \sim Q^{S_i}_{t-1} \vee \sim P_t \vee Q^{T_i}_{t} ∼ Q t − 1 S i ​ ​ ∨ ∼ P t ​ ∨ Q t T i ​ ​ for all rules ( S i , 1 ) → T i (S_i, 1) \rightarrow T_i ( S i ​ , 1 ) → T i ​ , for 1 ≤ t ≤ m 1 \le t \le m 1 ≤ t ≤ m . These clauses are logically equivalent to " Q t − 1 S i Q^{S_i}_{t-1} Q t − 1 S i ​ ​ and P t P_t P t ​ implies Q t T i Q^{T_i}_{t} Q t T i ​ ​ " which is equivalent to ( S i , 1 ) → T i (S_i, 1) \rightarrow T_i ( S i ​ , 1 ) → T i ​ . In other words, they ensure proper transition between states based on the input.

for all rules and for all rules , for . These clauses are logically equivalent to " and implies " which is equivalent to . In other words, they ensure proper transition between states based on the input. Finally, we want to start in the initial state so we add the clause Q 0 1 Q^1_0 Q 0 1 ​ .

Let's see this in action for the above FSM which accepts strings with an even number of ones in them. First, we have two states, so n = 2 n=2 n=2 . Let's build the SAT instance to handle inputs of length t t t . Also note that we can leave out the first set of clauses (the P t P_t Pt​ and ∼ P t \sim P_t ∼Pt​ ones), in which case any SAT assignment will give us some accepted input. Which means we can list all the strings accepted by the FSM by looking at all the satisfying assignments of the above set of clauses.

Here is an example for t = 3 t=3 t=3 . In this input Q t i Q^i_t Qti​ is written as Qi-t . The states are also labelled 0 0 0 and 1 1 1 instead of 1 1 1 to n n n in the above.

# No more than one state at each step ~Q0-0 ~Q1-0 ~Q0-1 ~Q1-1 ~Q0-2 ~Q1-2 ~Q0-3 ~Q1-3 # At least one state in each step Q0-0 Q1-0 Q0-1 Q1-1 Q0-2 Q1-2 Q0-3 Q1-3 # Add the rules # (EVEN, 1) -> ODD ~Q0-0 ~P1 Q1-1 ~Q0-1 ~P2 Q1-2 ~Q0-2 ~P3 Q1-3 # (ODD, 1) -> EVEN ~Q1-0 ~P1 Q0-1 ~Q1-1 ~P2 Q0-2 ~Q1-2 ~P3 Q0-3 # (EVEN, 0) -> EVEN ~Q0-0 P1 Q0-1 ~Q0-1 P2 Q0-2 ~Q0-2 P3 Q0-3 # (ODD, 0) -> ODD ~Q1-0 P1 Q1-1 ~Q1-1 P2 Q1-2 ~Q1-2 P3 Q1-3 # Start in state 0 Q0-0 # End in an accepting state Q0-3

Let's see the output of running a SAT solver on this, and another file for t = 3 t=3 t=3 and t = 4 t=4 t=4 :

$ python sat.py --all --starting_with P --brief < tests/fsm/even-ones-3.in P1 P3 P1 P2 P2 P3 $ python sat.py --all --starting_with P --brief < tests/fsm/even-ones-4.in P1 P4 P1 P3 P1 P2 P3 P4 P1 P2 P2 P4 P2 P3 P3 P4