Parsimonious occurrence reduction for 3SAT

The existing occurrence splitter preserves the number of satisfying assignments. Each source variable has one value on every copy in its implication cycle, and numbering copies is injective. The counting problems below count only occurring variables and return zero outside their syntax. They reuse SharpSAT and the existing syntax guards rather than introducing new assignment or satisfiability semantics.

Main definitions

• Cslib.Complexity.SharpThreeSAT: model count for width-at-most-three CNF, zero otherwise.
• Cslib.Complexity.SharpThreeSATThree: model count with the additional three-occurrence bound.

Main results

• Cslib.Complexity.sharpThreeSATThree_toThreeSATThree: exact counts for the total compiler.
• Cslib.Complexity.SharpThreeSAT.mem_ThreeSAT_iff, Cslib.Complexity.SharpThreeSATThree.mem_ThreeSATThree_iff: positivity recovers the languages.
• Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree: the existing polynomial-time compiler is a parsimonious reduction.

References

The occurrence construction and its source credit are documented in ThreeSATThree. Its count preservation is an original elementary consequence of CNF.copies_agree.

def Cslib.Complexity.SharpThreeSAT (φ : Logic.PL.CNF ℕ) : ℕ

Count satisfying assignments of width-at-most-three CNF; reject other syntax with count zero. Only variables occurring in the formula are counted.

def Cslib.Complexity.SharpThreeSATThree (φ : Logic.PL.CNF ℕ) : ℕ

Count satisfying assignments of width-three, occurrence-three CNF; reject other syntax with count zero. Repetitions are literal positions, as in ThreeSATThree.syntaxCheck.

theorem Cslib.Complexity.SharpThreeSAT.mem_ThreeSAT_iff {φ : Logic.PL.CNF ℕ} : φ ∈ ThreeSAT ↔ 0 < SharpThreeSAT φ

Membership in ThreeSAT is equivalent to a positive guarded model count.

theorem Cslib.Complexity.SharpThreeSATThree.mem_ThreeSATThree_iff {φ : Logic.PL.CNF ℕ} : φ ∈ ThreeSATThree ↔ 0 < SharpThreeSATThree φ

Membership in ThreeSATThree is equivalent to a positive guarded model count.

theorem Cslib.Complexity.sharpThreeSATThree_toThreeSATThree (φ : Logic.PL.CNF ℕ) : SharpThreeSATThree (toThreeSATThree φ) = SharpThreeSAT φ

The total occurrence compiler preserves the count, including rejected inputs.

theorem Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree : ParsimoniousReducible encCNF encCNF SharpThreeSAT SharpThreeSATThree

The already-certified polynomial-time 3SAT-to-3SAT-3 compiler is parsimonious.