Documentation

Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting

Unique extensions through the fixed crossover #

The fixed clause tables have exactly one satisfying full assignment for each pair of incoming bits. The explicit Boolean extension and its uniqueness are preserved by the internal splitting rings. Construction and source credit are documented in Crossover and CrossoverSplit.

Main definitions #

Main results #

References #

The construction adapts [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)]. Unique extension is the parsimony condition of [HuntMaratheRadhakrishnanStearns1998, Definition 3.1]. Their Theorem 3.2 proves that property for Lichtenstein's crossover; kernel evaluation checks the adapted 13-variable table here.

source
def Cslib.Logic.PL.CNF.Crossover.canonicalExtension (a b : Bool) :
Variable → Bool

The full satisfying assignment determined by the left and top input values. The explicit Boolean expressions describe all nine internal values as well as the outputs.

Instances For
    source
    theorem Cslib.Logic.PL.CNF.Crossover.eval_canonicalExtension (a b : Bool) :
    eval (canonicalExtension a b) formula = true

    The explicit extension satisfies all 26 clauses for every pair of inputs.

    source
    theorem Cslib.Logic.PL.CNF.Crossover.eq_canonicalExtension_of_holds {σ : Variable → Bool} (h : eval σ formula = true) :
    σ = canonicalExtension (σ Variable.aLeft) (σ Variable.bTop)

    Every satisfying full assignment is the explicit extension of its two incoming values.

    source
    theorem Cslib.Logic.PL.CNF.Crossover.ext_of_holds {σ τ : Variable → Bool} (hσ : eval σ formula = true) (hτ : eval τ formula = true) (ha : σ Variable.aLeft = τ Variable.aLeft) (hb : σ Variable.bTop = τ Variable.bTop) :
    σ = τ

    Satisfying assignments agreeing on the incoming ports agree on every variable.

    source
    theorem Cslib.Logic.PL.CNF.Crossover.existsUnique_holds (a b : Bool) :
    ∃! σ : Variable → Bool, eval σ formula = true ∧ σ Variable.aLeft = a ∧ σ Variable.bTop = b

    Each pair of incoming values extends uniquely to a satisfying full assignment.

    source
    def Cslib.Logic.PL.CNF.Crossover.canonicalSplitExtension (a b : Bool) :
    SplitVariable → Bool

    The explicit full split assignment: every local copy receives its original variable's canonical value, determined by the left and top inputs.

    Instances For
      source
      theorem Cslib.Logic.PL.CNF.Crossover.eval_canonicalSplitExtension (a b : Bool) :
      eval (canonicalSplitExtension a b) splitFormula = true

      The canonical split extension satisfies all 74 clauses.

      source
      theorem Cslib.Logic.PL.CNF.Crossover.eq_canonicalSplitExtension_of_holds {σ : SplitVariable → Bool} (h : eval σ splitFormula = true) :
      σ = canonicalSplitExtension (σ SplitVariable.aLeft) (σ SplitVariable.bTop)

      Every satisfying split assignment is the explicit extension of its incoming values. The implication rings identify the six copies before applying the original uniqueness result; no enumeration of assignments to the 53 split variables is needed.

      source
      theorem Cslib.Logic.PL.CNF.Crossover.split_ext_of_holds {σ τ : SplitVariable → Bool} (hσ : eval σ splitFormula = true) (hτ : eval τ splitFormula = true) (ha : σ SplitVariable.aLeft = τ SplitVariable.aLeft) (hb : σ SplitVariable.bTop = τ SplitVariable.bTop) :
      σ = τ

      Satisfying split assignments agreeing on the two incoming ports agree everywhere.

      source
      theorem Cslib.Logic.PL.CNF.Crossover.existsUnique_split_holds (a b : Bool) :
      ∃! σ : SplitVariable → Bool, eval σ splitFormula = true ∧ σ SplitVariable.aLeft = a ∧ σ SplitVariable.bTop = b

      Each pair of incoming values extends uniquely to a satisfying full split assignment.