Gluing CNF gadgets with private auxiliary variables

A gadget has shared variables V and auxiliary variables W. Gluing a finite list of gadgets tags every auxiliary variable with its site, keeping auxiliary variables of different sites distinct. Only the shared variables connect the gadgets. A shared assignment extends to the assembled formula exactly when it extends to every gadget separately.

This is the semantic substitution rule used when finite SAT reductions replace crossings by fixed gadgets. It concerns satisfiability; geometric compatibility and resource bounds are separate obligations.

Main definitions

• Cslib.Logic.PL.CNF.glue: assemble gadgets with site-tagged auxiliary variables.

Main results

• Cslib.Logic.PL.CNF.eval_glue: evaluate the assembled formula one gadget at a time.
• Cslib.Logic.PL.CNF.exists_eval_glue_iff: local auxiliary assignments can be chosen independently for a fixed shared assignment.
• Cslib.Logic.PL.CNF.satisfiable_glue_iff: the satisfiability substitution rule.
• Cslib.Logic.PL.CNF.length_glue, Cslib.Logic.PL.CNF.length_vars_glue: exact size identities.

References

This indexed-list formulation of gadget gluing and its proofs are original.

def Cslib.Logic.PL.CNF.glue {V : Type u_1} {W : Type u_2} {I : Type u_3} (sites : List I) (gadget : I → CNF (V ⊕ W)) : CNF (V ⊕ I × W)

Assemble gadgets sharing V, tagging each auxiliary variable with its gadget site. Repeated sites repeat the same constraints and the same auxiliary variables.

theorem Cslib.Logic.PL.CNF.eval_glue {V : Type u_1} {W : Type u_2} {I : Type u_3} (sites : List I) (gadget : I → CNF (V ⊕ W)) (σ : V ⊕ I × W → Bool) : eval σ (glue sites gadget) = true ↔ ∀ (i : I), i ∈ sites → eval (Sum.elim (fun (v : V) => σ (Sum.inl v)) fun (w : W) => σ (Sum.inr (i, w))) (gadget i) = true

A global assignment satisfies the assembly exactly when it satisfies every relabelled gadget.

theorem Cslib.Logic.PL.CNF.exists_eval_glue_iff {V : Type u_1} {W : Type u_2} {I : Type u_3} (sites : List I) (gadget : I → CNF (V ⊕ W)) (σ : V → Bool) : (∃ (τ : I × W → Bool), eval (Sum.elim σ τ) (glue sites gadget) = true) ↔ ∀ (i : I), i ∈ sites → ∃ (τ : W → Bool), eval (Sum.elim σ τ) (gadget i) = true

For a fixed assignment of the shared variables, the private assignments of distinct gadgets can be chosen independently.

theorem Cslib.Logic.PL.CNF.satisfiable_glue_iff {V : Type u_1} {W : Type u_2} {I : Type u_3} (sites : List I) (gadget : I → CNF (V ⊕ W)) : (glue sites gadget).Satisfiable ↔ ∃ (σ : V → Bool), ∀ (i : I), i ∈ sites → ∃ (τ : W → Bool), eval (Sum.elim σ τ) (gadget i) = true

The assembly is satisfiable exactly when one shared assignment extends to each local gadget.

theorem Cslib.Logic.PL.CNF.length_glue {V : Type u_1} {W : Type u_2} {I : Type u_3} (sites : List I) (gadget : I → CNF (V ⊕ W)) : List.length (glue sites gadget) = (List.map (fun (i : I) => List.length (gadget i)) sites).sum

The number of clauses is the sum of the numbers of clauses in the local gadgets.

theorem Cslib.Logic.PL.CNF.length_vars_glue {V : Type u_1} {W : Type u_2} {I : Type u_3} (sites : List I) (gadget : I → CNF (V ⊕ W)) : (glue sites gadget).vars.length = (List.map (fun (i : I) => (gadget i).vars.length) sites).sum

Relabelling and gluing preserve every literal occurrence, including repetitions.