Counting accepting runs is parsimoniously #P-complete

The machine bridge of the counting world. The machine M_φ of a CNF instance (DescriptiveComplexity.satMachine) has exactly as many accepting runs as φ has models (DescriptiveComplexity.card_haltWalk_satMachine), so the reduction of DescriptiveComplexity.Problems.Machine.Interp is parsimonious (DescriptiveComplexity.SatTM.sharpSat_ordered_parsimonious_sharpNtmAccept). With membership (DescriptiveComplexity.sharpNtmAccept_mem_sharpP) this gives

• DescriptiveComplexity.sharpNtmAccept_sharpP_parsimoniousComplete, and
• DescriptiveComplexity.mem_sharpP_iff_le_sharpNtmAccept: a counting problem is in #P – counts the witnesses of an existential second-order sentence – exactly when it reduces parsimoniously to counting the accepting runs of a nondeterministic machine within a polynomial budget. That is the definition of #P in Valiant 1979.

Why the counts agree

The machine branches only at the guess, and it guesses only at the variables of the formula, writing “false” at every other element. So:

• an accepting run ends on the tape of the assignment it guessed, which is a model (DescriptiveComplexity.good_of_haltWalk, from the run analysis DescriptiveComplexity.sat_of_guess);
• every model has a run ending on its tape (DescriptiveComplexity.exists_haltWalk_of_good);
• two runs ending on the same tape are the same run (DescriptiveComplexity.haltWalk_ext): a truth value once written is never overwritten, so the final tape says what each guess step wrote, and away from the guess the machine is deterministic.

def DescriptiveComplexity.SatGood {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Bool) : Prop

The assignments the machine can guess and accept: true only at variables of the instance, and satisfying every clause.

Equations

• DescriptiveComplexity.SatGood ν = ((∀ (x : A), ν x = true → DescriptiveComplexity.SatVar x) ∧ ∀ (e : A), DescriptiveComplexity.SatCl e → ∃ (y : A), DescriptiveComplexity.SatLit e y (ν y))

theorem DescriptiveComplexity.symV_injective {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {v v' : Bool} {x : A} (h : symV v x = symV v' x) : v = v'

theorem DescriptiveComplexity.symV_ne_symU {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {v : Bool} {x y : A} : symV v x ≠ symU y

theorem DescriptiveComplexity.exists_haltWalk_of_good {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (h : SatGood ν) : ∃ (conf : SatV A → Config (SatV A)), (satMachine A).IsHaltWalk conf ∧ ∀ (p : SatTag × (Fin 2 → A)), MaxPos tagTupleLe SatPosn p → (conf p).tape = doneTape ν

Every model has a run: a halting walk ending on its tape.

theorem DescriptiveComplexity.good_of_haltWalk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {conf : SatV A → Config (SatV A)} (h : (satMachine A).IsHaltWalk conf) : ∃ (ν : A → Bool), SatGood ν ∧ ∀ (p : SatTag × (Fin 2 → A)), MaxPos tagTupleLe SatPosn p → (conf p).tape = doneTape ν

Every run is the run of a model: a halting walk ends on the tape of an assignment the machine can guess and accept.

theorem DescriptiveComplexity.haltWalk_ext {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {conf conf' : SatV A → Config (SatV A)} (h : (satMachine A).IsHaltWalk conf) (h' : (satMachine A).IsHaltWalk conf') {p₁ : SatV A} (hp₁ : MaxPos tagTupleLe SatPosn p₁) (htape : (conf p₁).tape = (conf' p₁).tape) : conf = conf'

Two runs ending on the same tape are the same run.

theorem DescriptiveComplexity.doneTape_injective {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {ν ν' : A → Bool} (h : doneTape ν = doneTape ν') : ν = ν'

theorem DescriptiveComplexity.card_haltWalk_satMachine {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Nat.card { conf : SatV A → Config (SatV A) // (satMachine A).IsHaltWalk conf } = Nat.card { ν : A → Bool // SatGood ν }

The machine of a CNF instance has as many accepting runs as the assignments it can guess and accept.

The machine characterization of #P

theorem DescriptiveComplexity.sharpNtmAccept_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpNTMAccept

Counting the accepting runs of a machine is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpNtmAccept_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpNTMAccept

Counting the accepting runs of a nondeterministic machine is parsimoniously #P-complete. The class of this library is defined in logic; this theorem is the bridge saying it is the machine one. Registered in the Lax archive as Lax366625.CountingRunsComplete.sharpNtmAccept_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpNtmAccept_sharpP_complete : SharpP.Complete SharpNTMAccept

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

theorem DescriptiveComplexity.mem_sharpP_iff_le_sharpNtmAccept {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) : SharpP.Mem C ↔ Nonempty (OrderedParsimoniousReduction C SharpNTMAccept)

The machine characterization of #P: a counting problem counts the witnesses of an existential second-order sentence exactly when it reduces parsimoniously to counting the accepting runs of a nondeterministic machine. Registered in the Lax archive as Lax366625.CountingRunsComplete.mem_sharpP_iff_le_sharpNtmAccept.

theorem DescriptiveComplexity.sharpNtmAccept_interreducible_sharpSat : Nonempty (OrderedParsimoniousReduction SharpNTMAccept SharpSAT) ∧ Nonempty (OrderedParsimoniousReduction SharpSAT SharpNTMAccept)

Counting accepting runs and counting models reduce to each other, parsimoniously: the counting form of the Cook–Levin correspondence.