#SAT is parsimoniously #P-complete

The counting form of the Cook–Levin theorem: every #P-definable counting problem reduces to DescriptiveComplexity.SharpSAT by an ordered parsimonious reduction (DescriptiveComplexity.sharpSat_parsimoniousHard_of_sharpPDefinable), so #SAT is parsimoniously #P-complete (DescriptiveComplexity.sharpSat_sharpP_parsimoniousComplete).

The reduction is the Tseitin interpretation of DescriptiveComplexity.Problems.Sat.Hardness, and the reason it preserves the number of solutions is the classical one: the gate variables of a Tseitin encoding are functionally determined by the input variables (DescriptiveComplexity.Tseitin.gates_unique), and every variable of the encoding sits at a canonically padded tuple (DescriptiveComplexity.Tseitin.litSem_varCanon), so a model of the encoding is exactly an assignment of the block satisfying the kernel.

One thing has to be added to the decision reduction. A block variable at a tuple that the kernel never mentions occurs in no clause of the encoding, so it is not a variable of the CNF formula, while the witness count ranges over all assignments of the block. The interpretation DescriptiveComplexity.sharpTseitinInterp therefore adds one tautological clause R(ā) ∨ ¬R(ā) per block variable and tuple, which makes each of them occur without constraining anything.

@[reducible, inline]

