def NPCompleteness.BoolFormula.vars : BoolFormula → Finset ℕ

The (finite) set of variable indices occurring in a Boolean formula φ. Recursively collected: variables of constants are empty, of var n is {n}, and of compound formulas is the union of subformulas' variable sets.

def NPCompleteness.BoolFormula.numVars (φ : BoolFormula) : ℕ

The number of distinct variables occurring in φ.

noncomputable def NPCompleteness.BoolFormula.countSat (φ : BoolFormula) : ℕ

The number of satisfying assignments of φ, where assignments range over Boolean valuations of the variables actually occurring in φ. Variables not in φ.vars are set to false (and do not affect the truth value by eval_eq_of_agree_on_vars).

noncomputable def NPCompleteness.BoolFormula.sharpSat (φ : BoolFormula) : ℕ

The #SAT count of φ: the number of satisfying assignments of φ. Alias for countSat.

noncomputable def NPCompleteness.SharpSAT : Set (BoolFormula × ℕ)

The #SAT language as a set of pairs ⟨φ, k⟩: #SAT = {⟨φ, k⟩ | φ has exactly k satisfying assignments} (Sipser, Lecture 25).