Documentation

DescriptiveComplexity.Problems.Partition.Hardness

Partition is NP-hard #

Partition asks for a set of items weighing exactly as much as the items it leaves out. Karp derives it from Knapsack by padding an instance with the two weights 2Σ − T and Σ + T; both are arithmetic in the total, so that padding is not first-order and the reduction has to start elsewhere. It starts here from NAE-SAT, whose not-all-equal condition is the two-sided constraint a balanced split imposes.

The gadget #

One digit block per variable and one per clause, in base 2 ^ (3 |A|), and one item per literal, per slack position and per empty clause:

the item of the literal (x, s) has the digit 1 in the block of x and in the block of every clause where (x, s) occurs;
the block of a variable therefore totals 2, so a balanced split takes exactly one of the two literals of each variable: it is an assignment;
the item of a slack occurrence – an occurrence of a clause that is neither its first nor its last – has the digit 1 in the block of that clause, which brings the total of a clause of width w to w + (w − 2); a balanced split takes w − 1 of them, that is, between 1 and w − 1 true literals: exactly not-all-equal satisfaction;
a clause with no literal at all totals 1 with its own item, an odd digit, so no split exists – which is the right answer, an empty clause being not-all-equal unsatisfiable. A clause of width one needs no item of its own: it has no slack occurrence, so its block already totals 1.

Nothing here bounds the width, so the reduction starts from NAE-SAT rather than from its width-three restriction: w + (w − 2) is even and the interval [1, w − 1] is the not-all-equal condition at every width.

What the order is for #

Positions are (block, index) pairs ordered lexicographically, one block being 3 |A| positions, so the lowest position of a block has rank 3 |A| · the rank of the block (DescriptiveComplexity.PartRed.bitRank_pLow) – the two-level analogue of the block structure of the Knapsack reduction. Only lowest positions ever carry a bit, so weights are read digit by digit, and 3 |A| bits keep the base above every digit the gadget writes.

The order of the interpreted structure is described once, by a key into ℕ × A × ℕ × A read lexicographically (DescriptiveComplexity.PartRed.bwLe_iff), rather than tag pair by tag pair.

The minimum of the order #

noncomputable def DescriptiveComplexity.PartRed.minF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

A minimum of the order, as a formula over the ordered expansion of the vocabulary of CNF instances.

Equations

DescriptiveComplexity.PartRed.minF x = DescriptiveComplexity.botF x

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.realize_minF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {x : α} :

(minF x).Realize v ↔ IsBot (v x)

Dependency graph

The tags #

inductive DescriptiveComplexity.PartRed.PTag :

Tags of the reduction. The items are those of the literals, of the slack occurrences and of the empty clauses; the positions carry a block – a variable block (false) or a clause block (true) – and an index inside it, of which Fin 3 are enough to keep the base above every digit.

