NP membership from witness relations

Membership in Cslib.Complexity.NP asks for a verifier whose certificates have length exactly p (enc a).length. Problems are usually given by a witness relation instead: a belongs to the problem when some witness b with R a b exists, the witnesses of a member can be chosen of polynomial length, and R is decidable in polynomial time Papadimitriou, Proposition 9.1. This file turns such relations into membership in NP, handling the exact-length convention in one place.

A certificate is a witness prefix padded with false to the required length, and the verifier ignores the padding (Cslib.Complexity.IsVerifier.of_padding). Four kinds of witnesses are supported:

• witnesses b : β with an encoding encW that has a decoder Turing.MultiTapeTM.Decoder (Cslib.Complexity.mem_NP_of_witness): the certificate is frame (encW b) followed by padding. The verifier Cslib.Complexity.witnessVerifier decodes the framed prefix of the certificate, re-encodes the decoded witness to reject malformed certificates, and checks the witness (Cslib.Complexity.witnessVerifier_eq_true_iff). The decoder is what makes the parsing polynomial-time: a check that is polynomial-time on encoded witnesses says nothing about words that encode no witness;
• sets of candidates from a list computed from the instance (Cslib.Complexity.mem_NP_of_subsetWitness): bit i of the certificate selects the i-th candidate at its first occurrence (Cslib.Complexity.selectDistinct), missing bits are false, and bits beyond the candidates are ignored;
• sub-multisets of a list of entries computed from the instance (Cslib.Complexity.mem_NP_of_subMultisetWitness): bit i of the certificate selects the i-th entry (Cslib.Complexity.maskSelect), so a value occurring several times may be selected several times. Subset sum, partition and knapsack use these;
• bit strings read with default false, directly through IsVerifier.of_padding, as for the assignments of SAT.

NP is also closed under polynomial-time reductions (Cslib.Complexity.PolyTimeReducible.mem_NP, the unrelativized counterpart of Cslib.Complexity.PolyTimeReducible.mem_NPWithOracle). Certificates for the original instance have a length polynomial in its own length, while the verifier of the target expects a length determined by the reduced instance, so the verifier reads only that prefix of the certificate (Cslib.Complexity.exists_truncated_verifier), and List.exists_length_eq_take_iff matches the two certificate quantifiers.

For verifiers on concatenated strings, Cslib.Complexity.mem_NP_setOf_exists_append places the pairs (a, u) admitting an accepted suffix of length q (enc a).length in NP. This is the inner existential quantifier used in the Karp–Lipton argument.

Main definitions

• Cslib.Complexity.witnessVerifier: the verifier of a witness relation, parsing certificates with a decoder.
• Cslib.Complexity.subsetVerifier: the verifier of a subset problem, selecting candidates by a mask (Cslib.Complexity.selectDistinct).
• Cslib.Complexity.maskVerifier: the verifier of a sub-multiset problem, selecting entries by a mask (Cslib.Complexity.maskSelect).
• Cslib.Complexity.encWithEntries: an instance paired with selected entries, the input of the checks of both kinds of verifier.

Main results

• Cslib.Complexity.witnessVerifier_eq_true_iff: the witness verifier accepts exactly a framed encoded witness that passes the check, followed by any bits.
• Cslib.Complexity.isVerifier_witnessVerifier, Cslib.Complexity.mem_NP_of_witness: a relation with polynomially short witnesses decided in polynomial time defines a problem in NP.
• Cslib.Complexity.mem_NP_of_check: the same for a problem given by a sound check under which every member has a short accepted witness.
• Cslib.Complexity.isVerifier_subsetVerifier, Cslib.Complexity.mem_NP_of_subsetWitness: subset problems over polynomial-time candidate lists with polynomial-time checks are in NP.
• Cslib.Complexity.isVerifier_maskVerifier, Cslib.Complexity.mem_NP_of_subMultisetWitness: the same for sub-multisets of polynomial-time lists of entries.
• Cslib.Complexity.PolyTimeReducible.mem_NP: NP is closed under polynomial-time reductions.
• Cslib.Complexity.mem_NP_setOf_exists_append: a polynomially bounded suffix accepted by a polynomial-time verifier defines a problem in NP on pairs.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• C. H. Papadimitriou, Computational Complexity