abbrev DescriptiveComplexity.SharpTseitinTag {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : Type

The tags of the parsimonious Tseitin interpretation: those of the Tseitin interpretation, and one tautological clause per block variable.

Equations

• DescriptiveComplexity.SharpTseitinTag B φ = (DescriptiveComplexity.TseitinTag B φ ⊕ B.ι)

noncomputable def DescriptiveComplexity.sharpLitFml {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) (s : Bool) (tc tx : SharpTseitinTag B φ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (tseitinDim B φ))

The defining formula of satPosIn (s = true) and satNegIn (s = false): the literals of the Tseitin interpretation, and the block variable i at the tuple of its tautological clause, with both signs.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.sharpLitFml B φ s (Sum.inl tc_2) (Sum.inl tx_2) = DescriptiveComplexity.tseitinLitFml B φ s tc_2 tx_2
• DescriptiveComplexity.sharpLitFml B φ s tc tx = ⊥

noncomputable def DescriptiveComplexity.sharpTseitinInterp {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.sat (SharpTseitinTag B φ) (tseitinDim B φ)

The parsimonious Tseitin interpretation: the CNF instance of the Tseitin encoding of φ, with one tautological clause per block variable and canonically padded tuple.

Equations

• One or more equations did not get rendered due to their size.

The points of the interpreted instance

def DescriptiveComplexity.sharpOldPt {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} (e : (tseitinInterp B φ).Map A) : (sharpTseitinInterp B φ).Map A

A point of the Tseitin instance, as a point of the parsimonious one.

Equations

• DescriptiveComplexity.sharpOldPt e = (Sum.inl e.1, e.2)

def DescriptiveComplexity.tseitinVarPt {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (x : Fin (tseitinDim B φ) → A) : (tseitinInterp B φ).Map A

The propositional variable indexed by vt at the tuple x, as a point of the Tseitin instance.

Equations

• DescriptiveComplexity.tseitinVarPt vt x = (Sum.inr vt, x)

Characterization of the interpreted relations

Models of the interpreted instance are assignments of the block

theorem DescriptiveComplexity.sharp_occurs_canon {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {e : (sharpTseitinInterp B φ).Map A} (he : SatOccurs ((sharpTseitinInterp B φ).Map A) e) : ∃ (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (x : Fin (tseitinDim B φ) → A), e = sharpOldPt (tseitinVarPt vt x) ∧ Tseitin.VarCanon vt x

Variables of the interpreted instance: an element occurring in a clause is a propositional variable of the encoding at a tuple canonical for it.

theorem DescriptiveComplexity.sharp_occurs_block {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] (i : B.ι) {u : Fin (tseitinDim B φ) → A} (hu : Canon (B.arity i) u) : SatOccurs ((sharpTseitinInterp B φ).Map A) (sharpOldPt (tseitinVarPt (Sum.inl i) u))

Every block variable at a canonically padded tuple is a variable of the interpreted instance: it occurs in its tautological clause.

def DescriptiveComplexity.sharpVal {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} [L.Structure A] (μ : B.Assignment A) (e : (sharpTseitinInterp B φ).Map A) : Prop

The truth assignment of the interpreted instance determined by an assignment of the block, before its restriction to the variables of the instance.

Equations

• DescriptiveComplexity.sharpVal μ (Sum.inl (Sum.inr vt), x) = DescriptiveComplexity.tseitinVal B φ μ vt x
• DescriptiveComplexity.sharpVal μ e = False

theorem DescriptiveComplexity.sharpVal_varPt {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} [L.Structure A] (μ : B.Assignment A) (vt : B.ι ⊕ (m : ℕ) × Tseitin.NodeAt φ m) (x : Fin (tseitinDim B φ) → A) : sharpVal μ (sharpOldPt (tseitinVarPt vt x)) ↔ tseitinVal B φ μ vt x

theorem DescriptiveComplexity.sharp_old_clauses {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {ν : (sharpTseitinInterp B φ).Map A → Prop} (hν : ∀ (c : (sharpTseitinInterp B φ).Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : (sharpTseitinInterp B φ).Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν x) (c : (tseitinInterp B φ).Map A) (hc : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]) : ∃ (x : (tseitinInterp B φ).Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν (sharpOldPt x) ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν (sharpOldPt x)

The clauses of the Tseitin instance hold under a truth assignment of the parsimonious instance satisfying all its clauses.

theorem DescriptiveComplexity.sharpVal_clauses {L : FirstOrder.Language} {B : SOBlock} {φ : (L.sum B.lang).Sentence} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (μ : B.Assignment A) (hμ : Tseitin.RealizeWith μ φ finZeroElim) (c : (sharpTseitinInterp B φ).Map A) (hc : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]) : ∃ (x : (sharpTseitinInterp B φ).Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ sharpVal μ x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬sharpVal μ x

The truth assignment determined by an assignment of the block realizing the kernel satisfies every clause of the parsimonious instance.

noncomputable def DescriptiveComplexity.sharpModelEquiv {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) (A : Type) [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) : { ν : (sharpTseitinInterp B φ).Map A → Prop // SatModel ((sharpTseitinInterp B φ).Map A) ν } ≃ { μ : B.Assignment A // Tseitin.RealizeWith μ φ finZeroElim }

Models of the interpreted instance are the assignments of the block realizing the kernel, bijectively: a model induces a block assignment through canonical padding, and is recovered from it because gates determine the position variables and every variable of the instance sits at a canonical tuple.

Equations

• One or more equations did not get rendered due to their size.

Correctness of the reduction

theorem DescriptiveComplexity.sharpSat_sharpTseitin {L : FirstOrder.Language} (B : SOBlock) (φ : (L.sum B.lang).Sentence) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : SharpSAT.Count ((sharpTseitinInterp B φ).Map A) = witnessCount B φ A

Correctness of the parsimonious Tseitin interpretation: the interpreted CNF instance has as many models as the kernel has witnesses.

The counting Cook–Levin theorem

def DescriptiveComplexity.orderCollapse (L : FirstOrder.Language) : (L.sum FirstOrder.Language.order).sum FirstOrder.Language.order →ᴸ L.sum FirstOrder.Language.order

The vocabulary map identifying the two order symbols of a doubly ordered expansion. The kernel of a #P definition reads the order of the instance as part of its vocabulary, and the Tseitin interpretation reads it again to pad its tuples; both are the one order of the instance.

Equations

• DescriptiveComplexity.orderCollapse L = (FirstOrder.Language.LHom.id (L.sum FirstOrder.Language.order)).sumElim FirstOrder.Language.LHom.sumInr

instance DescriptiveComplexity.orderCollapse_isExpansionOn {L : FirstOrder.Language} (A : Type) [L.Structure A] [LinearOrder A] : (orderCollapse L).IsExpansionOn A

noncomputable def DescriptiveComplexity.sharpTseitinReduction {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (B : SOBlock) (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (hφ : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], C.Count A = witnessCount B φ A) : OrderedParsimoniousReduction C SharpSAT

The generic parsimonious Tseitin reduction: an ordered parsimonious reduction to #SAT from any counting problem that counts, on nonempty finite ordered structures, the witnesses of an existential second-order sentence.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpSat_parsimoniousHard_of_sharpPDefinable {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (hC : SharpPDefinable C) : Nonempty (OrderedParsimoniousReduction C SharpSAT)

The hardness half of the counting Cook–Levin theorem: every #P-definable counting problem admits an ordered parsimonious reduction to #SAT.

theorem DescriptiveComplexity.sharpSat_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpSAT

#SAT is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpSat_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpSAT

#SAT is parsimoniously #P-complete: the counting form of the Cook–Levin theorem (Valiant 1979). Membership is DescriptiveComplexity.sharpSat_mem_sharpP; hardness is the generic parsimonious Tseitin reduction DescriptiveComplexity.sharpTseitinReduction. Registered in the Lax archive as Lax366625.SharpSatComplete.sharpSat_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpSat_sharpP_complete : SharpP.Complete SharpSAT

SharpSAT is #P-complete: parsimoniously, hence under subtractive reductions.