SAT Solver

In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE.

SAT was the first known example of an NP-complete problem. That briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed (but not proven, see P versus NP problem) that no such algorithm can exist.

3-satisfiability is a special case of k-satisfiability (k-SAT) or simply satisfiability (SAT), when each clause contains exactly k = 3 literals.

3-SAT is NP-complete and it is used as a starting point for proving that other problems are also NP-hard. This is done by polynomial-time reduction from 3-SAT to the other problem.

EG. Subset sum problem
Assume that we are given some integers, such as {-7, -3, -2, 5, 8}, and we wish to know whether some of the integers can add up to zero. As the number of integers that we feed into the algorithm becomes larger, the number of subsets grows exponentially, and in fact the subset sum problem is NP-complete. An algorithm that verifies whether a given subset has sum zero is called verifier. A problem is said to be in NP if and only if there exists a verifier for the problem that executes in polynomial time.