Counting the variable occurrences of a CSP instance

The variable occurrences F.vars of a CSP instance bound its other sizes. When every scope is nonempty there are at least as many occurrences as constraints (CSP.length_le_length_vars), and when every variable occurs at most Δ times there are at most Δ occurrences per variable (CSP.length_vars_le_mul_numVars). The auxiliary formula F.varCNF has one clause per constraint (CSP.length_varCNF).

Main results

• Cslib.Logic.PL.CSP.length_varCNF: F.varCNF has as many clauses as F has constraints.
• Cslib.Logic.PL.CSP.length_le_length_vars: with nonempty scopes, at least as many occurrences as constraints.
• Cslib.Logic.PL.CSP.length_vars_le_mul_numVars: at most Δ n occurrences when every one of the n variables occurs at most Δ times.

@[simp]

theorem Cslib.Logic.PL.CSP.length_varCNF {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : List.length F.varCNF = List.length F

theorem Cslib.Logic.PL.CSP.length_le_length_vars {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : ∀ c ∈ F, 1 ≤ c.2.length) : List.length F ≤ F.vars.length

An instance whose scopes are nonempty has at least as many variable occurrences as constraints.

theorem Cslib.Logic.PL.CSP.length_vars_le_mul_numVars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} {Δ : ℕ} (hΔ : ∀ (v : V), List.count v F.vars ≤ Δ) : F.vars.length ≤ Δ * F.numVars

An instance in which every variable occurs at most Δ times has at most Δ n variable occurrences, for n variables.