In mathematical logic, satisfiability is about whether a formula can be valid under some interpretation (parameters). We say that a formula is unsatisfiable if it can't be true under any interpretation. A Boolean satisfiability problem, or SAT, is all about whether a Boolean formula is valid (satisfiable) under any of the values of its parameters. Since many problems can be reduced to SAT problems, and solvers and optimizations for it exist, it is an important class of problems.
SAT problems have been proven to be NP-complete. NP-completeness (short for nondeterministic polynomial time) means that a solution to a problem can be verified in polynomial time. Note that this doesn't mean that a solution can be found quickly, only that a solution can be verified quickly. NP-complete problems are often approached with search heuristics and algorithms.
In this recipe, we'll address a SAT problem in various ways. We'll take a relatively simple...
