Model counts under compact variable numbering

First-occurrence numbering preserves the number of satisfying assignments on the variables occurring in a formula. The variable type may be infinite or empty.

Main results

• Cslib.Logic.PL.CNF.modelCount_compact: compaction preserves the model count.

References

This is an elementary counting property of the existing compaction construction.

theorem Cslib.Logic.PL.CNF.modelCount_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.compact.modelCount = φ.modelCount

First-occurrence numbering preserves the number of satisfying assignments, including for empty formulas, empty clauses, and repeated literal occurrences.