The base graph, as an algorithm sees it

The constraint graph of a 3CNF formula has three edges per clause, a vertex per variable and a vertex per clause. This module computes those numbers and those endpoints from the formula's encoding, in polynomial time.

The vertex numbering puts variables first, so a clause vertex sits at maxVar + 1 + j; both quantities are read off the encoding by the loops of MaxLoop and the parser.

Main definitions

• Complexity.baseEdgesU — the edge count, in unary
• Complexity.baseMaxU — the largest variable index, in unary

Main results

• Complexity.baseEdgesU_eq, Complexity.baseMaxU_eq — what they compute
• Complexity.baseTailU_eq, Complexity.baseHeadU_eq — the two endpoints
• Complexity.baseKey_mem_FP, Complexity.length_baseKey_le — the constraint's bounded key
• Complexity.baseOk_mem_P — the constraint is polynomial-time decidable
• Complexity.baseAlg — the base graph as an AlgCSP
• Complexity.baseAlg_numEdges_eq, Complexity.baseAlg_tail_eq, Complexity.baseAlg_head_eq — it agrees with baseCSP
• Complexity.card_gapAlpha — the alphabet fits in 23 bits
• Complexity.litSignFn_encode — the sign flag is the literal's sign
• Complexity.baseAlg_models — the base graph is modelled faithfully

noncomputable def Complexity.baseEdgesU (E : List Bool → List Bool) (z : List Bool) : List Bool

The number of edges, in unary: three per clause.

Equations

• Complexity.baseEdgesU E z = Complexity.clauseCountFn (E z) ++ Complexity.clauseCountFn (E z) ++ Complexity.clauseCountFn (E z)

theorem Complexity.baseEdgesU_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) : baseEdgesU E ∈ FP

theorem Complexity.baseEdgesU_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (x : List Bool) : baseEdgesU E x = List.replicate (3 * List.length (Φ x)) true

noncomputable def Complexity.baseMaxU (E : List Bool → List Bool) (z : List Bool) : List Bool

The largest variable index, in unary.

Equations

• Complexity.baseMaxU E z = Complexity.maxFn Complexity.slotVar (Complexity.pair (Complexity.baseEdgesU E z) (E z))

theorem Complexity.baseMaxU_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) : baseMaxU E ∈ FP

theorem Complexity.baseMaxU_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) : (baseMaxU E x).length = (Φ x).maxVar

noncomputable def Complexity.baseTailU (E : List Bool → List Bool) (w : List Bool) : List Bool

The unary form of the first endpoint: the clause vertex.

Equations

• Complexity.baseTailU E w = Complexity.baseMaxU E (Complexity.pairFst w) ++ [true] ++ List.replicate (Complexity.divFn [false, false, false] (Complexity.pairSnd w)).length true

noncomputable def Complexity.baseHeadU (E : List Bool → List Bool) (w : List Bool) : List Bool

The unary form of the second endpoint: the variable vertex.

Equations

• Complexity.baseHeadU E w = Complexity.slotVar (Complexity.pair (E (Complexity.pairFst w)) (Complexity.pairSnd w))

theorem Complexity.baseTailU_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) : baseTailU E ∈ FP

theorem Complexity.baseHeadU_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) : baseHeadU E ∈ FP

What the endpoints compute

theorem Complexity.baseTailU_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (e : ℕ) : (baseTailU E (pair x (List.replicate e true))).length = (Φ x).maxVar + 1 + e / 3

theorem Complexity.baseHeadU_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) {e : ℕ} (he : e < 3 * List.length (Φ x)) : (baseHeadU E (pair x (List.replicate e true))).length = (ThreeSATCSP.litOf (Φ x) (e / 3) ⟨e % 3, ⋯⟩).var

The key the constraint looks at

noncomputable def Complexity.baseSigns (E : List Bool → List Bool) (z : List Bool) : List Bool

The three literal signs of the clause an edge belongs to.

Equations

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

noncomputable def Complexity.baseKey (E : List Bool → List Bool) (w : ℕ) (z : List Bool) : List Bool

Everything the constraint depends on: the clause's signs, the position inside the clause, and the two symbol blocks.

Equations

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

theorem Complexity.baseSigns_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) : baseSigns E ∈ FP

theorem Complexity.baseKey_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) (w : ℕ) : baseKey E w ∈ FP

theorem Complexity.length_baseSigns_le (E : List Bool → List Bool) (z : List Bool) : (baseSigns E z).length ≤ 3

theorem Complexity.length_baseKey_le (E : List Bool → List Bool) (w : ℕ) (z : List Bool) : (baseKey E w z).length ≤ 2 * w + 22

The constraint

noncomputable def Complexity.baseOkKey (w : ℕ) (k : List Bool) : Prop

What the constraint says, as a predicate of the key alone: the two blocks name symbols in the image of the alphabet embedding whose preimages satisfy the clause and agree on the checked position.

Equations

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

noncomputable def Complexity.baseOk (E : List Bool → List Bool) (w : ℕ) : Language