lit (s : Bool) : PTag
The item of the literal (x, s); its tuple is (x, ⊥).
slk (s : Bool) : PTag
The item of the slack occurrence (x, s) of c; its tuple is (c, x).
emp : PTag
The item of the empty clause c; its tuple is (c, ⊥).
pos (k : Bool) (f : Fin 3) : PTag
The f-th position of the block (k, e); its tuple is (e, y).

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.instDecidableEqPTag.decEq (x✝ x✝¹ : PTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.PartRed.instDecidableEqPTag :

DecidableEq PTag

Equations

DescriptiveComplexity.PartRed.instDecidableEqPTag = DescriptiveComplexity.PartRed.instDecidableEqPTag.decEq

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.PartRed.instFintypePTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.PartRed.instNonemptyPTag :

Dependency graph

def DescriptiveComplexity.PartRed.tagRk :

The rank of a tag: the items first, then the positions of the variable blocks, then those of the clause blocks. It is the leading component of the key, so it separates items from positions and variable blocks from clause blocks.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.subRk :

The rank of a tag inside a block: the index of a position, and 0 for the items, which no block holds.

Equations

DescriptiveComplexity.PartRed.subRk (DescriptiveComplexity.PartRed.PTag.pos k f) = ↑f
DescriptiveComplexity.PartRed.subRk x✝ = 0

Instances For

Dependency graph

The interpretation #

noncomputable def DescriptiveComplexity.PartRed.itemF :

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

Defining formula for the items: one per literal, one per slack occurrence and one per empty clause.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.posnF :

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

Defining formula for the bit positions: every tagged pair is one.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.PartRed.bitF :

PTag → PTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for the bits of the weights. Only the lowest position of a block – index 0, second coordinate a minimum – ever carries a bit.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.leKF (t t' : PTag) :

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

Defining formula for the order: the key (tag rank, first coordinate, index in the block, second coordinate), read lexicographically.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.PartRed.pInterp :

FOInterpretation SatOcc.satOrd FirstOrder.Language.binWeights PTag 2

The interpretation of a binary-weighted instance in a CNF structure: one item per literal, slack occurrence and empty clause, one block of 3 |A| positions per variable and per clause. The target symbol is unused, Partition carrying no number to reach.

Equations

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

Instances For

Dependency graph

The points of the interpreted structure #

def DescriptiveComplexity.PartRed.pPt {A : Type} (t : PTag) (w : Fin 2 → A) :

The point of tag t over the pair w.

Equations

DescriptiveComplexity.PartRed.pPt t w = (t, w)

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.pPt_snd {A : Type} (t : PTag) (w : Fin 2 → A) (j : Fin 2) :

(pPt t w).2 j = w j

Dependency graph

def DescriptiveComplexity.PartRed.pLit {A : Type} (a₀ : A) (s : Bool) (x : A) :

The item of the literal (x, s).

Equations

DescriptiveComplexity.PartRed.pLit a₀ s x = DescriptiveComplexity.PartRed.pPt (DescriptiveComplexity.PartRed.PTag.lit s) ![x, a₀]

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.pSlk {A : Type} (s : Bool) (c x : A) :

The item of the slack occurrence (x, s) of the clause c.

Equations

DescriptiveComplexity.PartRed.pSlk s c x = DescriptiveComplexity.PartRed.pPt (DescriptiveComplexity.PartRed.PTag.slk s) ![c, x]

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.pEmp {A : Type} (a₀ c : A) :

The item of the empty clause c.

Equations

DescriptiveComplexity.PartRed.pEmp a₀ c = DescriptiveComplexity.PartRed.pPt DescriptiveComplexity.PartRed.PTag.emp ![c, a₀]

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.pPos {A : Type} (f : Fin 3) (b : Bool × A) (y : A) :

The f-th position of the block b.

Equations

DescriptiveComplexity.PartRed.pPos f b y = DescriptiveComplexity.PartRed.pPt (DescriptiveComplexity.PartRed.PTag.pos b.1 f) ![b.2, y]

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.pLow {A : Type} (a₀ : A) (b : Bool × A) :

The lowest position of the block b.

Equations

DescriptiveComplexity.PartRed.pLow a₀ b = DescriptiveComplexity.PartRed.pPos 0 b a₀

Instances For

Dependency graph

Characterization of the interpreted relations #

@[simp]

theorem DescriptiveComplexity.PartRed.bwItem_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) :

BWItem (pPt (PTag.lit s) w) ↔ IsBot (w 1)

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwItem_slk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) :

BWItem (pPt (PTag.slk s) w) ↔ SatOcc.Mid (w 0) (w 1) s

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwItem_emp {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (w : Fin 2 → A) :

BWItem (pPt PTag.emp w) ↔ SatOcc.EmptyCl (w 0) ∧ IsBot (w 1)

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwItem_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k : Bool) (f : Fin 3) (w : Fin 2 → A) :

¬BWItem (pPt (PTag.pos k f) w)

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwPosn_pos {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k : Bool) (f : Fin 3) (w : Fin 2 → A) :

BWPosn (pPt (PTag.pos k f) w)

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwPosn_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) :

