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

theorem DescriptiveComplexity.PartRed.tag_ext {t t' : PTag} (h₁ : tagRk t = tagRk t') (h₂ : subRk t = subRk t') :

t = t'

The two ranks together determine the tag.

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

theorem DescriptiveComplexity.PartRed.pPt_surj {A : Type} (q : pInterp.Map A) :

∃ (t : PTag) (w : Fin 2 → A), q = pPt t w

Dependency graph

theorem DescriptiveComplexity.PartRed.pPt_eq_iff {A : Type} {t t' : PTag} {w w' : Fin 2 → A} :

pPt t w = pPt t' w' ↔ t = t' ∧ w = w'

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

theorem DescriptiveComplexity.PartRed.tuple₂_ext {A : Type} {w w' : Fin 2 → A} (h0 : w 0 = w' 0) (h1 : w 1 = w' 1) :

w = w'

Two 2-tuples with the same coordinates are equal.

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

theorem DescriptiveComplexity.PartRed.pLit_injective {A : Type} (a₀ : A) :

Function.Injective fun (p : A × Bool) => pLit a₀ p.2 p.1

Dependency graph

theorem DescriptiveComplexity.PartRed.pSlk_injective {A : Type} (c : A) :

Function.Injective fun (p : A × Bool) => pSlk p.2 c p.1

Dependency graph

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

Function.Injective fun (u : (Bool × A) × Fin 3 × A) => pPos u.2.1 u.1 u.2.2

Dependency graph

theorem DescriptiveComplexity.PartRed.pLow_injective {A : Type} (a₀ : A) :

Function.Injective (pLow a₀)

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

theorem DescriptiveComplexity.PartRed.isLinOrd_bwLe {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] :

The interpreted order is a linear order: the lexicographic order of the keys, which are pairwise distinct.

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

theorem DescriptiveComplexity.PartRed.isLinOrd_blkLe {A : Type} [LinearOrder A] :

Dependency graph

theorem DescriptiveComplexity.PartRed.blkLt_iff {A : Type} [LinearOrder A] {k k' : Bool} {x e : A} :

blkLe (k, x) (k', e) ∧ (k, x) ≠ (k', e) ↔ k = k' ∧ x < e ∨ k = false ∧ k' = true

Being strictly below a block.

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 #

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

BWBit (pPt (PTag.lit s) w) (pPt (PTag.pos k f) w') ↔ f = 0 ∧ IsBot (w 1) ∧ IsBot (w' 1) ∧ if k = true then SatOcc.OccIn (w' 0) (w 0) s else w' 0 = w 0

Dependency graph

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

BWBit (pPt (PTag.slk s) w) (pPt (PTag.pos k f) w') ↔ f = 0 ∧ k = true ∧ SatOcc.Mid (w 0) (w 1) s ∧ IsBot (w' 1) ∧ w' 0 = w 0

Dependency graph

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

BWBit (pPt PTag.emp w) (pPt (PTag.pos k f) w') ↔ f = 0 ∧ k = true ∧ SatOcc.EmptyCl (w 0) ∧ IsBot (w 1) ∧ IsBot (w' 1) ∧ w' 0 = w 0

Dependency graph

@[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

theorem DescriptiveComplexity.PartRed.eq_pLow_of_bit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {i q : pInterp.Map A} (h : BWBit i q) (hq : BWPosn q) :

∃ (b : Bool × A), q = pLow a₀ b

Only the lowest position of a block ever carries a bit.

Dependency graph

The place values #

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

BWLe (pPt (PTag.pos k f) w) (pPt (PTag.pos k' f') w') ↔ k = false ∧ k' = true ∨ k = k' ∧ (w 0 < w' 0 ∨ w 0 = w' 0 ∧ (↑f < ↑f' ∨ ↑f = ↑f' ∧ w 1 ≤ 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

theorem DescriptiveComplexity.PartRed.binNum_eq_digit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) {p : pInterp.Map A → Prop} {sub : Bool × A → Prop} (hp : ∀ (q : pInterp.Map A), BWPosn q ∧ p q ↔ ∃ (b : Bool × A), sub b ∧ q = pLow a₀ b) :

binNum BWLe BWPosn p = digitNum blkLe (fun (x : Bool × A) => True) (pbase A) fun (b : Bool × A) => if sub b then 1 else 0

A binary number whose bits sit on the lowest positions of the blocks selected by sub is the base-2 ^ (3 |A|) number with digit 1 there.

Dependency graph

theorem DescriptiveComplexity.PartRed.bwWeight_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (i : pInterp.Map A) :

BWWeight i = digitNum blkLe (fun (x : Bool × A) => True) (pbase A) fun (b : Bool × A) => if BWBit i (pLow a₀ b) then 1 else 0

Every weight is read digit by digit: the digit of a block is 1 when the item carries a bit at its lowest position, and 0 otherwise.

Dependency graph

theorem DescriptiveComplexity.PartRed.sum_weights_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (S : pInterp.Map A → Prop) :

∑ᶠ (i : pInterp.Map A) (_ : i ∈ {i : pInterp.Map A | S i}), BWWeight i = digitNum blkLe (fun (x : Bool × A) => True) (pbase A) fun (b : Bool × A) => {i : pInterp.Map A | S i ∧ BWBit i (pLow a₀ b)}.ncard

The weight of a set of items, read digit by digit: the digit of a block is the number of selected items carrying a bit there.

Dependency graph

Counting the items of a block #

noncomputable def DescriptiveComplexity.PartRed.cnt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (a₀ : A) (S : pInterp.Map A → Prop) (b : Bool × A) :

The number of selected items carrying a bit in a block: the digit that block contributes to the weight of the selection.

Equations

DescriptiveComplexity.PartRed.cnt a₀ S b = {i : DescriptiveComplexity.PartRed.pInterp.Map A | S i ∧ DescriptiveComplexity.BWBit i (DescriptiveComplexity.PartRed.pLow a₀ b)}.ncard

Instances For

Dependency graph

theorem DescriptiveComplexity.PartRed.sum_weights_eq_cnt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (S : pInterp.Map A → Prop) :

∑ᶠ (i : pInterp.Map A) (_ : i ∈ {i : pInterp.Map A | S i}), BWWeight i = digitNum blkLe (fun (x : Bool × A) => True) (pbase A) (cnt a₀ S)

Dependency graph

theorem DescriptiveComplexity.PartRed.cnt_add_cnt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (a₀ : A) {S : pInterp.Map A → Prop} (hS : ∀ (i : pInterp.Map A), S i → BWItem i) (b : Bool × A) :

cnt a₀ S b + cnt a₀ (fun (i : pInterp.Map A) => BWItem i ∧ ¬S i) b = cnt a₀ BWItem b

A selection and the items it leaves out split every digit.

Dependency graph

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

theorem DescriptiveComplexity.PartRed.bit_pLow_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (x : A) (i : pInterp.Map A) :

BWBit i (pLow a₀ (false , x)) ↔ ∃ (s : Bool), i = pLit a₀ s x

The items carrying a bit in a variable block are the two literals of that variable.

Dependency graph

theorem DescriptiveComplexity.PartRed.bit_pLow_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (c : A) (i : pInterp.Map A) :

BWBit i (pLow a₀ (true , c)) ↔ (∃ (p : A × Bool), SatOcc.OccIn c p.1 p.2 ∧ i = pLit a₀ p.2 p.1) ∨ (∃ (p : A × Bool), SatOcc.Mid c p.1 p.2 ∧ i = pSlk p.2 c p.1) ∨ SatOcc.EmptyCl c ∧ i = pEmp a₀ c

The items carrying a bit in a clause block are the literals occurring in the clause, its slack items, and its own item if it is empty.

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

theorem DescriptiveComplexity.PartRed.cnt_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (S : pInterp.Map A → Prop) (x : A) :

cnt a₀ S (false , x) = {s : Bool | S (pLit a₀ s x)}.ncard

The digit of a variable block counts the selected literals of that variable.

Dependency graph

theorem DescriptiveComplexity.PartRed.cnt_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (S : pInterp.Map A → Prop) (c : A) :

cnt a₀ S (true , c) = {p : A × Bool | p ∈ SatOcc.OccSet c ∧ S (pLit a₀ p.2 p.1)}.ncard + {p : A × Bool | p ∈ SatOcc.MidSet c ∧ S (pSlk p.2 c p.1)}.ncard + if SatOcc.EmptyCl c ∧ S (pEmp a₀ c) then 1 else 0

The digit of a clause block counts the selected literals occurring in the clause, its selected slack items, and its own item if it is empty.

Dependency graph

theorem DescriptiveComplexity.PartRed.cnt_item_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (x : A) :

cnt a₀ BWItem (false , x) = 2

Every variable block totals two: a balanced split takes exactly one of the two literals of the variable.

Dependency graph

theorem DescriptiveComplexity.PartRed.cnt_item_cls {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) (c : A) :

cnt a₀ BWItem (true , c) = (SatOcc.OccSet c).ncard + (SatOcc.MidSet c).ncard + if SatOcc.EmptyCl c then 1 else 0

A clause block totals its occurrences plus its slack occurrences, plus one if the clause is empty.

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

theorem DescriptiveComplexity.PartRed.cnt_le {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (a₀ : A) {S : pInterp.Map A → Prop} (hS : ∀ (i : pInterp.Map A), S i → BWItem i) (b : Bool × A) :

cnt a₀ S b ≤ cnt a₀ BWItem b

A selection weighs at most as much as all the items, digit by digit.

Dependency graph

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

cnt a₀ BWItem b < pbase A

No carry: every digit the gadget writes stays below the base, 3 |A| bits being more than the 4 |A| + 1 items a block can hold.

Dependency graph

theorem DescriptiveComplexity.PartRed.sum_eq_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) {S : pInterp.Map A → Prop} (hS : ∀ (i : pInterp.Map A), S i → BWItem i) :

∑ᶠ (i : pInterp.Map A) (_ : i ∈ {i : pInterp.Map A | S i}), BWWeight i = ∑ᶠ (i : pInterp.Map A) (_ : i ∈ {i : pInterp.Map A | BWItem i ∧ ¬S i}), BWWeight i ↔ ∀ (b : Bool × A), 2 * cnt a₀ S b = cnt a₀ BWItem b

The balance condition, digit by digit: a selection weighs as much as the items it leaves out exactly when it takes half of every digit.

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

def DescriptiveComplexity.PartRed.TrueSet {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) (c : A) :

Set (A × Bool)

The true occurrences of a clause under an assignment.

Equations

DescriptiveComplexity.PartRed.TrueSet ν c = {p : A × Bool | p ∈ DescriptiveComplexity.SatOcc.OccSet c ∧ DescriptiveComplexity.SatOcc.LitTrue ν p.1 p.2}

Instances For

Dependency graph

Correctness of the reduction #

theorem DescriptiveComplexity.PartRed.litTrue_iff_sel {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {S : pInterp.Map A → Prop} (hbal : ∀ (b : Bool × A), 2 * cnt a₀ S b = cnt a₀ BWItem b) (x : A) (s : Bool) :

S (pLit a₀ s x) ↔ SatOcc.LitTrue (fun (y : A) => S (pLit a₀ true y)) x s

A balanced split is an assignment: the two literals of a variable split its block, so exactly one of them is selected.

Dependency graph

theorem DescriptiveComplexity.PartRed.exists_occ_selected {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) {S T : pInterp.Map A → Prop} (hcompl : ∀ (i : pInterp.Map A), BWItem i → (S i ↔ ¬T i)) (hbal : ∀ (b : Bool × A), cnt a₀ S b = cnt a₀ T b) {c : A} (hc : SatOcc.IsCl c) :

∃ p ∈ SatOcc.OccSet c, S (pLit a₀ p.2 p.1)

A balanced split satisfies every clause, not all equal: if no occurrence of a clause were selected, the slack of that clause – strictly fewer items than it has occurrences – would have to make up for all of them, and an empty clause could not be split at all.

Dependency graph

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