Generic linear-witness interface for the SAT guess-and-verify machine #
The concrete machine in SAT.Internal.GuessVerify only assumes that guessed
witnesses have length at most |x| + 1; most of its machine proof is already
parametric in the verifier language. This module packages those generic
theorems for any relation with that same linear bound.
Main result #
SAT.language_mem_NP_of_linear_witness_verifierP_direct-- a linearly balanced relation with a polynomial-time paired verifier defines an NP language
theorem
Complexity.SAT.linearGuessVerify_acceptsInTime_of_mem
{k : ℕ}
{R : List Bool → List Bool → Prop}
{L : Language}
(hbound : ∀ (x y : List Bool), R x y → y.length ≤ x.length + 1)
(hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), R x y)
(M : TM k)
{f : ℕ → ℕ}
(hM : M.DecidesInTime (pairLang R) f)
(x : List Bool)
(hx : x ∈ L)
:
(satGuessVerifyNTM M).AcceptsInTime x (satGuessVerifyTime f x.length)
A member with a linearly bounded witness has an accepting run of the generic guess-and-verify machine.
theorem
Complexity.SAT.linearGuessVerify_not_acceptsInTime_of_not_mem
{k : ℕ}
{R : List Bool → List Bool → Prop}
{L : Language}
(hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), R x y)
(M : TM k)
{f : ℕ → ℕ}
(hM : M.DecidesInTime (pairLang R) f)
(x : List Bool)
(hx : x ∉ L)
:
¬(satGuessVerifyNTM M).AcceptsInTime x (satGuessVerifyTime f x.length)
A nonmember has no accepting run of the generic guess-and-verify machine within its uniform time bound.
theorem
Complexity.SAT.linearGuessVerify_decidesInTime
{k : ℕ}
{R : List Bool → List Bool → Prop}
{L : Language}
(hbound : ∀ (x y : List Bool), R x y → y.length ≤ x.length + 1)
(hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), R x y)
(M : TM k)
{f : ℕ → ℕ}
(hM : M.DecidesInTime (pairLang R) f)
:
(satGuessVerifyNTM M).DecidesInTime L (satGuessVerifyTime f)
The generic SAT guess-and-verify machine decides any language described
by a linearly bounded relation whose paired language is decided by M.
theorem
Complexity.SAT.language_mem_NP_of_linear_witness_verifierP_direct
{R : List Bool → List Bool → Prop}
{L : Language}
(hbound : ∀ (x y : List Bool), R x y → y.length ≤ x.length + 1)
(hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), R x y)
(hverify : pairLang R ∈ P)
:
A relation with witnesses bounded by |x| + 1 and a verifier in P
places its existential language in NP.