Witnesses parsed by a decoder

def Cslib.Complexity.witnessVerifier {α β : Type} {encW : β ↪ List Bool} (D : Turing.MultiTapeTM.Decoder encW) (check : α × β → Bool) (x : α × List Bool) : Bool

The verifier of the witness relation decided by check. It decodes the framed prefix of the certificate with D, rejects the certificate unless it starts with the framed encoding of the decoded witness, and checks that witness.

theorem Cslib.Complexity.witnessVerifier_eq_true_iff {α β : Type} {encW : β ↪ List Bool} {D : Turing.MultiTapeTM.Decoder encW} {check : α × β → Bool} {a : α} {w : List Bool} : witnessVerifier D check (a, w) = true ↔ ∃ (b : β) (v : List Bool), w = Turing.MultiTapeTM.frame (encW b) ++ v ∧ check (a, b) = true

Malformed certificates are rejected. witnessVerifier D check accepts exactly the certificates that consist of the framed encoding of a witness accepted by check, followed by any bits.

@[simp]

theorem Cslib.Complexity.witnessVerifier_frame_append {α β : Type} {encW : β ↪ List Bool} (D : Turing.MultiTapeTM.Decoder encW) (check : α × β → Bool) (a : α) (b : β) (v : List Bool) : witnessVerifier D check (a, Turing.MultiTapeTM.frame (encW b) ++ v) = check (a, b)

A certificate framing the encoding of a witness, followed by any bits, is checked as that witness.

