Documentation

DescriptiveComplexity.Problems.ExactCover

Exact Cover is NP-complete #

EXACT COVER (Karp 1972): is there a subfamily covering every ground element exactly once? The problem lives on FirstOrder.Language.setSystem unchanged (DescriptiveComplexity.ExactCover, DescriptiveComplexity.Problems.SetFamily.Defs) – exactness is a property of the subfamily, not a new vocabulary, and it replaces the threshold, so the marked set plays no role at all.

Hardness comes from exactly-one satisfiability (DescriptiveComplexity.Problems.OneInSat) by a reduction with no gadget and no counting, order-free and of dimension 1:

the ground elements are the variables and the clauses, a variable being an element that occurs in some clause (DescriptiveComplexity.SatOccurs);
the family has one set per literal (x, s) of a variable x, namely {x} ∪ {clauses where (x, s) occurs}.

Covering the element x exactly once picks exactly one of the two literals of x – that is a truth assignment – and covering a clause exactly once is exactly what exactly-one satisfaction asks. Nothing here depends on the width of the clauses, which is why the source is unrestricted 1-in-SAT rather than its width-three restriction.

inductive DescriptiveComplexity.ExactCoverRed.ECTag :

Tags of the reduction: the ground element of a variable, the ground element of a clause, and the set of a literal.

velt : ECTag
The ground element of a variable.
celt : ECTag
The ground element of a clause.
lset (s : Bool) : ECTag
The set of the literal (x, s).

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.ExactCoverRed.instDecidableEqECTag :

DecidableEq ECTag

Equations

DescriptiveComplexity.ExactCoverRed.instDecidableEqECTag = DescriptiveComplexity.ExactCoverRed.instDecidableEqECTag.decEq

Dependency graph