The constraint, as a language on the verifier's verdict argument.

Equations

• Complexity.baseOk E w = {z : List Bool | Complexity.baseOkKey w (Complexity.baseKey E w z)}

theorem Complexity.baseOk_mem_P (E : List Bool → List Bool) (hE : E ∈ FP) (w : ℕ) : baseOk E w ∈ P

The record

noncomputable def Complexity.baseAlg (E : List Bool → List Bool) (hE : E ∈ FP) : AlgCSP

The base graph as an algorithm.

Equations

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

@[simp]

theorem Complexity.numEdges_baseAlg (E : List Bool → List Bool) (hE : E ∈ FP) (x : List Bool) : (baseAlg E hE).numEdges x = (baseEdgesU E x).length

@[simp]

theorem Complexity.width_baseAlg (E : List Bool → List Bool) (hE : E ∈ FP) : (baseAlg E hE).width = 23

theorem Complexity.vert_baseAlg_false (E : List Bool → List Bool) (hE : E ∈ FP) (x : List Bool) (e : ℕ) : (baseAlg E hE).vert false x e = (baseTailU E (pair x (List.replicate e true))).length

theorem Complexity.vert_baseAlg_true (E : List Bool → List Bool) (hE : E ∈ FP) (x : List Bool) (e : ℕ) : (baseAlg E hE).vert true x e = (baseHeadU E (pair x (List.replicate e true))).length

@[simp]

theorem Complexity.ok_baseAlg (E : List Bool → List Bool) (hE : E ∈ FP) : (baseAlg E hE).ok = baseOk E 23

The symbol codec fits

theorem Complexity.card_gapAlpha : Fintype.card GapAlpha = 2 ^ 23

theorem Complexity.length_symEnc_gapAlpha (s : GapAlpha) : (symEnc GapAlpha 23 s).length = 23

theorem Complexity.symDec_symEnc_gapAlpha (s : GapAlpha) : symDec GapAlpha (symEnc GapAlpha 23 s) = s

The sign flag

theorem Complexity.litSignFn_encode (φ : SAT.CNF) {j p : ℕ} (hj : j < List.length φ) (hp : p < List.length φ[j]) : litSignFn (pair (pair (List.replicate j true) (List.replicate p true)) φ.encode) = [φ[j][p].sign]

theorem Complexity.litOf_eq (φ : SAT.CNF) {j : ℕ} (hj : j < List.length φ) (p : Fin 3) (hq : ↑p < List.length φ[j]) : ThreeSATCSP.litOf φ j p = φ[j][↑p]

Agreement with the real graph

theorem Complexity.baseAlg_numEdges_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE' : E ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (x : List Bool) : (baseAlg E hE').numEdges x = (baseCSP (Φ x)).numEdges

theorem Complexity.baseAlg_tail_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE' : E ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (e : ℕ) (he : e < (baseCSP (Φ x)).numEdges) : (baseAlg E hE').vert false x e = ↑((baseCSP (Φ x)).tail ⟨e, he⟩)

theorem Complexity.baseAlg_head_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE' : E ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (e : ℕ) (he : e < (baseCSP (Φ x)).numEdges) : (baseAlg E hE').vert true x e = ↑((baseCSP (Φ x)).head ⟨e, he⟩)

The key on a well-formed argument

theorem Complexity.baseSigns_pair (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) {e : ℕ} (he : e < 3 * List.length (Φ x)) (a : List Bool) : baseSigns E (pair (pair x (List.replicate e true)) a) = [(ThreeSATCSP.litOf (Φ x) (e / 3) 0).sign, (ThreeSATCSP.litOf (Φ x) (e / 3) 1).sign, (ThreeSATCSP.litOf (Φ x) (e / 3) 2).sign]

theorem Complexity.baseKey_pair (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) {e : ℕ} (he : e < 3 * List.length (Φ x)) {a : List Bool} (ha : a.length = 46) : baseKey E 23 (pair (pair x (List.replicate e true)) a) = pair (pair [(ThreeSATCSP.litOf (Φ x) (e / 3) 0).sign, (ThreeSATCSP.litOf (Φ x) (e / 3) 1).sign, (ThreeSATCSP.litOf (Φ x) (e / 3) 2).sign] (List.replicate (e % 3) true)) a

The constraint agrees

theorem Complexity.baseAlg_ok_iff (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE' : E ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (e : ℕ) (he : e < (baseCSP (Φ x)).numEdges) (u v : List Bool) (hu : u.length = 23) (hv : v.length = 23) : pair (pair x (List.replicate e true)) (u ++ v) ∈ (baseAlg E hE').ok ↔ (baseCSP (Φ x)).rel ⟨e, he⟩ (symDec GapAlpha u) (symDec GapAlpha v) = true

theorem Complexity.baseAlg_models (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE' : E ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) : (baseAlg E hE').Models (fun (x : List Bool) => baseCSP (Φ x)) (symEnc GapAlpha 23) (symDec GapAlpha)

The base graph is modelled faithfully.