DP-hardness of SAT-UNSAT #
The hardness half of the completeness of SAT-UNSAT
(Papadimitriou & Yannakakis 1984): every
DP-definable problem admits an ordered first-order reduction to SAT-UNSAT
(DescriptiveComplexity.satUnsat_hard_of_dpDefinable), which with the membership half
DescriptiveComplexity.satUnsat_mem_DP makes it DP-complete
(DescriptiveComplexity.SATUNSAT_DP_complete).
A DP definition of Q is a Σ₁-definable S and a Π₁-definable T with
Q ≡ S ⊓ T. Complementing the second half, Tᶜ is Σ₁-definable, so the
Cook–Levin discharge DescriptiveComplexity.sat_hard_of_sigmaSODefinable applies to
both S and Tᶜ and yields two ordered reductions to SAT. Running them
side by side into one paired-CNF instance is what this file does: Q holds
iff the first CNF instance is satisfiable and the second is not, which is
exactly SAT-UNSAT of the pair.
Pairing two interpretations #
DescriptiveComplexity.pairInterp puts two interpretations into Language.sat together
into one interpretation into Language.satPair: tags T₁ ⊕ T₂, dimension
max d₁ d₂, and each of the six relations defined by its own side's formula on
its own tags – and by ⊥ as soon as one argument's tag belongs to the other
side, so that the two formulas never see each other's points.
The two sides now share a universe of tuples longer than either originally
used, and the extra coordinates must not be left free: a clause and its
variables would acquire |A|^(dim−dᵢ) copies each, every clause copy
containing every copy of each of its variables, and the blow-up of an
unsatisfiable instance can be satisfiable ({x}, {¬x} becomes
(x₁ ∨ … ∨ xₖ) ∧ (¬x₁ ∨ … ∨ ¬xₖ)). So each side's formulas are conjoined with
DescriptiveComplexity.canonF, pinning the spare coordinates to a minimum of the
order: the points of a side are then in bijection with the points of its own
interpretation (DescriptiveComplexity.sidePt), and everything else in the paired
universe is junk – neither a clause nor an occurrence, hence harmless by
DescriptiveComplexity.satisfiable_iff_of_cover.
Both sides are handled once, by a section generic in the tag injection
inj : T → Tg and its partial inverse get : Tg → Option T, instantiated at
Sum.inl/Sum.getLeft? and Sum.inr/Sum.getRight?.
Satisfiability of one side, along a covering embedding #
The Language.satPair counterpart of DescriptiveComplexity.satisfiable_iff_of_cover:
one side of a paired instance is satisfiable exactly when a plain CNF
structure covering its clauses and occurrences is.
One side of the paired instance #
The defining formulas of one side, and the characterization of the relations
they interpret. Everything here is generic in the tag injection inj and its
partial inverse get, so that it serves both sides of the pair.
The defining formula of one side's relation R at a tuple t of tags:
this side's own formula, its coordinates re-read among the d available ones
and its argument tuples pinned to canonically padded ones – and ⊥ unless
every argument's tag belongs to this side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The points of one side #
A tuple congruence for relations, then the injection of one side's own interpretation into the paired universe and the characterization of the interpreted relations along it.
The point of the paired universe holding a point of one side's own interpretation: its tag injected, its tuple canonically padded.
Equations
- DescriptiveComplexity.sidePt I inj J a₀ b = (inj b.1, DescriptiveComplexity.pad a₀ b.2)
Instances For
Dependency graph
Pairing two interpretations into one #
The symbols of the first side of a paired CNF vocabulary.
Equations
Instances For
Dependency graph
The symbols of the second side of a paired CNF vocabulary.
Equations
Instances For
Dependency graph
Two CNF interpretations, paired into one. The tags of the two sides
are kept apart in a sum, the dimension is the larger of the two, and each of
the six relations is defined by its own side's formula on its own tags, at
canonically padded tuples – and by ⊥ as soon as an argument belongs to the
other side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The first side of the paired instance is satisfiable exactly when the first interpretation is.
Dependency graph
The second side of the paired instance is satisfiable exactly when the second interpretation is.
Dependency graph
The reduction #
Two reductions to SAT, paired into one reduction to SAT-UNSAT. Given a
problem Q that is the conjunction of S and T, a reduction of S to SAT
and one of Tᶜ to SAT, the paired interpretation sends A to the pair of
their images: its first CNF instance is satisfiable iff S holds, and its
second is unsatisfiable iff T does.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
DP-completeness of SAT-UNSAT #
The hardness half: every DP-definable problem admits an ordered
first-order reduction to SAT-UNSAT. The Σ₁ half and the complement of the
Π₁ half are both discharged by Cook–Levin
(DescriptiveComplexity.sat_hard_of_sigmaSODefinable), and the two CNF instances so
produced are paired into one.
Dependency graph
Dependency graph
SAT-UNSAT is DP-complete (Papadimitriou & Yannakakis
1984): membership is
DescriptiveComplexity.satUnsat_mem_DP, the shape of the problem itself; hardness is
DescriptiveComplexity.satUnsat_hard_of_dpDefinable, the two Cook–Levin discharges run
side by side into one paired instance.
Registered in the Lax archive as
Lax564036.SatUnsatDPComplete.satUnsat_DP_complete.