def DescriptiveComplexity.ExactCoverRed.instDecidableEqECTag.decEq (x✝ x✝¹ : ECTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.ExactCoverRed.instFintypeECTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.ExactCoverRed.instNonemptyECTag :

Dependency graph

The interpretation #

noncomputable def DescriptiveComplexity.ExactCoverRed.occursF {α : Type} (x : α) :

FirstOrder.Language.sat.Formula α

x is a variable of the formula – it occurs in some clause –, as a formula. Without this guard an element in no clause would be a ground element with two singleton sets to choose from: harmless for the existence of an exact cover, and a factor two in their number.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.ExactCoverRed.elemF :

ECTag → FirstOrder.Language.sat.Formula (Fin 1 × Fin 1)

Defining formula for the ground elements: the variables and the clauses.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.ExactCoverRed.famF :

ECTag → FirstOrder.Language.sat.Formula (Fin 1 × Fin 1)

Defining formula for the family: one set per literal of a variable.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.ExactCoverRed.memF :

ECTag → ECTag → FirstOrder.Language.sat.Formula (Fin 2 × Fin 1)

Defining formula for incidence: the set of (x, s) contains the element of x and the elements of the clauses where (x, s) occurs.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.ExactCoverRed.memF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.ExactCoverRed.ecInterp :

FOInterpretation FirstOrder.Language.sat FirstOrder.Language.setSystem ECTag 1

The interpretation of Exact Cover instances in CNF instances.

Equations

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

Instances For

Dependency graph

The points #

def DescriptiveComplexity.ExactCoverRed.ecPt {A : Type} (t : ECTag) (x : A) :

The point of tag t over the element x.

Equations

DescriptiveComplexity.ExactCoverRed.ecPt t x = (t, fun (x_1 : Fin 1) => x)

Instances For

Dependency graph

theorem DescriptiveComplexity.ExactCoverRed.ecPt_eq_iff {A : Type} {t t' : ECTag} {x x' : A} :

ecPt t x = ecPt t' x' ↔ t = t' ∧ x = x'

Dependency graph

Characterization of the four relations #

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssElem_velt {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :

SSElem (ecPt ECTag.velt x) ↔ SatOccurs A x

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssElem_celt {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) :

SSElem (ecPt ECTag.celt c) ↔ SatOcc.IsCl c

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssElem_lset {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x : A) :

¬SSElem (ecPt (ECTag.lset s) x)

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssFam_lset {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x : A) :

SSFam (ecPt (ECTag.lset s) x) ↔ SatOccurs A x

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssFam_velt {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :

¬SSFam (ecPt ECTag.velt x)

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssFam_celt {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :

¬SSFam (ecPt ECTag.celt x)

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssMem_velt_lset {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) (s : Bool) (y : A) :

SSMem (ecPt ECTag.velt x) (ecPt (ECTag.lset s) y) ↔ x = y

Dependency graph

@[simp]

theorem DescriptiveComplexity.ExactCoverRed.ssMem_celt_lset {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) (s : Bool) (x : A) :

SSMem (ecPt ECTag.celt c) (ecPt (ECTag.lset s) x) ↔ SatOcc.OccIn c x s

Dependency graph

theorem DescriptiveComplexity.ExactCoverRed.ssFam_cases {A : Type} [FirstOrder.Language.sat.Structure A] {q : ecInterp.Map A} (h : SSFam q) :

∃ (s : Bool) (x : A), SatOccurs A x ∧ q = ecPt (ECTag.lset s) x

The sets of the family are exactly the literal sets of the variables.

Dependency graph

Correctness #

Stated for an explicit assignment and an explicit cover, so that the same lemmas give the equivalence of the two decision problems and the bijection between their solutions (DescriptiveComplexity.Problems.ExactCoverCounting).

def DescriptiveComplexity.ExactCoverRed.coverOf {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) (S : ecInterp.Map A) :

The subfamily of an assignment: the sets of its true literals.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.ExactCoverRed.assignOf {A : Type} (G : ecInterp.Map A → Prop) (z : A) :

The assignment of a subfamily: the variables whose positive literal set is chosen.

Equations

DescriptiveComplexity.ExactCoverRed.assignOf G z = G (DescriptiveComplexity.ExactCoverRed.ecPt (DescriptiveComplexity.ExactCoverRed.ECTag.lset true) z)

Instances For

Dependency graph

theorem DescriptiveComplexity.ExactCoverRed.exactCoverBy_coverOf {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (hν : OneInProper ν) :

ExactCoverBy SSElem SSFam SSMem (coverOf ν)

The true literals of an exactly-one assignment form an exact cover.

Dependency graph

theorem DescriptiveComplexity.ExactCoverRed.exactCoverBy_lit {A : Type} [FirstOrder.Language.sat.Structure A] {G : ecInterp.Map A → Prop} (hG : ExactCoverBy SSElem SSFam SSMem G) {x : A} (hx : SatOccurs A x) (s : Bool) :

G (ecPt (ECTag.lset s) x) ↔ SatOcc.LitTrue (assignOf G) x s

The chosen sets of an exact cover are the true literals of its assignment, at every variable.

Dependency graph

theorem DescriptiveComplexity.ExactCoverRed.oneInProper_assignOf {A : Type} [FirstOrder.Language.sat.Structure A] {G : ecInterp.Map A → Prop} (hG : ExactCoverBy SSElem SSFam SSMem G) :

OneInProper (assignOf G)

An exact cover reads off an exactly-one assignment.

Dependency graph

theorem DescriptiveComplexity.ExactCoverRed.oneInSatisfiable_iff_hasExactCover (A : Type) [FirstOrder.Language.sat.Structure A] :

OneInSatisfiable A ↔ HasExactCover (ecInterp.Map A)

Correctness of the reduction: a CNF structure is exactly-one satisfiable iff its literal set system has an exact cover.

Dependency graph

noncomputable def DescriptiveComplexity.oneInSat_fo_reduction_exactCover :

FOReduction OneInSAT ExactCover

1-in-SAT FO-reduces to Exact Cover: the ground elements are the variables and the clauses, and the family has one set per literal. No order, no gadget and no counting.

Equations

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

Instances For

Dependency graph

NP-completeness #

theorem DescriptiveComplexity.exactCover_NP_hard :

NP.Hard ExactCover

Exact Cover is NP-hard: 1-in-SAT, which is NP-hard, FO-reduces to it.

Dependency graph

theorem DescriptiveComplexity.exactCover_NP_complete :

NP.Complete ExactCover

Exact Cover is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem. Registered in the Lax archive as Lax799700.SetFamily.exactCover_NP_complete.

Dependency graph