What is SAT in mathematics?

Question

What is SAT, SAT-Solvers and propositional reasoning?

I heard a lot about these terms but never worked closely. Looking for someone to explain these terms in easy language with simple example(s).

Answer 1

Propositional Logic

A proposition in logic is a "zeroth order" statement. So, a propositional formula is roughly one without quantifiers, relations, or functions, such as

$ ((P \to Q) \to P) \to P $

a propositional formula with (meta)variables (such as $P$ and $Q$) is satisfiable if there exist assignments for the variables such that the formula is true. For example

$ ((\top \to \bot) \to \top) \to \top$

is true in most logics. In classical logic, everything is either true or false, so we only care about assignments of truth values. For the remainder of this discussion I will only consider the classical case.

SAT

The boolean satisfiability problem asks "is a given propositional formula satisfiable."

A related problem is the question of "propositional validity". A propositional formula is valid if it is true under every assignment.

Thus, validity and satisfiability are closely related, because if $P$ is satisfiable, then $\lnot P$ is not valid. And, if $P$ is valid, then $\lnot P$ is not satisfiable.

Boolean Satisfiability is of great interest to computer science:

It is not known if an efficient algorithm exists to determine if a propositional statement is satisfiable. Propositional satisfiability is also called SAT. Here, we say an algorithm is efficient if the time it takes is bound above by a polynomial function of its input. No such algorithm is known to exist in this case, but also, it is not yet been shown that such an algorithm is impossible. The class of problems which have polynomial time solutions is called P.

SAT, NPC and P vs NP

On the other hand, checking if a given assignment succeeds is in polynomial time. The class of problems that have this form: they have multiple candidate solutions, and checking those solutions is polynomial time is called NP. The name NP comes from "non-deterministic polynomial" because under the alternate model of computation where you can do arbitrary number of things at the same time, and return which ever succeeds first (or fail if they all do) supports solving these problems in polynomial time (sadly, such computers do not exist). It turns out, that ANY problem in NP can be converted into SAT in polynomial time, and as such, SAT is "NP complete" or "in NPC". If one could solve SAT in polynomial time, one could solve all problems in NP in polynomial time.

This would be a massive result, as it would imply the existence of efficient algorithms for essentially all problems (including breaking any code, proving any mathematical theorem, etc). Most computer scientists think that $P \not = NP$, but this has not been proven, and finding a solution in either direction would be a huge deal. See P vs NP

SAT is the first problem that was proven to be NPC, and it is among the easiest to show. Generally then, showing that sat reduces to another problem in polynomial time is the technique used to show other problems are NPC.

SAT solvers

Although it is widely believed that no efficient algorithms exist to solve SAT in general, various tools have been written which try to be fast in practice. These tools are called SAT solvers. In fact, SAT solvers are so amazingly fast in practice, that often the solution to hard problems in CS is to reduce these hard problems to SAT. This is particularly true in AI, and leads to a wonderful duality, between two subfields of CS

In complexity theory "We want to show problem X is hard, and we know SAT is hard, so lets reduce SAT to X."

In artificial intelligence "We want to solve problem X, and we know that SAT isn't too hard, so lets reduce X to SAT."

The efficiency of SAT solvers can be overstated. One can make even the best SAT solvers choke by encoding certain problems into them (like integer factorization) that are hard in practice even if not in theory. And, if you know things about the structure of your problem, you can often construct custom solutions that will far outperform of the shelf SAT solvers. Still, the large amount of engineering work spent on SAT solvers and related tools (such as SMT solvers) should be taken advantage of when appropriate.