2.1. Problems and Encodings
A decision problem is a set of instances, A : Set α. Complexity is measured on words, so a problem
comes with an encoding of its instances as bit strings, enc : α ↪ List Bool. The encoding is
part of every statement: whether a problem is in P can depend on it, as it does for
numbers written in unary rather than binary.
Encodings are built from a few combinators: encBool and encNat (binary) for
atoms, encPair and encList for pairs and lists, and encBits for bit
strings, which encode themselves. Encodings are ordinary functions, so you can look at them:
#eval encNat 5
#eval encPair encNat encBool (5, true)
Problems fix their encodings next to their definitions. Satisfiability of CNF formulas over
variables numbered by natural numbers is SAT, encoded by encCNF:
example : SAT = {φ : Cslib.Logic.PL.CNF ℕ | φ.Satisfiable} := rfl
example : encCNF = encList (encList (encPair encNat encBool)) := rfl
A graph is a list of vertices and a list of edges (Graph), encoded by encGraph.
Clique asks whether a graph has a clique of a given size, so its instances are pairs,
encoded by encPair encGraph encNat.