Native polynomial-time computation of the paired-port compiler

Original variable names and all integer coordinates use binary encodings. List positions and compact ranks use unary counters. The paths, crossing-site selection, and occurrence lookup reuse the original compiler's native polynomial-time implementations. Ordinary cells are selected from the retained path points by filtering and first-occurrence selection.

Only the local port tag has a fixed finite encoding: an ordinary side/lane pair or a paired crossover variable. Template tables and all finite dispatches are fixed independently of the input formula. Neither the input formulas nor their coordinate or variable domains are finite.

Main definitions

• encVariable: binary cell coordinates and a fixed finite local tag.
• encPlacedClause: the emitted clause, position, and literal incidence routes.

Main results

• computableInPolyTime_ordinaryCells: polynomial-time selection of occupied ordinary cells.
• computableInPolyTime_placedClauses, computableInPolyTime_rawFormula: actual compiler records.
• computableInPolyTime_formula: the compact formula under binary CNF encodings.
• computableInPolyTime_positions, computableInPolyTime_routes: its binary geometric data.

References

The compiler is the construction defined in PairedCompile.

@[instance_reducible]

def Cslib.Complexity.SAT.ParsimoniousPlanar.instFinEnumInternal : FinEnum Logic.PL.CNF.Crossover.Internal

Explicit constructive enumeration of the eight split internal crossover variables.

@[instance_reducible]

instance Cslib.Complexity.SAT.ParsimoniousPlanar.instFinEnumVariable : FinEnum Logic.PL.CNF.PairedCrossover.Variable

Explicit constructive enumeration of the 57 paired-crossover variables.

def Cslib.Complexity.SAT.ParsimoniousPlanar.encVariable : Variable ↪ List Bool

Binary cell coordinates together with a fixed finite ordinary-port or crossover tag.

def Cslib.Complexity.SAT.ParsimoniousPlanar.encPlacedClause : PlacedClause ↪ List Bool

A clause and its binary position and incidence-route data.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.computableInPolyTime_ordinaryCells : Turing.MultiTapeTM.ComputableInPolyTime ordinaryCells encCNF Orthogonal.encRoute

Ordinary cells are selected from polynomial-size retained paths, without enumerating a coordinate box or a domain depending on the numeric magnitude of an input label.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.computableInPolyTime_placedClauses : Turing.MultiTapeTM.ComputableInPolyTime placedClauses encCNF (Turing.MultiTapeTM.encList encPlacedClause)

The complete actual list of emitted clauses and drawing records is native polynomial-time.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.computableInPolyTime_rawFormula : Turing.MultiTapeTM.ComputableInPolyTime rawFormula encCNF (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encVariable Turing.MultiTapeTM.encBool)))

Projecting the actual records computes the structured output formula.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.computableInPolyTime_formula : Turing.MultiTapeTM.ComputableInPolyTime formula encCNF encCNF

The actual compact formula compiler is native polynomial-time under binary CNF encodings. Compact ranks are computed as unary counters and then encoded in binary.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.computableInPolyTime_positions : Turing.MultiTapeTM.ComputableInPolyTime positions encCNF Orthogonal.encRoute

All actual output vertex positions are computed in polynomial time with binary coordinates.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.computableInPolyTime_routes : Turing.MultiTapeTM.ComputableInPolyTime routes encCNF (Turing.MultiTapeTM.encList Orthogonal.encRoute)

All actual clause-to-variable incidence routes are computed in polynomial time with binary coordinates.