Model counts under CNF relabelling

Relabelling preserves the count when it is injective on the occurring variables. Collisions outside that support are harmless, including when the source variable type is infinite or empty.

Main results

• Cslib.Logic.PL.CNF.modelCount_relabel_of_injOn: support-injective relabelling preserves counts.
• Cslib.Logic.PL.CNF.modelCount_relabel: globally injective relabelling preserves counts.

References

These are original elementary transport proofs for the existing occurring-variable model count.

theorem Cslib.Logic.PL.CNF.modelCount_relabel_of_injOn {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {f : V → W} (φ : CNF V) (hf : Set.InjOn f {v : V | v ∈ φ.vars}) : (relabel f φ).modelCount = φ.modelCount

Relabelling injectively on the occurring variables preserves the number of satisfying assignments. No injectivity is required outside those variables.

theorem Cslib.Logic.PL.CNF.modelCount_relabel {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {f : V → W} (hf : Function.Injective f) (φ : CNF V) : (relabel f φ).modelCount = φ.modelCount

Relabelling along an injective map preserves the number of satisfying assignments.