Cheatsheet

We all know equations with unknown variables on real number domain are studied a lot. And yes-or-no variables can also form equations. We call that Boolean algebra.

Propositional logic deals with formulas, in which everything is abstracted as a Boolean variable. A formula consists of variables and is true or false according to the truth values of variables. A formula is actually recursively defined.

In Boolean Satisfiabilty Problem (SAT), we try find a set of values that are either true or false to make the formula true.

SAT is a family of problems that are pervasive in the real world. For example, the input and output of logic gate circuits are perfectly described by Boolean formulas.

We use operators in logic formula to form CNF. Some well-known operators are “and” ($\wedge$), “or” ($\wedge$), and “not” ($\neg$). operators are simply a mapping from any numbers of Boolean values to a Boolean value( $\mathrm{op}: \{ \mathbf{true}, \mathbf{false} \}^n \mapsto \{ \mathbf{true}, \mathbf{false} \}$).

SAT is hard to solve. Or strictly, SAT solving is hard to scale. For example, for 30 variables, there are $2^{30}$ combinations of values, and for 31 variables there are $2^{31}$. Add a variable and see a double in run time to find the answer.

We have rules and can syntactically reason with formulas. For example, for variables A, B, if A and B is true, then A is true and B is true.

We can semantically enumerate the possibilities of combinations and search for the valid solution.

Search can be guided to be efficient. A search process is an iteration. We can find a better solution from the current solution.