What is SAT?

The Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. SAT techniques can be used to prove or disprove properties: if the negation of a property cannot be satisfied, then the property is valid. If the negation of a property is satisfied by a certain interpretation, then this interpretation is a counterexample of the property.