¬BWPosn (pPt (PTag.lit s) w)

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwPosn_slk {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (w : Fin 2 → A) :

¬BWPosn (pPt (PTag.slk s) w)

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwPosn_emp {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (w : Fin 2 → A) :

¬BWPosn (pPt PTag.emp w)

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwTgt_none {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : PTag) (w : Fin 2 → A) :

¬BWTgt (pPt t w)

Dependency graph

def DescriptiveComplexity.PartRed.pKey {A : Type} (q : pInterp.Map A) :

ℕ × A × ℕ × A

The key of a point: tag rank, first coordinate, index in the block, second coordinate.

Equations

DescriptiveComplexity.PartRed.pKey q = (DescriptiveComplexity.PartRed.tagRk q.1, q.2 0, DescriptiveComplexity.PartRed.subRk q.1, q.2 1)

Instances For

Dependency graph

def DescriptiveComplexity.PartRed.keyLe {A : Type} [LinearOrder A] :

ℕ × A × ℕ × A → ℕ × A × ℕ × A → Prop

The order of the interpreted structure, read lexicographically on the keys.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.PartRed.bwLe_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t t' : PTag) (w w' : Fin 2 → A) :

BWLe (pPt t w) (pPt t' w') ↔ keyLe (pKey (pPt t w)) (pKey (pPt t' w'))

Dependency graph

theorem DescriptiveComplexity.PartRed.pKey_injective {A : Type} :

Function.Injective pKey

Dependency graph

The blocks #

def DescriptiveComplexity.PartRed.blkLe {A : Type} [LinearOrder A] :

Bool × A → Bool × A → Prop

The order of the blocks: the variable blocks first, then the clause blocks, each group in the order of the input.

Equations

DescriptiveComplexity.PartRed.blkLe = DescriptiveComplexity.lexRel (fun (x1 x2 : Bool) => x1 ≤ x2) fun (x1 x2 : A) => x1 ≤ x2

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.PartRed.blkRank {A : Type} [LinearOrder A] (b : Bool × A) :

The rank of a block: how many blocks lie strictly below it.

Equations

DescriptiveComplexity.PartRed.blkRank b = DescriptiveComplexity.bitRank DescriptiveComplexity.PartRed.blkLe (fun (x : Bool × A) => True) b

Instances For

Dependency graph

The bits, and the lowest position of a block #

@[simp]

theorem DescriptiveComplexity.PartRed.bwBit_pos_left {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (k : Bool) (f : Fin 3) (w : Fin 2 → A) (q : pInterp.Map A) :

¬BWBit (pPt (PTag.pos k f) w) q

Dependency graph

@[simp]

theorem DescriptiveComplexity.PartRed.bwBit_item_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t : PTag) (w : Fin 2 → A) (s : Bool) (w' : Fin 2 → A) :

¬BWBit (pPt t w) (pPt (PTag.lit s) w') ∧ ¬BWBit (pPt t w) (pPt (PTag.slk s) w') ∧ ¬BWBit (pPt t w) (pPt PTag.emp w')

Dependency graph

The place values #

theorem DescriptiveComplexity.PartRed.key_pos {A : Type} (k : Bool) (f : Fin 3) (w : Fin 2 → A) :

pKey (pPt (PTag.pos k f) w) = (if k = true then 6 else 5, w 0, ↑f, w 1)

Dependency graph

theorem DescriptiveComplexity.PartRed.bitRank_pLow {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (b : Bool × A) :

bitRank BWLe BWPosn (pLow a₀ b) = 3 * Nat.card A * blkRank b

The block structure: the rank of the lowest position of a block is 3 |A| times the rank of the block, so its place value is (2 ^ (3 |A|)) ^ rank – one digit of base 2 ^ (3 |A|) per block.

Dependency graph

Weights, as base-`2 ^ (3 |A|)` numbers #

noncomputable def DescriptiveComplexity.PartRed.pbase (A : Type) [Finite A] :

The base: one digit per block, 3 |A| bits wide, which is above every digit the gadget writes, so digits never carry into the next block.

Equations

DescriptiveComplexity.PartRed.pbase A = 2 ^ (3 * Nat.card A)

Instances For

Dependency graph

theorem DescriptiveComplexity.PartRed.pbase_pos {A : Type} [Finite A] :

Dependency graph

Counting the items of a block #

Which items carry a bit in a block #

theorem DescriptiveComplexity.PartRed.pLow_eq {A : Type} (a₀ : A) (k : Bool) (e : A) :

pLow a₀ (k, e) = pPt (PTag.pos k 0) ![e, a₀]

Dependency graph

The digits, block by block #

theorem DescriptiveComplexity.PartRed.pLit_ne_pSlk {A : Type} (a₀ : A) (s s' : Bool) (x c y : A) :

pLit a₀ s x ≠ pSlk s' c y

Dependency graph

theorem DescriptiveComplexity.PartRed.pLit_ne_pEmp {A : Type} (a₀ : A) (s : Bool) (x c : A) :

pLit a₀ s x ≠ pEmp a₀ c

Dependency graph

theorem DescriptiveComplexity.PartRed.pSlk_ne_pEmp {A : Type} (a₀ : A) (s : Bool) (c x c' : A) :

pSlk s c x ≠ pEmp a₀ c'

Dependency graph

The digits stay below the base #

theorem DescriptiveComplexity.PartRed.ncard_le_two_card {A : Type} [Finite A] (X : Set (A × Bool)) :

X.ncard ≤ 2 * Nat.card A

Dependency graph

The selection made by an assignment #

def DescriptiveComplexity.PartRed.splitSet {A : Type} (a₀ : A) (ν : A → Prop) (M : A → Set (A × Bool)) :

pInterp.Map A → Prop

The items a not-all-equal assignment selects: the true literals, and the slack items chosen by M.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.PartRed.pLit_eq_iff {A : Type} {a₀ : A} {s s' : Bool} {x x' : A} :

pLit a₀ s x = pLit a₀ s' x' ↔ s = s' ∧ x = x'

Dependency graph

theorem DescriptiveComplexity.PartRed.pSlk_eq_iff {A : Type} {s s' : Bool} {c c' x x' : A} :

pSlk s c x = pSlk s' c' x' ↔ s = s' ∧ c = c' ∧ x = x'

Dependency graph

theorem DescriptiveComplexity.PartRed.splitSet_pLit {A : Type} {a₀ : A} {ν : A → Prop} {M : A → Set (A × Bool)} (s : Bool) (x : A) :

splitSet a₀ ν M (pLit a₀ s x) ↔ SatOcc.LitTrue ν x s

Dependency graph

theorem DescriptiveComplexity.PartRed.splitSet_pSlk {A : Type} {a₀ : A} {ν : A → Prop} {M : A → Set (A × Bool)} (s : Bool) (c x : A) :

splitSet a₀ ν M (pSlk s c x) ↔ (x, s) ∈ M c

Dependency graph

theorem DescriptiveComplexity.PartRed.splitSet_pEmp {A : Type} {a₀ : A} {ν : A → Prop} {M : A → Set (A × Bool)} (c : A) :

¬splitSet a₀ ν M (pEmp a₀ c)

Dependency graph

Correctness of the reduction #

theorem DescriptiveComplexity.PartRed.naeSatisfiable_iff_hasEqualSplit (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

NAESatisfiable A ↔ HasEqualSplit (pInterp.Map A)

Correctness of the reduction: a CNF structure is not-all-equal satisfiable iff the interpreted binary-weighted instance splits into two halves of equal weight.

Dependency graph

noncomputable def DescriptiveComplexity.naeSat_ordered_fo_reduction_partition :

OrderedFOReduction NAESAT Partition

NAE-SAT ordered-FO-reduces to Partition: one item per literal, one per slack occurrence and one per empty clause; one digit block of 3 |A| bit positions per variable and per clause. A variable block totals 2, so a balanced split is an assignment; a clause block of width w totals w + (w − 2), so a balanced split takes between 1 and w − 1 true literals, which is not-all-equal satisfaction.

Equations

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

Instances For

Dependency graph