Documentation

DescriptiveComplexity.Problems.OneInSat.Reduction

3SAT ordered-FO-reduces to 1-in-SAT #

The classical gadget, with the width case analysis removed by the three slots of DescriptiveComplexity.Problems.OneInSat.Slots. Every clause c of the input gets

three slot variables slot i c, tied to its occurrences by the link clauses link i c = {¬ slot i c} ∪ {the i-th literal of c, if there is one} – read as exactly-one clauses these say slot i c ↔ (i-th literal) when the occurrence exists and slot i c = false when it does not, the same clause description in both cases, one literal shorter;
four fresh variables fresh j c and the three gadget clauses piece one c = {¬ slot one c, d, e}, piece two c = {slot two c, e, f}, piece three c = {¬ slot three c, f, g}, which are exactly-one satisfiable iff some slot of c is true.

Since a slot is true exactly when the corresponding literal is (DescriptiveComplexity.OneInRed.exists_litTrue_iff_slot), the output is exactly-one satisfiable iff the input is satisfiable. Clauses of width 0, 1 and 2 need no special treatment: their missing slots are false, and an empty clause correctly yields an unsatisfiable gadget.

The whole construction is gated on the width check ThreeSatToSat.wideOrdF, as the reduction of 3SAT to SAT is: on a wide input every element becomes a clause with no literal at all, and a clause with no literal has no true literal, let alone exactly one. The order is used only to say i-th occurrence, so this is an ordered reduction; the dimension is 1, all the fresh variables being carried by tags.

inductive DescriptiveComplexity.OneInRed.OITag :

Tags of the gadget: the copy of a variable, the three slots and four fresh variables of a clause, and its three link and three gadget clauses.

var : OITag
The copy of a propositional variable.
slot (i : Ix3) : OITag
The i-th slot variable of a clause.
fresh (j : Ix4) : OITag
The j-th fresh variable of a clause.
link (i : Ix3) : OITag
The i-th link clause of a clause.
piece (i : Ix3) : OITag
The i-th gadget clause of a clause.

Instances For

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instDecidableEqOITag :

DecidableEq OITag

Equations

DescriptiveComplexity.OneInRed.instDecidableEqOITag = DescriptiveComplexity.OneInRed.instDecidableEqOITag.decEq

