Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
In my Computability and Complexity class, we are focusing on P, NP, NP-complete, and NP-hard problems and the one thing that keeps coming up is the SAT problem, in the context of reduction from one complexity to another or to explain certain concepts.
Why is SAT so ubiquitous in theoretical computer science?
SAT was the first problem shown to be NP-complete, in Stephen Cook's seminal paper. Even nowadays, when introducing the theory of NP-completeness, the starting point is usually the NP-completeness of SAT.
SAT is also amenable to surprisingly successful heuristic algorithms, implemented by software known as SAT solvers. As a result, there is a lot of practical interest into formulating problems efficiently as instances of SAT.
SAT also shows up in fine-grained complexity, one of whose main assumptions is the strong exponential time hypothesis, which is a conjecture on the computational complexity of SAT.
It is worth mentioning that mathematicians cared about SAT [1] even before it was shown to be NP-complete. See for example Godel's 1956 letter to Von Neumann, where it is known that SAT is $\Omega(n)$ (which I believe is still the best lower bound known, although we know explicit constant factors for some lower bound at least), and discussed that if SAT is $O(n^2)$ it would have vast consequences for mathematics.
I have quoted the relevant passage below for completeness:
One can obviously easily construct a Turing machine, which for every formula $F$ in first order predicate logic and every natural number $n$, allows one to decide if there is a proof of $F$ of length $n$ (length = number of symbols). Let $\Psi(F, n)$ be the number of steps the machine requires for this and let $\phi(n) = \max_F\Psi(F, n)$. The question is how fast $\psi(n)$ grows for an optimal machine. One can show that $\psi(n)≥kn$. If there really were a machine with $\phi(n)\sim kn$ (or even $\sim kn^2$), this would have consequences of the greatest importance. Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine.
...
after all $\phi(n)\sim kn$ (or $\sim kn^2$) only means that the number of steps as opposed to trial and error can be reduced from $N$ to $\log N$ (or $(\log N)^2$). However, such strong reductions appear in other finite problems, for example in the computation of the quadratic residue symbol using repeated application of the law of reciprocity. It would be interesting to know, for instance, the situation concerning the determination of primality of a number and how strongly in general the number of steps in finite combinatorial problems can be reduced with respect to simple exhaustive search.
[1] The problem discussed there is perhaps closer to something like TQBF than SAT, but Arora and Barak describe it as SAT in passing, and I am no logician.
I'll add another perspective, based loosely on Andreas Blass's comment on the accepted answer: SAT is in some sense 'conceptually universal' for a broad class of NP-complete problems. To be more specific, I'd argue that SAT captures the essence of Constraint Satisfaction Problems: find a configuration that satisfies a given set of conditions. Sudoku is a canonical example: we want to place a multiset of objects (usually given as numbers) in a grid such that each row has exactly one of each object and each column has exactly one of each object and each specific subgrid has exactly one of each object.
SAT acts as a sort of assembly language for CSPs; we can 'compile down' a constraint problem into a set of specifically boolean constraints and then transform them into normal form. For instance, for a 4x4 sudoku we could use $4\times4\times4=64$ variables $v_{i,j,n}$ for $1\leq i,j,n\leq 4$ where $v_{i,j,n}$ is true iff the $(i,j)$'th cell of the grid contains the object labeled $\bar{n}$. The constraint that the first row has at least one instance of object $\bar{1}$, for instance, is the clause $v_{1,1,1}|v_{2,1,1}|v_{3,1,1}|v_{4,1,1}$. The constraint that it has no more than one is a little more complicated, but still 'just' polynomially so; it can be expressed as $\neg(v_{1,1,1}\wedge v_{2,1,1})$ $\wedge\neg(v_{1,1,1}\wedge v_{3,1,1})$ $\wedge\neg(v_{1,1,1}\wedge v_{4,1,1})$ $\wedge\neg(v_{2,1,1}\wedge v_{3,1,1})$ $\wedge\neg(v_{2,1,1}\wedge v_{4,1,1})$ $\wedge\neg(v_{3,1,1}\wedge v_{4,1,1})$. In other words, make sure that no two cells in the row both have an instance of object $\bar{1}$. Similar constraints will make sure that every cell has an object and no single cell has two objects in it, etc.
This process is obviously clunky, but hopefully you can see how it's also mechanical, in much the same way as translating a higher-level programming language into assembly code is; we simply need to find some set of booleans that describes the possible state of the thing we're looking for and then write out the set of constraints that those booleans must satisfy both in order to be a valid configuration and in order to be a solution to the problem. Indeed, my understanding is that actual CSP solvers work a lot like this: there's a 'higher level language' for expressing constraints in, and those constraints are then translated down to either SAT or something much like it, to which various solving algorithms can be applied.
You've gotten a number of good answers already so I hesitate to try to contribute more, but I see two more factors that I think make SAT particularly interesting to a lot of people.
The first factor is the "proximity" between 2SAT and 3SAT. We know how to solve 2SAT problems in polynomial time, and have proven that 3SAT is NP complete. It's easy to compare the two, see how they differ, come up with ideas for how it might be possible to transform a 3SAT problem into some equivalent 2SAT problem, etc.
The other factor is that with SAT problems, the goal is clear and it's usually pretty obvious whether we've actually solved the problem or not.
Many of the better known NP-complete problems deal with optimization (e.g., knapsack, traveling salesman). Consider, for the moment, if I have an algorithm that claims to produce the optimal result for traveling salesman in polynomial time.
Especially if you try to examine this on a black-box basis, it may be difficult to be sure whether this actually produces the right result or not. In most cases, about all you could do would be to use some well-known algorithm, and try to find a set of inputs for which you could get a better result than I did. But it's basically a completely open-ended search, and your results could never be "yes it works"--only "it doesn't work" or "it might work".
