FewP is in SPP

FewP ⊆ SPP Köbler, Schöning, Toda and Torán, in the gap formulation of Fenner, Fortnow and Kurtz. For a problem in FewP, let T be the set of certificates of length len accepted on an instance, of size m ≤ q. The subsets U ⊆ T cancel in pairs by parity: ∑ U ⊆ T, (-1) ^ |U| = (1 - 1) ^ m is 1 when m = 0 and 0 otherwise. Every subset has at most q elements, so it is listed, in increasing order, in q slots of len + 1 bits, each a flag followed by a certificate. The numbers E and O of such listings of the subsets of even and of odd size are counted by polynomial-time verifiers, so they are in #P, and 1 + O - E is a GapP function equal to 1 on members and 0 on the other instances.

The listings

A word of q slots is read from the left (Cslib.Complexity.SortedSubsets.step). A flagged slot lists its certificate, which must be accepted, come before every empty slot and exceed the last certificate listed in binary value; an empty slot must hold only bits false. The well-formed words are exactly the increasing listings of the subsets of T with at most q elements. The proof does not construct this bijection; it shows by induction on the number of slots that the well-formed words, counted with the sign of the parity of their number of certificates, sum to the sign of the starting state when no accepted certificate is above the last one listed, and to 0 otherwise (Cslib.Complexity.SortedSubsets.signedSum_eq): a first empty slot leaves one well-formed completion, and a first certificate c contributes, by induction, the opposite sign exactly when c is the largest certificate above the last one listed.

Main definitions

• Cslib.Complexity.SortedSubsets.step: read one slot of a listing.
• Cslib.Complexity.SortedSubsets.verifier: the verifier counting the listings of a given parity.

Main results

• Cslib.Complexity.SortedSubsets.signedSum_eq: the signed count of the listings.
• Cslib.Complexity.SortedSubsets.computableInPolyTime_verifier: the verifier is polynomial-time.
• Cslib.Complexity.FewP_subset_SPP: FewP ⊆ SPP.

References

• J. Köbler, U. Schöning, S. Toda, J. Torán, Turing machines with few accepting computations and low sets for PP
• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes

@[reducible, inline]

abbrev Cslib.Complexity.SortedSubsets.State : Type

The state of a scan of slots: whether the slots read so far are well formed, the parity of the number of certificates listed, whether an empty slot has been read, whether a certificate has been listed, and the last certificate listed.

def Cslib.Complexity.SortedSubsets.init : State

The state before any slot is read.

def Cslib.Complexity.SortedSubsets.step (acc : List Bool → Bool) (s : State) (slot : List Bool) : State

Read one slot, a flag bit followed by a certificate. A flagged slot lists its certificate, which must be accepted by acc, come before every empty slot, and exceed the last certificate listed in binary value; an empty slot must hold only bits false.

def Cslib.Complexity.SortedSubsets.accepts (b : Bool) (s : State) : Bool

A final state is accepted for the parity b when it is well formed and lists a number of certificates of parity b.

def Cslib.Complexity.SortedSubsets.sign (s : State) : ℤ

The sign of a final state: 0 if malformed, otherwise 1 or -1 by the parity of the number of certificates listed.

def Cslib.Complexity.SortedSubsets.above (acc : List Bool → Bool) (len : ℕ) (s : State) : Finset (Fin len → Bool)

The certificates of length len accepted by acc that may be listed after the state s: above the last certificate listed, if any.

def Cslib.Complexity.SortedSubsets.signedSum (acc : List Bool → Bool) (len k : ℕ) (s : State) : ℤ

The words of k slots of len + 1 bits read from the state s, counted with the sign of the final state.

theorem Cslib.Complexity.SortedSubsets.signedSum_eq {acc : List Bool → Bool} {len : ℕ} (k : ℕ) (s : State) (hk : s.1 = true → s.2.2.1 = false → (above acc len s).card ≤ k) : signedSum acc len k s = if s.2.2.1 = false ∧ (above acc len s).Nonempty then 0 else sign s

The signed count of the listings. From a well-formed state, the words of k slots, counted with the sign of the parity of the certificates listed, sum to the sign of the state when an empty slot has been read or no accepted certificate is above the last one listed, and to 0 otherwise, provided at most k accepted certificates are above it.

The verifiers

def Cslib.Complexity.SortedSubsets.verifier {α : Type} (enc : α ↪ List Bool) (p q : Polynomial ℕ) (V : α × List Bool → Bool) (b : Bool) (x : α × List Bool) : Bool

The verifier counting the listings of parity b: on an instance a, the certificate, read as q slots of len + 1 bits, where len = p (enc a).length, is a well-formed increasing listing of certificates of length len accepted by V with a number of certificates of parity b.

theorem Cslib.Complexity.SortedSubsets.computableInPolyTime_verifier {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (p q : Polynomial ℕ) (b : Bool) : Turing.MultiTapeTM.ComputableInPolyTime (verifier enc p q V b) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The verifiers are polynomial-time.

theorem Cslib.Complexity.FewP_subset_SPP {α : Type} {enc : α ↪ List Bool} : FewP enc ⊆ SPP enc

FewP ⊆ SPP Köbler, Schöning, Toda and Torán, Fenner, Fortnow and Kurtz. For a problem in FewP whose instances have at most q accepted certificates, the numbers E and O of increasing listings, in q slots, of sets of accepted certificates of even and of odd size are in #P, and 1 + O - E, in GapP, is 1 on members and 0 on the other instances.