def DescriptiveComplexity.OneInRed.instDecidableEqOITag.decEq (x✝ x✝¹ : OITag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instFintypeOITag :

Equations

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

instance DescriptiveComplexity.OneInRed.instNonemptyOITag :

def DescriptiveComplexity.OneInRed.clauseTag :

The tags carrying a clause of the output.

Equations

Instances For

def DescriptiveComplexity.OneInRed.posPair :

OITag → OITag → Bool

The pairs of tags joined by a positive literal, on the same element: the gadget clauses containing a fresh variable, and the second gadget clause containing its slot.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.OneInRed.posPair x✝¹ x✝ = false

Instances For

def DescriptiveComplexity.OneInRed.negPair :

OITag → OITag → Bool

The pairs of tags joined by a negative literal, on the same element: the first and third gadget clauses contain their slot negatively, and so does every link clause.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.OneInRed.negPair x✝¹ x✝ = false

Instances For

The interpretation #

noncomputable def DescriptiveComplexity.OneInRed.samePtF (b : Bool) :

SatOcc.satOrd.Formula (Fin 2 × Fin 1)

The literal joining two tags on the same element, if there is one.

Equations

DescriptiveComplexity.OneInRed.samePtF b = if b = true then DescriptiveComplexity.SatOcc.eqF (0, 0) (1, 0) else ⊥

Instances For

noncomputable def DescriptiveComplexity.OneInRed.linkLitF (t₁ t₂ : OITag) (s : Bool) :

SatOcc.satOrd.Formula (Fin 2 × Fin 1)

The literal of a link clause coming from the i-th occurrence of its clause, with sign s.

Equations

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

Instances For

noncomputable def DescriptiveComplexity.OneInRed.isClauseF (t : OITag) :

SatOcc.satOrd.Formula (Fin 1 × Fin 1)

Defining formula for “is a clause”: link and gadget clauses sit on the clauses of the input, and on a wide input everything is a clause.

Equations

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

Instances For

noncomputable def DescriptiveComplexity.OneInRed.posInF (t₁ t₂ : OITag) :

SatOcc.satOrd.Formula (Fin 2 × Fin 1)

Defining formula for “occurs positively in”.

Equations

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

Instances For

noncomputable def DescriptiveComplexity.OneInRed.negInF (t₁ t₂ : OITag) :

SatOcc.satOrd.Formula (Fin 2 × Fin 1)

Defining formula for “occurs negatively in”.

Equations

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

Instances For

noncomputable def DescriptiveComplexity.OneInRed.oiInterp :

FOInterpretation SatOcc.satOrd FirstOrder.Language.sat OITag 1

The interpretation of 1-in-SAT instances in ordered CNF instances.

Equations

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

Instances For

The vertices of the gadget #

def DescriptiveComplexity.OneInRed.pt {A : Type} (t : OITag) (x : A) :

The point of tag t over the element x.

Equations

DescriptiveComplexity.OneInRed.pt t x = (t, fun (x_1 : Fin 1) => x)

Instances For

theorem DescriptiveComplexity.OneInRed.pt_eq_iff {A : Type} {t t' : OITag} {x x' : A} :

pt t x = pt t' x' ↔ t = t' ∧ x = x'

theorem DescriptiveComplexity.OneInRed.pt_eta {A : Type} {t : OITag} {w : Fin 1 → A} :

(t, w) = pt t (w 0)

theorem DescriptiveComplexity.OneInRed.pt_surj {A : Type} (q : oiInterp.Map A) :

∃ (t : OITag) (x : A), q = pt t x

Characterization of the three relations #

theorem DescriptiveComplexity.OneInRed.isCl_pt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : OITag) (x : A) :

SatOcc.IsCl (pt t x) ↔ clauseTag t = true ∧ SatOcc.IsCl x ∨ ThreeSatToSat.Wide A

The clauses of the gadget.

theorem DescriptiveComplexity.OneInRed.posIn_pt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t₁ t₂ : OITag) (x y : A) :

SatOcc.PosIn (pt t₁ x) (pt t₂ y) ↔ ¬ThreeSatToSat.Wide A ∧ (posPair t₁ t₂ = true ∧ x = y ∨ ∃ (i : Ix3), (t₁ = OITag.link i ∧ t₂ = OITag.var) ∧ NthOcc i x y true)

The positive literals of the gadget.

theorem DescriptiveComplexity.OneInRed.negIn_pt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t₁ t₂ : OITag) (x y : A) :

SatOcc.NegIn (pt t₁ x) (pt t₂ y) ↔ ¬ThreeSatToSat.Wide A ∧ (negPair t₁ t₂ = true ∧ x = y ∨ ∃ (i : Ix3), (t₁ = OITag.link i ∧ t₂ = OITag.var) ∧ NthOcc i x y false)

The negative literals of the gadget.

The literals of a gadget clause #

theorem DescriptiveComplexity.OneInRed.occIn_pt_cases {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {tc : OITag} {c : A} {q : oiInterp.Map A} {u : Bool} (h : SatOcc.OccIn (pt tc c) q u) :

(∃ (t : OITag), (if u = true then posPair tc t else negPair tc t) = true ∧ q = pt t c) ∨ ∃ (i : Ix3) (y : A), tc = OITag.link i ∧ NthOcc i c y u ∧ q = pt OITag.var y

Every literal of a gadget clause is either prescribed by the pair of tags, on the same element, or is the copy of the i-th literal of the clause of a link clause.

theorem DescriptiveComplexity.OneInRed.isCl_gadget {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t : OITag} {c : A} (ht : clauseTag t = true) (hc : SatOcc.IsCl c) :

SatOcc.IsCl (pt t c)

The link and gadget clauses of a clause of the input are clauses.

theorem DescriptiveComplexity.OneInRed.occIn_same_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t₁ t₂ : OITag} {c : A} (hw : ¬ThreeSatToSat.Wide A) (ht : clauseTag t₁ = true) (hc : SatOcc.IsCl c) (hp : posPair t₁ t₂ = true) :

