DP, the class of differences of NP problems

The class DP (Papadimitriou & Yannakakis 1984): the problems that are the conjunction of an NP problem and a coNP one – equivalently, the difference S \ U of two NP problems, taking U := Tᶜ. Logically, and this is how the class is defined here (DescriptiveComplexity.DPDefinable), it is definability by a conjunction of a Σ₁ and a Π₁ sentence.

DP is not a level of the polynomial hierarchy, and not the same thing as NP ∩ coNP: the conjunction is of two different problems, whereas P ∈ NP ∩ coNP asks one problem to have both kinds of definition. It sits just above NP and coNP and inside the second level of the hierarchy: NP ∪ coNP ⊆ DP ⊆ Σ₂ᵖ ∩ Π₂ᵖ (DescriptiveComplexity.NP_subset_DP, DescriptiveComplexity.coNP_subset_DP, DescriptiveComplexity.DP_subset_sigmaP_two, DescriptiveComplexity.DP_subset_piP_two). The lower bounds conjoin the tautology to the other side; the upper bounds merge (∃X. φ) ∧ (∀Y. ψ) into the single alternation ∃X ∀Y. (φ ∧ ψ), which is sound in both block orders because neither kernel mentions the other's variables.

The canonical DP-complete problem, SAT-UNSAT (Papadimitriou & Yannakakis 1984), lives in DescriptiveComplexity.Problems.SatUnsat: its hardness runs the Cook–Levin discharge of the Σ₁ half and that of the complement of the Π₁ half side by side into one paired-CNF instance.

Why closure needs the order-elimination lemma

A DescriptiveComplexity.ComplexityClass must be closed under reductions, and for DP this is not inherited from the two levels it is built out of. Pulling a definition back through an ordered reduction produces a sentence over the ordered expansion, correct for every linear order; the existing closure theorems then remove the order because the problem they are given is order-invariant. Here the two halves are not: only their conjunction is, so S (I≼.Map A) really does depend on the order ≼.

The way out is to let the two halves disagree about the order and quantify it in opposite directions – existentially on the Σ side (DescriptiveComplexity.DecisionProblem.comapExOrd) and universally on the Π side (DescriptiveComplexity.DecisionProblem.comapAllOrd). Their conjunction is still equivalent to the pullback: for the forward direction every order works for both halves, and backwards the order witnessing the existential is one of those the universal covers. Each half is then definable at its level by DescriptiveComplexity.sigmaSODefinable_of_orderPull and DescriptiveComplexity.piSODefinable_of_orderPull, which are exactly the order-elimination construction stated for a sentence rather than for a reduction.

Pulling a problem back along an interpretation

