Geometry of the paired-port compiler #
The compiler reuses the canonical unit paths. Paired accesses have disjoint supports, and their only boundary contacts identify the same lane of the same unit grid edge. All geometric assertions concern entire real supports.
Main results #
access_eq_translate: every actual access uses the common fixed paired-port interface.route_contacts,routes_contacts: continuous endpoint-only contacts of the actual routes.isPlanarOrthogonalDrawing: the actual compact formula's continuous drawing certificate.
References #
The paired macrocell assembly is original.
Within one cell, boundary positions identify both the side and the lane.
Every actual access is proper and orthogonal.
Every actual access is continuously simple.
All actual access routes have the same fixed cost.
Every actual access stays in its closed cell and touches its boundary only at its port.
Contacts between accesses in different cells occur at both designated boundary ports.
Distinct paired ports of one cell have disjoint continuous accesses.
Equality of paired seam points identifies the lane and the old single seam midpoint.
All actual unit steps are proper; this includes final steps into clause cells.
Paired seam points of every actual path step are all distinct, including final steps.
Every original clause cell is disjoint from all ordinary tiles.
Every actual final literal route is proper, orthogonal and continuously simple.
The final incidence starts at its clause center and ends at its actual signal variable.
Every route in a placed seam clause is an actual paired access.
Every route in a seam clause is proper, orthogonal and continuously simple.
Seam incidence routes match their literal variables in both lane orientations.
Every seam literal uses one of its two actual presented signals.
Every structured variable lies strictly inside its indexed macrocell.
Every raw variable has the tag prescribed by its cell's kind.
Actual variable positions identify their structured names.
The variable-position prefix of the actual drawing has no repetitions.
The actual drawing has exactly the compact incidence graph's number of vertices.
Compaction preserves the ordered incidence graph.
Every actual output route is proper, orthogonal and continuously simple.
Each actual placed clause supplies exactly one route per literal, in literal order.
The actual route count is the edge count of the final compact incidence graph.
Every actual literal/route pair has the clause and variable endpoints in its record.
The final incidence is exactly one translated clause spoke and one neighboring access.
Matching paired boundaries of actual occurrence steps identify the whole occurrence and oriented step, as well as the lane.
A raw variable's incidence-graph index resolves to its actual geometric position.
A raw clause's incidence-graph index resolves to its actual placed clause position.
Actual indexed routes have the final compact incidence graph's endpoints, in clause-to- variable order, including repeated literal incidences.
Every emitted variable lies in a selected crossing or a retained occupied path cell.
No actual variable is placed in an original clause cell.
Every translated original-clause spoke stays in its clause cell.
Every translated ordinary core incidence is strictly inside its cell.
Every translated crossover core incidence is strictly inside its cell.
An actual access visits a correctly tagged variable only at its own endpoint.
Every actual route can meet an emitted variable only at its variable endpoint.
Ordinary clause positions are strictly inside their cell.
Crossover clause positions are strictly inside their cell.
An ordinary tile retains the fixed ring's clause-position order.
A crossover tile retains the fixed paired crossover's clause-position order.
Emitted seam clause positions are a sublist of all paired path boundaries.
All actual paired-link clauses have distinct positions.
All actual original, ordinary, crossover and paired-seam clause positions are distinct.
Every actual incidence route contains at least two distinct endpoint positions.
Actual variable and clause position lists are disjoint.
Every actual displayed graph vertex has its own position.
A translated clause spoke touches its cell boundary only at the chosen paired port.
Distinct actual route values meet only at endpoints of both routes, over the complete real plane. Unit-step ownership includes the omitted final binary link.
Distinct actual incidence occurrences have distinct polygonal route lists.
Every actual route meets an actual clause vertex only at its own clause endpoint. The original-clause case includes isolated empty clauses.
Actual indexed routes avoid all nonincident declared graph vertices.
Actual indexed incidence routes meet only at their shared declared graph endpoints.
The actual paired-port compiler supplies a continuous planar orthogonal drawing. The only assumptions are source width and literal-occurrence bounds of three.