theorem Cslib.Complexity.isVerifier_witnessVerifier {α β : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {encW : β ↪ List Bool} (D : Turing.MultiTapeTM.Decoder encW) {check : α × β → Bool} {R : α → β → Prop} (hR : ∀ (a : α) (b : β), check (a, b) = true ↔ R a b) (hp : ∀ (a : α) (b : β), R a b → ∃ (b' : β), R a b' ∧ (encW b').length ≤ Polynomial.eval (enc a).length p) : IsVerifier enc (2 * p + 1) (witnessVerifier D check) {a : α | ∃ (b : β), R a b}

Witness relations. If check decides R and every member has a witness whose encoding has length at most p (enc a).length, then witnessVerifier D check verifies {a | ∃ b, R a b} with certificates of length 2 * p + 1: a framed encoded witness, followed by padding.

theorem Cslib.Complexity.computableInPolyTime_witnessVerifier {α β : Type} {enc : α ↪ List Bool} {encW : β ↪ List Bool} (D : Turing.MultiTapeTM.Decoder encW) {check : α × β → Bool} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (Turing.MultiTapeTM.encPair enc encW) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (witnessVerifier D check) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The verifier of a witness relation is polynomial-time when its check is.

theorem Cslib.Complexity.mem_NP_of_witness {α β : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {encW : β ↪ List Bool} (D : Turing.MultiTapeTM.Decoder encW) {check : α × β → Bool} {R : α → β → Prop} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (Turing.MultiTapeTM.encPair enc encW) Turing.MultiTapeTM.encBool) (hR : ∀ (a : α) (b : β), check (a, b) = true ↔ R a b) (hp : ∀ (a : α) (b : β), R a b → ∃ (b' : β), R a b' ∧ (encW b').length ≤ Polynomial.eval (enc a).length p) : {a : α | ∃ (b : β), R a b} ∈ NP enc

NP membership from a witness relation Papadimitriou, Proposition 9.1. If check decides the relation R in polynomial time, the witness encoding has a decoder, and every member has a witness whose encoding has length at most p (enc a).length, then {a | ∃ b, R a b} is in NP.

theorem Cslib.Complexity.mem_NP_of_check {α β : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {A : Set α} {encW : β ↪ List Bool} (D : Turing.MultiTapeTM.Decoder encW) {check : α × β → Bool} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (Turing.MultiTapeTM.encPair enc encW) Turing.MultiTapeTM.encBool) (sound : ∀ (a : α) (b : β), check (a, b) = true → a ∈ A) (complete : ∀ a ∈ A, ∃ (b : β), check (a, b) = true ∧ (encW b).length ≤ Polynomial.eval (enc a).length p) : A ∈ NP enc

NP membership from a sound and complete check. If check accepts a witness only for members of A, and every member has a witness accepted by check whose encoding has length at most p (enc a).length, then A is in NP. This is mem_NP_of_witness for the relation check (a, b) = true, stated for the problem A itself.

@[reducible, inline]

abbrev Cslib.Complexity.encWithEntries {α γ : Type} (enc : α ↪ List Bool) (encγ : γ ↪ List Bool) : α × List γ ↪ List Bool

An instance paired with a list of selected entries, the input of the check of a subset or mask verifier: the encoded instance, framed, followed by the entries, each framed.

Subset witnesses

theorem Cslib.Complexity.computableInPolyTime_selectDistinct {γ : Type} [DecidableEq γ] (encγ : γ ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : List γ × List Bool) => selectDistinct x.1 x.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList encγ) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList encγ)

Selecting the entries of a list from a mask is polynomial-time.

def Cslib.Complexity.subsetVerifier {α γ : Type} [DecidableEq γ] (vs : α → List γ) (check : α × List γ → Bool) (x : α × List Bool) : Bool

The verifier of a subset problem over the candidates vs a: select candidates by the certificate mask (selectDistinct) and check the selected list.

theorem Cslib.Complexity.isVerifier_subsetVerifier {α γ : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} [DecidableEq γ] {vs : α → List γ} (hvs : ∀ (a : α), (vs a).length ≤ Polynomial.eval (enc a).length p) {check : α × List γ → Bool} {P : α → Finset γ → Prop} (hP : ∀ (a : α) (l : List γ), l.Nodup → (∀ v ∈ l, v ∈ vs a) → (check (a, l) = true ↔ P a l.toFinset)) : IsVerifier enc p (subsetVerifier vs check) {a : α | ∃ (S : Finset γ), (∀ v ∈ S, v ∈ vs a) ∧ P a S}

Subset witnesses. Let the candidates vs a be at most p (enc a).length many, and let check decide P a on the duplicate-free lists of candidates. Then subsetVerifier vs check verifies the problem of having a set S of candidates with P a S, with certificates of length p: the mask of S, followed by padding.

theorem Cslib.Complexity.computableInPolyTime_subsetVerifier {α γ : Type} {enc : α ↪ List Bool} [DecidableEq γ] {encγ : γ ↪ List Bool} {vs : α → List γ} (hvs : Turing.MultiTapeTM.ComputableInPolyTime vs enc (Turing.MultiTapeTM.encList encγ)) {check : α × List γ → Bool} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (encWithEntries enc encγ) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (subsetVerifier vs check) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The verifier of a subset problem is polynomial-time when the candidates and the check are.

theorem Cslib.Complexity.mem_NP_of_subsetWitness {α γ : Type} {enc : α ↪ List Bool} [DecidableEq γ] {encγ : γ ↪ List Bool} {vs : α → List γ} (hvs : Turing.MultiTapeTM.ComputableInPolyTime vs enc (Turing.MultiTapeTM.encList encγ)) {check : α × List γ → Bool} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (encWithEntries enc encγ) Turing.MultiTapeTM.encBool) {P : α → Finset γ → Prop} (hP : ∀ (a : α) (l : List γ), l.Nodup → (∀ v ∈ l, v ∈ vs a) → (check (a, l) = true ↔ P a l.toFinset)) : {a : α | ∃ (S : Finset γ), (∀ v ∈ S, v ∈ vs a) ∧ P a S} ∈ NP enc

NP membership of subset problems. If the candidates vs a and the check of the selected candidates are polynomial-time, and check decides P a on duplicate-free lists of candidates, then having a set S of candidates with P a S is in NP.

Mask witnesses

theorem Cslib.Complexity.computableInPolyTime_maskSelect {γ : Type} (encγ : γ ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : List γ × List Bool) => maskSelect x.1 x.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList encγ) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList encγ)

Selecting the entries of a list by a mask (maskSelect) is polynomial-time.

def Cslib.Complexity.maskVerifier {α γ : Type} (items : α → List γ) (check : α × List γ → Bool) (x : α × List Bool) : Bool

The verifier of a sub-multiset problem over the entries items a: select entries by the certificate mask (maskSelect) and check the selected list.

theorem Cslib.Complexity.isVerifier_maskVerifier {α γ : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {items : α → List γ} (hitems : ∀ (a : α), (items a).length ≤ Polynomial.eval (enc a).length p) {check : α × List γ → Bool} {P : α → Multiset γ → Prop} (hP : ∀ (a : α) (l : List γ), l.Sublist (items a) → (check (a, l) = true ↔ P a ↑l)) : IsVerifier enc p (maskVerifier items check) {a : α | ∃ s ≤ ↑(items a), P a s}

Sub-multiset witnesses. Let the entries items a be at most p (enc a).length many, and let check decide P a on the sublists of the entries. Then maskVerifier items check verifies the problem of having a sub-multiset s of the entries with P a s, with certificates of length p: a mask selecting s, padded with false. Unlike isVerifier_subsetVerifier, a repeated entry may be selected repeatedly.

theorem Cslib.Complexity.computableInPolyTime_maskVerifier {α γ : Type} {enc : α ↪ List Bool} {encγ : γ ↪ List Bool} {items : α → List γ} (hitems : Turing.MultiTapeTM.ComputableInPolyTime items enc (Turing.MultiTapeTM.encList encγ)) {check : α × List γ → Bool} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (encWithEntries enc encγ) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (maskVerifier items check) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The verifier of a sub-multiset problem is polynomial-time when the entries and the check are.

theorem Cslib.Complexity.mem_NP_of_subMultisetWitness {α γ : Type} {enc : α ↪ List Bool} {encγ : γ ↪ List Bool} {items : α → List γ} (hitems : Turing.MultiTapeTM.ComputableInPolyTime items enc (Turing.MultiTapeTM.encList encγ)) {check : α × List γ → Bool} (hcheck : Turing.MultiTapeTM.ComputableInPolyTime check (encWithEntries enc encγ) Turing.MultiTapeTM.encBool) {P : α → Multiset γ → Prop} (hP : ∀ (a : α) (l : List γ), l.Sublist (items a) → (check (a, l) = true ↔ P a ↑l)) : {a : α | ∃ s ≤ ↑(items a), P a s} ∈ NP enc

NP membership of sub-multiset problems. If the entries items a and the check of the selected entries are polynomial-time, and check decides P a on the sublists of the entries, then having a sub-multiset s of the entries with P a s is in NP.

Closure under reductions

theorem Cslib.Complexity.PolyTimeReducible.mem_NP {α β : Type} {enc : α ↪ List Bool} {A : Set α} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ NP encB) : A ∈ NP enc

NP is closed under polynomial-time reductions. The verifier of A runs the verifier of B on the reduced instance and on the prefix of the certificate whose length the verifier of B expects. For the oracle classes, see Cslib.Complexity.PolyTimeReducible.mem_NPWithOracle.

theorem Cslib.Complexity.PolyTimeReducible.mem_coNP {α β : Type} {enc : α ↪ List Bool} {A : Set α} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ coNP encB) : A ∈ coNP enc

coNP is closed under polynomial-time reductions.

The inner quantifier

theorem Cslib.Complexity.mem_NP_setOf_exists_append {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (q : Polynomial ℕ) : {y : α × List Bool | ∃ (v : List Bool), v.length = Polynomial.eval (enc y.1).length q ∧ V (y.1, y.2 ++ v) = true} ∈ NP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)

The inner quantifier of a Π₂ verifier is in NP. For a polynomial-time V, the pairs (a, u) for which V accepts (a, u ++ v) for some v of length q (enc a).length form a problem in NP, for the encoding of pairs.