SAT-UNSAT, the canonical DP problem

SAT-UNSAT (Papadimitriou & Yannakakis 1984): given two CNF formulas, is the first satisfiable and the second not? It is the prototypical problem of DescriptiveComplexity.DP, the class of differences of NP problems, and it wears its DP definition on its sleeve – one half is an NP condition, the other a coNP one, and they are imposed on disjoint parts of the vocabulary.

The vocabulary

An instance carries the two formulas side by side: Language.satPair is two copies of Language.sat, one per side. Both live on the same universe – there is no need to keep the two formulas' variables apart, since each side's clauses only mention their own occurrence relations, and a truth assignment for one side is free to do as it likes on the other side's variables.

What is here, and what is not

The vocabulary, the semantics and isomorphism-invariance, and the three problems: DescriptiveComplexity.SATUNSAT itself together with its two halves DescriptiveComplexity.SatFirst (an NP condition) and DescriptiveComplexity.UnsatSecond (a coNP one), which are what a DP definition of it will conjoin. Satisfiability of a side is stated once, parameterized by the triple of relation symbols to read (DescriptiveComplexity.SatWith), since the two sides differ only in that.

Membership in DP (DescriptiveComplexity.satUnsat_mem_DP) is proved without writing a single new kernel: each side is projected onto a plain Language.sat instance by a one-dimensional, single-tag interpretation (DescriptiveComplexity.sideInterp), so SatFirst reduces to SAT and SatSecond does too; Σ₁-definability of the first half and Π₁-definability of the second then come from DescriptiveComplexity.sat_sigmaSODefinable by closure of the levels under FO reductions, the second after complementing the reduction.

DP-hardness is in DescriptiveComplexity.Problems.SatUnsat.Hardness (DescriptiveComplexity.satUnsat_hard_of_dpDefinable, whence DescriptiveComplexity.SATUNSAT_DP_complete): the Cook–Levin discharge of the Σ₁ half and that of the complement of the Π₁ half, run side by side into a single paired instance. The lemma below on satisfiability along a clause-covering embedding is the step it needs.

inductive FirstOrder.Language.satPairRel : ℕ → Type

Relation symbols of the language of pairs of CNF instances: two copies of Language.satRel, one per side.

• isClause₁ : satPairRel 1

  isClause₁ c: c is a clause of the first formula.

• posIn₁ : satPairRel 2

  posIn₁ c x: x occurs positively in the first formula's clause c.

• negIn₁ : satPairRel 2

  negIn₁ c x: x occurs negatively in the first formula's clause c.

• isClause₂ : satPairRel 1

  isClause₂ c: c is a clause of the second formula.

• posIn₂ : satPairRel 2

  posIn₂ c x: x occurs positively in the second formula's clause c.

• negIn₂ : satPairRel 2

  negIn₂ c x: x occurs negatively in the second formula's clause c.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqSatPairRel {a✝ : ℕ} : DecidableEq (satPairRel a✝)

Equations

• FirstOrder.Language.instDecidableEqSatPairRel = FirstOrder.Language.instDecidableEqSatPairRel.decEq

def FirstOrder.Language.instDecidableEqSatPairRel.decEq {a✝ : ℕ} (x✝ x✝¹ : satPairRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

def FirstOrder.Language.satPair : Language

The relational vocabulary of pairs of CNF instances.

Equations

• FirstOrder.Language.satPair = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.satPairRel }

instance FirstOrder.Language.instIsRelationalSatPair : Language.satPair.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.spIsCl₁ : Language.satPair.Relations 1

“Is a clause of the first formula”.

Equations

• FirstOrder.Language.spIsCl₁ = FirstOrder.Language.satPairRel.isClause₁

@[reducible, inline]

abbrev FirstOrder.Language.spPos₁ : Language.satPair.Relations 2

“Occurs positively in”, first formula.

Equations

• FirstOrder.Language.spPos₁ = FirstOrder.Language.satPairRel.posIn₁

@[reducible, inline]

abbrev FirstOrder.Language.spNeg₁ : Language.satPair.Relations 2

“Occurs negatively in”, first formula.

Equations

• FirstOrder.Language.spNeg₁ = FirstOrder.Language.satPairRel.negIn₁

@[reducible, inline]

abbrev FirstOrder.Language.spIsCl₂ : Language.satPair.Relations 1

“Is a clause of the second formula”.

Equations

• FirstOrder.Language.spIsCl₂ = FirstOrder.Language.satPairRel.isClause₂

@[reducible, inline]

abbrev FirstOrder.Language.spPos₂ : Language.satPair.Relations 2

“Occurs positively in”, second formula.

Equations

• FirstOrder.Language.spPos₂ = FirstOrder.Language.satPairRel.posIn₂

@[reducible, inline]

abbrev FirstOrder.Language.spNeg₂ : Language.satPair.Relations 2

“Occurs negatively in”, second formula.

Equations

• FirstOrder.Language.spNeg₂ = FirstOrder.Language.satPairRel.negIn₂

Satisfiability of one side

def DescriptiveComplexity.SatWith (A : Type) [FirstOrder.Language.satPair.Structure A] (isCl : FirstOrder.Language.satPair.Relations 1) (pos neg : FirstOrder.Language.satPair.Relations 2) : Prop

Satisfiability of the side of the instance read by the given triple of symbols: some assignment of truth values makes every clause of that side contain a true literal. Both sides of SAT-UNSAT are instances of this.

Equations

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

theorem DescriptiveComplexity.satWith_iso {A B : Type} [FirstOrder.Language.satPair.Structure A] [FirstOrder.Language.satPair.Structure B] (e : FirstOrder.Language.satPair.Equiv A B) (isCl : FirstOrder.Language.satPair.Relations 1) (pos neg : FirstOrder.Language.satPair.Relations 2) : SatWith A isCl pos neg ↔ SatWith B isCl pos neg

