Constant-factor costs of the actual positive drawing compiler

Costs are counted on the actual emitted route lists. The source-slot sequence of every fixed profile contains each source occurrence once. Consequently inherited exteriors are charged once, while every original clause receives only a fixed local route, segment and wire budget.

Main results

• clauseGeometry_local_costs: fixed segment and wire budgets for the actual local replacements.
• positiveDrawing_costs: constant-factor actual vertex, route, segment and wire bounds.

References

The exact finite-list accounting and cost estimates are original.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_local_costs {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < List.length φ) (c : Logic.PL.Clause ℕ) : (List.map (fun (e : LocalIncidence) => (List.consecutivePairs e.route).length) (clauseGeometry φ d i c).incidenceRoutes).sum ≤ 575 ∧ (List.map (fun (e : LocalIncidence) => Orthogonal.wireLength e.route) (clauseGeometry φ d i c).incidenceRoutes).sum ≤ 40252600

The actual collared local template has bounded total segment and Manhattan-wire costs. The conservative collar allowance is charged once per local incidence.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_routeCount (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : (positiveDrawing φ d).2.length ≤ 507 * List.length φ

The actual route list has at most 507 incidences per original clause.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_vertexCount_le (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : (positiveDrawing φ d).1.length ≤ 676 * List.length φ

The actual vertex list has at most 676 vertices per original clause.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_segmentCount {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) (hw : ∀ c ∈ φ, List.length c ≤ 3) : Graph.drawingSegmentCount (positiveDrawing φ d) ≤ 575 * List.length φ + Graph.drawingSegmentCount d

Each original source segment is retained once; every original clause contributes only a fixed local segment allowance.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_wireLength {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) (hw : ∀ c ∈ φ, List.length c ≤ 3) : Graph.drawingWireLength (positiveDrawing φ d) ≤ 40252600 * List.length φ + 1080000 * Graph.drawingWireLength d

Each inherited source wire is charged once after the fixed dilation. The rest is a constant local wire allowance per original clause.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_costs {φ : Logic.PL.CNF ℕ} {d : Graph.OrthogonalDrawing} (hd : (incidenceGraph φ).IsPlanarOrthogonalDrawing d) (hw : ∀ c ∈ φ, List.length c ≤ 3) : (positiveDrawing φ d).1.length ≤ 676 * List.length φ ∧ (positiveDrawing φ d).2.length ≤ 507 * List.length φ ∧ Graph.drawingSegmentCount (positiveDrawing φ d) ≤ 575 * List.length φ + Graph.drawingSegmentCount d ∧ Graph.drawingWireLength (positiveDrawing φ d) ≤ 40252600 * List.length φ + 1080000 * Graph.drawingWireLength d

All actual emitted drawing costs grow by only fixed factors. Inherited exterior incidences are counted exactly once, independently of source variable repetitions.