Exact block indexing for positive clause replacements

The positive compiler numbers auxiliaries by the position of their signed source clause. When signed clauses are themselves emitted in blocks, local drawings use local clause indices. Shifting those indices by the preceding signed block lengths gives exactly the original compiler's formula, including its variable names and clause order.

Main definitions

• PositiveExactOne.shift: translate the signed-clause index of positive auxiliaries.
• PositiveExactOne.formulaFrom: the positive compiler starting at a supplied clause index.
• PositiveExactOne.compileBlocks: compile signed blocks with their actual global offsets.

Main results

• PositiveExactOne.formula_flatten: exact global formula as separately compiled blocks.
• PositiveExactOneCompile.rawFormula_eq_blocks: partition by original source clauses.

References

These are original indexing identities for the two local compilers.

def Cslib.Logic.PL.CNF.PositiveExactOne.shift {V : Type u_1} (offset : ℕ) : Variable V → Variable V

Add the signed-clause offset to new positive auxiliaries, fixing source variables.

def Cslib.Logic.PL.CNF.PositiveExactOne.formulaFrom {V : Type u_1} (start : ℕ) (φ : CNF V) : CNF (Variable V)

Compile a signed formula whose first clause has the given global index.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.positiveLiteral_shift {V : Type u_1} (offset i j : ℕ) (l : Literal V) : (shift offset (positiveLiteral i j l).1, (positiveLiteral i j l).2) = positiveLiteral (offset + i) j l

Shifting preserves the source role of every terminal and shifts each private slot.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.complementBlock_shift {V : Type u_1} (offset i j : ℕ) (l : Literal V) : relabel (shift offset) (complementBlock i j l) = complementBlock (offset + i) j l

A complement block is equivariant under shifting its signed-clause index.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.clauseClauses_shift {V : Type u_1} (offset i : ℕ) (c : Clause V) : relabel (shift offset) (clauseClauses i c) = clauseClauses (offset + i) c

The entire local clause replacement shifts to its actual global clause index.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.formulaFrom_eq_relabel {V : Type u_1} (start : ℕ) (φ : CNF V) : formulaFrom start φ = relabel (shift start) (formula φ)

Starting a compiler at a nonzero index renames just its fresh auxiliaries.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.formulaFrom_append {V : Type u_1} (start : ℕ) (φ ψ : CNF V) : formulaFrom start (φ ++ ψ) = formulaFrom start φ ++ formulaFrom (start + List.length φ) ψ

Compiling a concatenation gives the second part its exact signed-clause offset.

def Cslib.Logic.PL.CNF.PositiveExactOne.compileBlocks {V : Type u_1} (start : ℕ) : List (CNF V) → CNF (Variable V)

Compile consecutive signed blocks with their true cumulative signed-clause offsets.

def Cslib.Logic.PL.CNF.PositiveExactOne.blockOffset {V : Type u_1} (bs : List (CNF V)) (i : ℕ) : ℕ

Number of signed clauses before one block.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.compileBlocks_eq_flatMap {V : Type u_1} (start : ℕ) (bs : List (CNF V)) : compileBlocks start bs = List.flatMap (fun (b : CNF V × ℕ) => relabel (shift (start + blockOffset bs b.2)) (formula b.1)) bs.zipIdx

The recursive partition is also an indexed concatenation with explicit prefix offsets.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.formulaFrom_flatten {V : Type u_1} (start : ℕ) (bs : List (CNF V)) : formulaFrom start bs.flatten = compileBlocks start bs

The blockwise compiler is exactly the indexed compiler on the flattened signed input.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.formula_flatten {V : Type u_1} (bs : List (CNF V)) : formula bs.flatten = compileBlocks 0 bs

Exact formula and fresh-variable names for the block partition at index zero.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.rawFormula_eq_blocks {V : Type u_1} (φ : CNF V) : rawFormula φ = PositiveExactOne.compileBlocks 0 (List.map (fun (c : Clause V × ℕ) => FromSAT.clause c.2 c.1) (List.zipIdx φ))

The actual positive formula is the concatenation of locally compiled source-clause profiles, with outer auxiliaries shifted by signed-block lengths.

def Cslib.Logic.PL.CNF.PositiveExactOneCompile.signedOffset {V : Type u_1} (φ : CNF V) (i : ℕ) : ℕ

The actual signed-clause offset of the replacement of original clause i.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.rawFormula_eq_flatMap {V : Type u_1} (φ : CNF V) : rawFormula φ = List.flatMap (fun (c : Clause V × ℕ) => relabel (PositiveExactOne.shift (signedOffset φ c.2)) (PositiveExactOne.formula (FromSAT.clause c.2 c.1))) (List.zipIdx φ)

Exact original-clause partition, in source order, with actual global auxiliary names.