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;
the family has one set per literal (x, s), 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.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.

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

theorem DescriptiveComplexity.ExactCoverRed.ecPt_surj {A : Type} (q : ecInterp.Map A) :

∃ (t : ECTag) (x : A), q = ecPt t 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)

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)

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), q = ecPt (ECTag.lset s) x

The sets of the family are exactly the literal sets.

Dependency graph

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

(∃ (x : A), q = ecPt ECTag.velt x) ∨ ∃ (c : A), SatOcc.IsCl c ∧ q = ecPt ECTag.celt c

The ground elements are exactly the variables and the clauses.

Dependency graph

Correctness #

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.

Dependency graph