Satisfiability of a side is isomorphism-invariant.

def DescriptiveComplexity.SatFirst : DecisionProblem FirstOrder.Language.satPair

The first formula of the pair is satisfiable: the NP half of SAT-UNSAT.

Equations

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

def DescriptiveComplexity.UnsatSecond : DecisionProblem FirstOrder.Language.satPair

The second formula of the pair is unsatisfiable: the coNP half.

Equations

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

def DescriptiveComplexity.SATUNSAT : DecisionProblem FirstOrder.Language.satPair

SAT-UNSAT: the first formula of the pair is satisfiable and the second is not.

Equations

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

Reading one side as a plain CNF instance

Rather than restate SAT's Σ₁ kernel for a pair of formulas, each side is projected onto a plain Language.sat instance by a one-dimensional, single-tag interpretation. Definability of both halves is then inherited from DescriptiveComplexity.sat_sigmaSODefinable by closure under FO reductions – no new kernel, and no second copy of its realization proof.

def DescriptiveComplexity.sideInterp (isCl : FirstOrder.Language.satPair.Relations 1) (pos neg : FirstOrder.Language.satPair.Relations 2) : FOInterpretation FirstOrder.Language.satPair FirstOrder.Language.sat Unit 1

The interpretation reading the side given by a triple of symbols as a plain CNF instance: same universe, the three relations renamed.

Equations

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

@[simp]

theorem DescriptiveComplexity.sideInterp_isClause {A : Type} [FirstOrder.Language.satPair.Structure A] (isCl : FirstOrder.Language.satPair.Relations 1) (pos neg : FirstOrder.Language.satPair.Relations 2) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![((), w)] ↔ FirstOrder.Language.Structure.RelMap isCl ![w 0]

@[simp]

theorem DescriptiveComplexity.sideInterp_posIn {A : Type} [FirstOrder.Language.satPair.Structure A] (isCl : FirstOrder.Language.satPair.Relations 1) (pos neg : FirstOrder.Language.satPair.Relations 2) (w w' : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![((), w), ((), w')] ↔ FirstOrder.Language.Structure.RelMap pos ![w 0, w' 0]

@[simp]

theorem DescriptiveComplexity.sideInterp_negIn {A : Type} [FirstOrder.Language.satPair.Structure A] (isCl : FirstOrder.Language.satPair.Relations 1) (pos neg : FirstOrder.Language.satPair.Relations 2) (w w' : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![((), w), ((), w')] ↔ FirstOrder.Language.Structure.RelMap neg ![w 0, w' 0]

theorem DescriptiveComplexity.satisfiable_sideInterp {A : Type} [FirstOrder.Language.satPair.Structure A] (isCl : FirstOrder.Language.satPair.Relations 1) (pos neg : FirstOrder.Language.satPair.Relations 2) : Satisfiable ((sideInterp isCl pos neg).Map A) ↔ SatWith A isCl pos neg

The projected instance is satisfiable exactly when that side is.

Satisfiability ignores elements outside the formula

The step both halves of a DP-hardness pairing will need. Pairing two reductions into one instance forces a common dimension and a common universe, so each side's formula ends up sitting inside a larger structure: the other side's points are there too, and so are the tuples the shorter side does not use. Those extra elements are not harmless by fiat, but they are harmless once they are neither clauses nor occurrences, which is what the lemma below says.

It is stated as transfer along an injection j that reflects the three relations, hits every clause, and hits every element occurring in a clause of its image. Elements outside the image are then pure spectators: a truth assignment may do as it likes on them.

theorem DescriptiveComplexity.satisfiable_iff_of_cover {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (j : B → A) (hj : Function.Injective j) (hcl : ∀ (b : B), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![j b] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![b]) (hpos : ∀ (b b' : B), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![j b, j b'] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![b, b']) (hneg : ∀ (b b' : B), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![j b, j b'] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![b, b']) (hclImg : ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (b : B), c = j b) (hoccImg : ∀ (b : B) (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![j b, x] ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![j b, x] → ∃ (b' : B), x = j b') : Satisfiable A ↔ Satisfiable B

Satisfiability transfers along a clause-covering embedding. The extra elements of A – those outside the image of j – are neither clauses nor occurrences, so they constrain nothing and a satisfying assignment of B extends to them arbitrarily.

Membership in DP

def DescriptiveComplexity.SatSecond : DecisionProblem FirstOrder.Language.satPair

The second formula of the pair is satisfiable: the problem DescriptiveComplexity.UnsatSecond complements.

Equations

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

def DescriptiveComplexity.satFirst_le_sat : FOReduction SatFirst SAT

Projecting the first side is a reduction of SatFirst to SAT.

Equations

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

def DescriptiveComplexity.satSecond_le_sat : FOReduction SatSecond SAT

Projecting the second side is a reduction of SatSecond to SAT.

Equations

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

theorem DescriptiveComplexity.satFirst_sigmaSODefinable : SigmaSODefinable 1 SatFirst

The first side's satisfiability is Σ₁-definable, inherited from SAT along the projection.

theorem DescriptiveComplexity.unsatSecond_eq_compl : UnsatSecond = SatSecondᶜ

UnsatSecond is the complement of SatSecond.

theorem DescriptiveComplexity.unsatSecond_piSODefinable : PiSODefinable 1 UnsatSecond

The second side's unsatisfiability is Π₁-definable: the complement of an NP condition, the reduction complementing along with it.

theorem DescriptiveComplexity.satUnsat_mem_DP : DP.Mem SATUNSAT

SAT-UNSAT is in DP, by its very shape: an NP condition on one side and a coNP condition on the other, imposed together.