SatOcc.OccIn (pt t₁ c) (pt t₂ c) true

A same-element positive literal of a gadget clause.

theorem DescriptiveComplexity.OneInRed.occIn_same_neg {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t₁ t₂ : OITag} {c : A} (hw : ¬ThreeSatToSat.Wide A) (ht : clauseTag t₁ = true) (hc : SatOcc.IsCl c) (hp : negPair t₁ t₂ = true) :

SatOcc.OccIn (pt t₁ c) (pt t₂ c) false

A same-element negative literal of a gadget clause.

theorem DescriptiveComplexity.OneInRed.occIn_link_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {i : Ix3} {c x : A} {s : Bool} (hw : ¬ThreeSatToSat.Wide A) (hc : SatOcc.IsCl c) (hn : NthOcc i c x s) :

SatOcc.OccIn (pt (OITag.link i) c) (pt OITag.var x) s

The literal of a link clause coming from the occurrence it links.

The assignment carried by the gadget #

def DescriptiveComplexity.OneInRed.oiAssign {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (p : oiInterp.Map A) :

The assignment of the gadget induced by an assignment of the input: the slots take the values of the literals they link, and the four fresh variables of a clause are the explicit witnesses of the gadget.

Equations

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

Instances For

@[simp]

theorem DescriptiveComplexity.OneInRed.oiAssign_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (x : A) :

oiAssign ν (pt OITag.var x) ↔ ν x

@[simp]

theorem DescriptiveComplexity.OneInRed.oiAssign_slot {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (i : Ix3) (c : A) :

oiAssign ν (pt (OITag.slot i) c) ↔ SlotVal ν i c

@[simp]

theorem DescriptiveComplexity.OneInRed.oiAssign_d {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c : A) :

oiAssign ν (pt (OITag.fresh Ix4.d) c) ↔ SlotVal ν Ix3.one c ∧ SlotVal ν Ix3.two c

@[simp]

theorem DescriptiveComplexity.OneInRed.oiAssign_e {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c : A) :

oiAssign ν (pt (OITag.fresh Ix4.e) c) ↔ SlotVal ν Ix3.one c ∧ ¬SlotVal ν Ix3.two c

@[simp]

theorem DescriptiveComplexity.OneInRed.oiAssign_f {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c : A) :

oiAssign ν (pt (OITag.fresh Ix4.f) c) ↔ ¬SlotVal ν Ix3.one c ∧ ¬SlotVal ν Ix3.two c

@[simp]

theorem DescriptiveComplexity.OneInRed.oiAssign_g {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c : A) :

oiAssign ν (pt (OITag.fresh Ix4.g) c) ↔ (SlotVal ν Ix3.one c ∨ SlotVal ν Ix3.two c) ∧ SlotVal ν Ix3.three c

theorem DescriptiveComplexity.OneInRed.litTrue_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (x : A) (s : Bool) :

SatOcc.LitTrue (oiAssign ν) (pt OITag.var x) s ↔ SatOcc.LitTrue ν x s

Which tags carry which literals #

theorem DescriptiveComplexity.OneInRed.posPair_link (i : Ix3) (t : OITag) :

posPair (OITag.link i) t = false

theorem DescriptiveComplexity.OneInRed.negPair_link_iff (i : Ix3) (t : OITag) :

negPair (OITag.link i) t = true ↔ t = OITag.slot i

theorem DescriptiveComplexity.OneInRed.posPair_piece_one (t : OITag) :

posPair (OITag.piece Ix3.one) t = true ↔ t = OITag.fresh Ix4.d ∨ t = OITag.fresh Ix4.e

theorem DescriptiveComplexity.OneInRed.negPair_piece_one (t : OITag) :

negPair (OITag.piece Ix3.one) t = true ↔ t = OITag.slot Ix3.one

theorem DescriptiveComplexity.OneInRed.posPair_piece_two (t : OITag) :

posPair (OITag.piece Ix3.two) t = true ↔ t = OITag.slot Ix3.two ∨ t = OITag.fresh Ix4.e ∨ t = OITag.fresh Ix4.f

theorem DescriptiveComplexity.OneInRed.negPair_piece_two (t : OITag) :

negPair (OITag.piece Ix3.two) t = false

theorem DescriptiveComplexity.OneInRed.posPair_piece_three (t : OITag) :

posPair (OITag.piece Ix3.three) t = true ↔ t = OITag.fresh Ix4.f ∨ t = OITag.fresh Ix4.g

theorem DescriptiveComplexity.OneInRed.negPair_piece_three (t : OITag) :

negPair (OITag.piece Ix3.three) t = true ↔ t = OITag.slot Ix3.three

theorem DescriptiveComplexity.OneInRed.clauseTag_cases {t : OITag} (h : clauseTag t = true) :

(∃ (i : Ix3), t = OITag.link i) ∨ ∃ (i : Ix3), t = OITag.piece i

Correctness #

theorem DescriptiveComplexity.OneInRed.enum_link {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {i : Ix3} {c : A} {y : oiInterp.Map A} {u : Bool} (h : SatOcc.OccIn (pt (OITag.link i) c) y u) :

y = pt (OITag.slot i) c ∧ u = false ∨ ∃ (x : A) (s : Bool), NthOcc i c x s ∧ y = pt OITag.var x ∧ u = s

The literals of the i-th link clause of c.

theorem DescriptiveComplexity.OneInRed.enum_piece {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {i : Ix3} {c : A} {y : oiInterp.Map A} {u : Bool} (h : SatOcc.OccIn (pt (OITag.piece i) c) y u) :

∃ (t : OITag), (if u = true then posPair (OITag.piece i) t else negPair (OITag.piece i) t) = true ∧ y = pt t c

The literals of the i-th gadget clause of c.

theorem DescriptiveComplexity.OneInRed.oneInProper_oiAssign {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hw : ¬ThreeSatToSat.Wide A) (hwidth : WidthAtMostThree A) {ν : A → Prop} (hν : ∀ (c : A), SatOcc.IsCl c → ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) :

OneInProper (oiAssign ν)

The gadget of a satisfiable input is exactly-one satisfiable.

theorem DescriptiveComplexity.OneInRed.litTrue_var_gen {A : Type} {μ : oiInterp.Map A → Prop} (x : A) (s : Bool) :

SatOcc.LitTrue (fun (z : A) => μ (pt OITag.var z)) x s ↔ SatOcc.LitTrue μ (pt OITag.var x) s

theorem DescriptiveComplexity.OneInRed.satisfiable_of_oneInProper {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hw : ¬ThreeSatToSat.Wide A) {μ : oiInterp.Map A → Prop} (hμ : OneInProper μ) (c : A) (hc : SatOcc.IsCl c) :

∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue (fun (z : A) => μ (pt OITag.var z)) x s

A gadget that is exactly-one satisfiable comes from a satisfiable input.

theorem DescriptiveComplexity.OneInRed.threeSatisfiable_iff_oneInSatisfiable_map {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] :

ThreeSatisfiable A ↔ OneInSatisfiable (oiInterp.Map A)

Correctness of the reduction: a CNF structure is a yes-instance of 3SAT iff its gadget is exactly-one satisfiable.

noncomputable def DescriptiveComplexity.OneInRed.threeSat_ordered_fo_reduction_oneInSat :

OrderedFOReduction ThreeSAT OneInSAT

3SAT ordered-FO-reduces to 1-in-SAT: the three-slot gadget.

Equations

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

Instances For