def DescriptiveComplexity.DecisionProblem.comap {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {Tag : Type} {dim : ℕ} (I : FOInterpretation L L' Tag dim) (Q : DecisionProblem L') : DecisionProblem L

The problem pulled back along an interpretation: its yes-instances are the structures whose image is a yes-instance of Q. It is a decision problem because interpretations are functorial on isomorphisms (DescriptiveComplexity.FOInterpretation.mapLEquiv).

Equations

• DescriptiveComplexity.DecisionProblem.comap I Q = { Holds := fun (A : Type) (x : L.Structure A) => Q.Holds (I.Map A), iso_invariant := ⋯ }

def DescriptiveComplexity.FOInterpretation.comapReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {Tag : Type} {dim : ℕ} [Finite Tag] [Nonempty Tag] (I : FOInterpretation L L' Tag dim) (Q : DecisionProblem L') : FOReduction (DecisionProblem.comap I Q) Q

The tautological reduction: the pullback of Q reduces to Q, by the very interpretation it was pulled back along.

Equations

• I.comapReduction Q = { Tag := Tag, tagFinite := inst✝¹, tagNonempty := inst✝, dim := dim, toInterpretation := I, correct := ⋯ }

Transporting an order along an isomorphism

The two order-quantified pullbacks below are decision problems, and proving it means moving a linear order from one structure to an isomorphic one.

The two order-quantified pullbacks

theorem DescriptiveComplexity.exOrd_iso {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} {dim : ℕ} (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (Q : DecisionProblem L') {A B : Type} [L.Structure A] [L.Structure B] (e : L.Equiv A B) (h : ∃ (lo : LinearOrder A), Q.Holds (I.Map A)) : ∃ (lo : LinearOrder B), Q.Holds (I.Map B)

def DescriptiveComplexity.DecisionProblem.comapExOrd {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} {dim : ℕ} (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (Q : DecisionProblem L') [L.IsRelational] : DecisionProblem L

The pullback of Q along an ordered interpretation, with the order quantified existentially: some linear order on the instance sends it to a yes-instance of Q.

Equations

• DescriptiveComplexity.DecisionProblem.comapExOrd I Q = { Holds := fun (A : Type) (x : L.Structure A) => ∃ (lo : LinearOrder A), Q.Holds (I.Map A), iso_invariant := ⋯ }

def DescriptiveComplexity.DecisionProblem.comapAllOrd {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} {dim : ℕ} (I : FOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (Q : DecisionProblem L') [L.IsRelational] : DecisionProblem L

The pullback of Q along an ordered interpretation, with the order quantified universally: every linear order on the instance sends it to a yes-instance of Q.

Equations

• DescriptiveComplexity.DecisionProblem.comapAllOrd I Q = { Holds := fun (A : Type) (x : L.Structure A) => ∀ (lo : LinearOrder A), Q.Holds (I.Map A), iso_invariant := ⋯ }

DP definability

def DescriptiveComplexity.DPDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is DP-definable if, on nonempty finite structures, it is the conjunction of a Σ₁-definable and a Π₁-definable problem: an NP condition and a coNP one, imposed together. Equivalently, it is the difference S \ Tᶜ of two NP problems.

Equations

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

theorem DescriptiveComplexity.dpDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : DPDefinable P ↔ DPDefinable Q

DP definability only depends on the finite instances of a problem.

Closure under reductions

theorem DescriptiveComplexity.DPDefinable.of_foReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) (h : DPDefinable Q) : DPDefinable P

DP definability is closed under first-order reductions: both halves are pulled back along the interpretation.

theorem DescriptiveComplexity.DPDefinable.of_orderedReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) (h : DPDefinable Q) : DPDefinable P

DP definability is closed under ordered first-order reductions. This is where the two halves have to be allowed to disagree about the order: the Σ half asks for some linear order, the Π half for all of them, and their conjunction is again the pullback.

DP inside the second level

The Σ half's guess and the Π half's challenge become the two blocks of a single alternation. The two kernels live over different expansions of the vocabulary, so each is transported into the doubly expanded one: the head kernel by DescriptiveComplexity.soLangEmbed, the other by DescriptiveComplexity.soLangLift along LHom.sumInl, which is an expansion on a sum structure.

theorem DescriptiveComplexity.DPDefinable.sigmaSODefinable_two {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : DPDefinable P) : SigmaSODefinable 2 P

DP ⊆ Σ₂ᵖ: (∃X. φ) ∧ (∀Y. ψ) is the single alternation ∃X ∀Y. (φ ∧ ψ). Nothing has to be guessed twice – the Π kernel does not mention X, which is what makes the conjunction slide inside both quantifiers.

theorem DescriptiveComplexity.DPDefinable.piSODefinable_two {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : DPDefinable P) : PiSODefinable 2 P

DP ⊆ Π₂ᵖ, the same merge with the blocks in the other order: ∀Y ∃X. (φ ∧ ψ). Recovering the Σ half from it uses that a block always has some assignment – the constantly true one will do.

The class

noncomputable def DescriptiveComplexity.DP : ComplexityClass

The class DP (Papadimitriou & Yannakakis 1984): the conjunctions of an NP condition and a coNP one. Hardness is stated cofinally, as for the other classes of this library (DescriptiveComplexity.CofinalHard).

Equations

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

theorem DescriptiveComplexity.mem_DP_iff {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : DP.Mem P ↔ DPDefinable P

Membership in DP is exactly DP definability, by definition.

NP and coNP inside DP

Both inclusions take the other half of the conjunction to be trivial: an NP condition alone is an NP condition conjoined with the tautology, and dually.

def DescriptiveComplexity.DecisionProblem.triv (L : FirstOrder.Language) [L.IsRelational] : DecisionProblem L

The trivially true problem, the unit of conjunction.

Equations

• DescriptiveComplexity.DecisionProblem.triv L = { Holds := fun (x : Type) (x_1 : L.Structure x) => True, iso_invariant := ⋯ }

def DescriptiveComplexity.trivBlock : SOBlock

A one-variable block, to carry the tautological kernel of the trivial problem: a Σ₁ or Π₁ witness needs a block to quantify, even an idle one.

Equations

• DescriptiveComplexity.trivBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 1 }

theorem DescriptiveComplexity.NP_subset_DP : NP ⊆ DP

NP ⊆ DP: an NP condition is itself a DP condition, conjoined with the tautology. Registered in the Lax archive as Lax564036.DPInclusions.NP_subset_DP.

theorem DescriptiveComplexity.coNP_subset_DP : coNP ⊆ DP

coNP ⊆ DP, the mirror image. Registered in the Lax archive as Lax564036.DPInclusions.coNP_subset_DP.

theorem DescriptiveComplexity.DP_subset_sigmaP_two : DP ⊆ SigmaP 2

DP ⊆ Σ₂ᵖ, as an inclusion of classes. Registered in the Lax archive as Lax564036.DPInclusions.DP_subset_sigmaP_two.

theorem DescriptiveComplexity.DP_subset_piP_two : DP ⊆ PiP 2

DP ⊆ Π₂ᵖ, as an inclusion of classes: DP sits inside the second level of the hierarchy from both sides. Registered in the Lax archive as Lax564036.DPInclusions.DP_subset_piP_two.