Documentation

DescriptiveComplexity.Problems.SetSplitting

Set Splitting is NP-complete #

SET SPLITTING, also known as hypergraph 2-colourability: can the ground elements of a set system be coloured with two colours so that no set of the family is monochromatic? Like Exact Cover it lives on FirstOrder.Language.setSystem unchanged (DescriptiveComplexity.SetSplitting, DescriptiveComplexity.Problems.SetFamily.Defs) and carries no threshold – the colouring, not a cardinality, is the whole question.

Hardness comes from NAE-SAT (DescriptiveComplexity.Problems.NaeSat) by a reduction with no gadget and no counting, order-free and of dimension 1:

the ground elements are the literals (x, s);
the family has one set {x, ¬x} per variable, and one set per clause, holding its literals.

A two-colouring splits the pair {x, ¬x} exactly when it gives the two literals of x opposite colours – that is a truth assignment – and it splits a clause set exactly when the clause has both a true and a false literal, which is not-all-equal satisfaction. The correspondence is so direct that the reduction is essentially the identity on clauses; only the pair sets are new, and they are what turns an arbitrary colouring into an assignment.

inductive DescriptiveComplexity.SetSplitRed.SplTag :

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

lit (s : Bool) : SplTag
The ground element of the literal (x, s).
pairSet : SplTag
The set {x, ¬x} of the variable x.
clSet : SplTag
The set of the literals of a clause.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SetSplitRed.instDecidableEqSplTag :

DecidableEq SplTag

Equations

DescriptiveComplexity.SetSplitRed.instDecidableEqSplTag = DescriptiveComplexity.SetSplitRed.instDecidableEqSplTag.decEq

Dependency graph

def DescriptiveComplexity.SetSplitRed.instDecidableEqSplTag.decEq (x✝ x✝¹ : SplTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SetSplitRed.instFintypeSplTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.SetSplitRed.instNonemptySplTag :

Nonempty SplTag

Dependency graph

The interpretation #

noncomputable def DescriptiveComplexity.SetSplitRed.elemF :

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

Defining formula for the ground elements: the literals.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SetSplitRed.famF :

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

Defining formula for the family: one set per variable and one per clause.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SetSplitRed.memF :

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

Defining formula for incidence: the pair set of x holds both literals of x, and the set of a clause holds the literals occurring in it.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SetSplitRed.splInterp :

FOInterpretation FirstOrder.Language.sat FirstOrder.Language.setSystem SplTag 1

The interpretation of Set Splitting 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.SetSplitRed.splPt {A : Type} (t : SplTag) (x : A) :

splInterp.Map A

The point of tag t over the element x.

Equations

DescriptiveComplexity.SetSplitRed.splPt t x = (t, fun (x_1 : Fin 1) => x)

Instances For

Dependency graph

theorem DescriptiveComplexity.SetSplitRed.splPt_eq_iff {A : Type} {t t' : SplTag} {x x' : A} :

splPt t x = splPt t' x' ↔ t = t' ∧ x = x'

Dependency graph

theorem DescriptiveComplexity.SetSplitRed.splPt_surj {A : Type} (q : splInterp.Map A) :

∃ (t : SplTag) (x : A), q = splPt t x

Dependency graph

Characterization of the four relations #

@[simp]

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

SSElem (splPt (SplTag.lit s) x)

Dependency graph

@[simp]

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

¬SSElem (splPt SplTag.pairSet x)

Dependency graph

@[simp]

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

¬SSElem (splPt SplTag.clSet x)

Dependency graph

@[simp]

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

SSFam (splPt SplTag.pairSet x)

Dependency graph

@[simp]

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

SSFam (splPt SplTag.clSet c) ↔ SatOcc.IsCl c

Dependency graph

@[simp]

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

¬SSFam (splPt (SplTag.lit s) x)

Dependency graph

@[simp]

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

SSMem (splPt (SplTag.lit s) x) (splPt SplTag.pairSet y) ↔ x = y

Dependency graph

@[simp]

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

SSMem (splPt (SplTag.lit s) x) (splPt SplTag.clSet c) ↔ SatOcc.OccIn c x s

Dependency graph

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

∃ (s : Bool) (x : A), q = splPt (SplTag.lit s) x

The ground elements are exactly the literals.

Dependency graph

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

(∃ (x : A), q = splPt SplTag.pairSet x) ∨ ∃ (c : A), SatOcc.IsCl c ∧ q = splPt SplTag.clSet c

The sets of the family are the pair sets and the clause sets.

Dependency graph

Correctness #

theorem DescriptiveComplexity.SetSplitRed.naeSatisfiable_iff_hasSetSplitting (A : Type) [FirstOrder.Language.sat.Structure A] :

NAESatisfiable A ↔ HasSetSplitting (splInterp.Map A)

Correctness of the reduction: a CNF structure is not-all-equal satisfiable iff its literal set system can be split.

Dependency graph

noncomputable def DescriptiveComplexity.naeSat_fo_reduction_setSplitting :

FOReduction NAESAT SetSplitting

NAE-SAT FO-reduces to Set Splitting: the ground elements are the literals, the family holds one pair set per variable and one set per clause. 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.setSplitting_mem_NP :

NP.Mem SetSplitting

Set Splitting is in NP: it is Σ₁-definable.

Dependency graph

theorem DescriptiveComplexity.setSplitting_NP_hard :

NP.Hard SetSplitting

Set Splitting is NP-hard: NAE-SAT, which is NP-hard, FO-reduces to it.

Dependency graph

theorem DescriptiveComplexity.setSplitting_NP_complete :

NP.Complete SetSplitting

Set Splitting is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.

Dependency graph