Planar 3SAT with three literal occurrences per variable

Clauses have width at most three, including binary clauses, and each variable has at most three literal occurrences. Planarity is witnessed by a finite integer orthogonal incidence drawing: routes are simple, avoid nonincident vertices, and intersect only at shared endpoints, with all contacts interpreted on full real segments. Parallel literal incidences are retained.

DrawnPlanarThreeSATThree supplies the drawing as part of the input. PlanarThreeSATThree requires its existence. The total compiler rejects inputs outside the syntactic restrictions by returning one empty clause and a one-vertex drawing.

The compiler is parsimonious: its paired implications force equality along each wire, and the local rings and crossover have unique extensions. Counts refer only to occurring variables.

Main definitions

• DrawnPlanarThreeSATThreeInstance, encDrawnPlanarThreeSATThree: supplied-drawing instances and their binary encoding.
• PlanarThreeSATThree, DrawnPlanarThreeSATThree: formula and supplied-drawing problems.
• toDrawnPlanarThreeSATThree, toPlanarThreeSATThree: total finite compilers.

Main results

• PlanarThreeSATThree_npHard, DrawnPlanarThreeSATThree_npHard: NP-hardness with an existential or supplied integer orthogonal incidence drawing.
• computableInPolyTime_toDrawnPlanarThreeSATThree, computableInPolyTime_toPlanarThreeSATThree: native polynomial-time computation.
• satisfiable_toPlanarThreeSAT_iff: total correctness after occurrence splitting.
• modelCount_toPlanarThreeSATThree, modelCount_toPlanarThreeSAT: exact count preservation on valid source syntax.
• toDrawnPlanarThreeSAT_fits, toDrawnPlanarThreeSAT_costs: explicit linear grid sides and quadratic formula, incidence-route, segment and Manhattan wire costs, measured against the original formula's clause and literal counts.

References

• Parsimonious planarization: Theorem 3.2 and Claim 3.3 of Hunt, Marathe, Radhakrishnan and Stearns.

The paired-port tiling, degree-three templates and explicit grid bounds are original. The fixed crossover's source credit is documented in Crossover.

structure Cslib.Complexity.DrawnPlanarThreeSATThreeInstance : Type

An instance of DrawnPlanarThreeSATThree: a CNF formula paired with a finite integer orthogonal drawing of its incidence graph.

• formula : Logic.PL.CNF ℕ

  The CNF formula.

• drawing : Graph.OrthogonalDrawing

  The supplied integer orthogonal incidence drawing.

theorem Cslib.Complexity.DrawnPlanarThreeSATThreeInstance.ext_iff {x y : DrawnPlanarThreeSATThreeInstance} : x = y ↔ x.formula = y.formula ∧ x.drawing = y.drawing

theorem Cslib.Complexity.DrawnPlanarThreeSATThreeInstance.ext {x y : DrawnPlanarThreeSATThreeInstance} (formula : x.formula = y.formula) (drawing : x.drawing = y.drawing) : x = y

def Cslib.Complexity.instDecidableEqDrawnPlanarThreeSATThreeInstance.decEq (x✝ x✝¹ : DrawnPlanarThreeSATThreeInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqDrawnPlanarThreeSATThreeInstance : DecidableEq DrawnPlanarThreeSATThreeInstance

@[instance_reducible]

instance Cslib.Complexity.instReprDrawnPlanarThreeSATThreeInstance : Repr DrawnPlanarThreeSATThreeInstance

def Cslib.Complexity.instReprDrawnPlanarThreeSATThreeInstance.repr : DrawnPlanarThreeSATThreeInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instInhabitedDrawnPlanarThreeSATThreeInstance : Inhabited DrawnPlanarThreeSATThreeInstance

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CNF ℕ} {T0 S0 : γ → ℕ} {x1 : γ → Graph.OrthogonalDrawing} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encCNF T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Graph.encOrthogonalDrawing T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { formula := x0 x, drawing := x1 x }) encIn encDrawnPlanarThreeSATThree (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_formula_inO : Turing.MultiTapeTM.ComputableInO DrawnPlanarThreeSATThreeInstance.formula encDrawnPlanarThreeSATThree encCNF (fun (a : DrawnPlanarThreeSATThreeInstance) => (encDrawnPlanarThreeSATThree a).length) fun (a : DrawnPlanarThreeSATThreeInstance) => (encDrawnPlanarThreeSATThree a).length

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Logic.PL.CNF ℕ × Graph.OrthogonalDrawing) => { formula := p.1, drawing := p.2 }) encDrawnPlanarThreeSATThreeFields encDrawnPlanarThreeSATThree 1 1

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_drawing_inO : Turing.MultiTapeTM.ComputableInO DrawnPlanarThreeSATThreeInstance.drawing encDrawnPlanarThreeSATThree Graph.encOrthogonalDrawing (fun (a : DrawnPlanarThreeSATThreeInstance) => (encDrawnPlanarThreeSATThree a).length) fun (a : DrawnPlanarThreeSATThreeInstance) => (encDrawnPlanarThreeSATThree a).length

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Logic.PL.CNF ℕ} {x1 : γ → Graph.OrthogonalDrawing} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encCNF budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Graph.encOrthogonalDrawing budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { formula := x0 x, drawing := x1 x }) encIn encDrawnPlanarThreeSATThree budget

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_drawing_deg : Turing.MultiTapeTM.ComputableInDegree DrawnPlanarThreeSATThreeInstance.drawing encDrawnPlanarThreeSATThree Graph.encOrthogonalDrawing 1 1

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_formula_deg : Turing.MultiTapeTM.ComputableInDegree DrawnPlanarThreeSATThreeInstance.formula encDrawnPlanarThreeSATThree encCNF 1 1

@[simp]

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_apply (a : DrawnPlanarThreeSATThreeInstance) : encDrawnPlanarThreeSATThree a = encDrawnPlanarThreeSATThreeFields (a.formula, a.drawing)

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CNF ℕ} {x1 : γ → Graph.OrthogonalDrawing} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encCNF) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Graph.encOrthogonalDrawing) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { formula := x0 x, drawing := x1 x }) encIn encDrawnPlanarThreeSATThree

def Cslib.Complexity.encDrawnPlanarThreeSATThree : DrawnPlanarThreeSATThreeInstance ↪ List Bool

Binary encoding of a CNF formula and its supplied orthogonal incidence drawing.

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_drawing_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → DrawnPlanarThreeSATThreeInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDrawnPlanarThreeSATThree S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).drawing) encIn✝ Graph.encOrthogonalDrawing S✝

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_formula_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → DrawnPlanarThreeSATThreeInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDrawnPlanarThreeSATThree → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).formula) encIn✝ encCNF

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_drawing_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → DrawnPlanarThreeSATThreeInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDrawnPlanarThreeSATThree → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).drawing) encIn✝ Graph.encOrthogonalDrawing

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_formula_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → DrawnPlanarThreeSATThreeInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDrawnPlanarThreeSATThree S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).formula) encIn✝ encCNF S✝

@[reducible, inline]

abbrev Cslib.Complexity.encDrawnPlanarThreeSATThreeFields : Logic.PL.CNF ℕ × Graph.OrthogonalDrawing ↪ List Bool

The tuple of the fields of encDrawnPlanarThreeSATThree.

theorem Cslib.Complexity.encDrawnPlanarThreeSATThree_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : DrawnPlanarThreeSATThreeInstance) => (a.formula, a.drawing)) encDrawnPlanarThreeSATThree encDrawnPlanarThreeSATThreeFields 1 1

def Cslib.Complexity.PlanarThreeSATThree : Set (Logic.PL.CNF ℕ)

Satisfiable width-three, occurrence-three formulas whose actual incidence graph admits an integer orthogonal drawing with continuous endpoint-only contacts.

def Cslib.Complexity.DrawnPlanarThreeSATThree : Set DrawnPlanarThreeSATThreeInstance

The same problem with finite vertex positions and incidence routes supplied explicitly.

def Cslib.Complexity.toDrawnPlanarThreeSATThree (φ : Logic.PL.CNF ℕ) : DrawnPlanarThreeSATThreeInstance

A total compiler, including an explicit drawing. Invalid syntactic inputs produce the unsatisfiable empty clause with its isolated clause vertex.

def Cslib.Complexity.toPlanarThreeSATThree (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF ℕ

Forget the drawing emitted by the total compiler.

theorem Cslib.Complexity.computableInPolyTime_toDrawnPlanarThreeSATThree : Turing.MultiTapeTM.ComputableInPolyTime toDrawnPlanarThreeSATThree encCNF encDrawnPlanarThreeSATThree

The formula and explicit binary-coordinate drawing are computed in native polynomial time.

theorem Cslib.Complexity.computableInPolyTime_toPlanarThreeSATThree : Turing.MultiTapeTM.ComputableInPolyTime toPlanarThreeSATThree encCNF encCNF

Dropping the computed drawing gives a native polynomial-time formula compiler.

theorem Cslib.Complexity.width_toPlanarThreeSATThree (φ : Logic.PL.CNF ℕ) (c : Logic.PL.Clause ℕ) : c ∈ toPlanarThreeSATThree φ → List.length c ≤ 3

The total formula output has width at most three, including on rejected inputs.

theorem Cslib.Complexity.count_vars_toPlanarThreeSATThree (φ : Logic.PL.CNF ℕ) (v : ℕ) : List.count v (toPlanarThreeSATThree φ).vars ≤ 3

The actual total output has at most three literal positions for every variable.

theorem Cslib.Complexity.modelCount_toPlanarThreeSATThree (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) : (toPlanarThreeSATThree φ).modelCount = φ.modelCount

Valid width-three, occurrence-three inputs preserve their exact number of models.

theorem Cslib.Complexity.sharpThreeSATThree_toPlanarThreeSATThree (φ : Logic.PL.CNF ℕ) : SharpThreeSATThree (toPlanarThreeSATThree φ) = SharpThreeSATThree φ

The total planar compiler preserves syntax-guarded counts, including rejected inputs.

theorem Cslib.Complexity.satisfiable_toPlanarThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : (toPlanarThreeSATThree φ).Satisfiable ↔ φ ∈ ThreeSATThree

The total output is satisfiable exactly on the source 3SAT-3 language.

theorem Cslib.Complexity.isPlanarOrthogonalDrawing_toDrawnPlanarThreeSATThree (φ : Logic.PL.CNF ℕ) : (SAT.incidenceGraph (toPlanarThreeSATThree φ)).IsPlanarOrthogonalDrawing (toDrawnPlanarThreeSATThree φ).drawing

Every total output, including the rejection branch, has the claimed actual drawing.

theorem Cslib.Complexity.mem_DrawnPlanarThreeSATThree_toDrawnPlanarThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toDrawnPlanarThreeSATThree φ ∈ DrawnPlanarThreeSATThree ↔ φ ∈ ThreeSATThree

Correctness for the supplied-drawing target, on every source formula.

theorem Cslib.Complexity.mem_PlanarThreeSATThree_toPlanarThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toPlanarThreeSATThree φ ∈ PlanarThreeSATThree ↔ φ ∈ ThreeSATThree

Correctness when the target problem requires the drawing's existence.

theorem Cslib.Complexity.polyTimeReducible_ThreeSATThree_DrawnPlanarThreeSATThree : PolyTimeReducible encCNF encDrawnPlanarThreeSATThree ThreeSATThree DrawnPlanarThreeSATThree

Native polynomial-time reduction to a formula with its actual orthogonal drawing.

theorem Cslib.Complexity.polyTimeReducible_ThreeSATThree_PlanarThreeSATThree : PolyTimeReducible encCNF encCNF ThreeSATThree PlanarThreeSATThree

Native polynomial-time reduction to a formula admitting an orthogonal drawing.

theorem Cslib.Complexity.DrawnPlanarThreeSATThree_npHard : NPHard encDrawnPlanarThreeSATThree DrawnPlanarThreeSATThree

Orthogonal planar 3SAT-3 with the drawing supplied is NP-hard under binary encodings.

theorem Cslib.Complexity.PlanarThreeSATThree_npHard : NPHard encCNF PlanarThreeSATThree

Satisfiability of occurrence-three, width-three formulas admitting an integer orthogonal incidence drawing is NP-hard under the ordinary binary formula encoding.

theorem Cslib.Complexity.toDrawnPlanarThreeSATThree_fits (φ : Logic.PL.CNF ℕ) : Graph.drawingFits (toDrawnPlanarThreeSATThree φ).drawing (1920 * (φ.numVars + List.length φ + φ.vars.length + 1)) (1920 * (φ.numVars + List.length φ + φ.vars.length + 1))

Explicit linear grid sides for the total supplied-drawing compiler.

theorem Cslib.Complexity.toDrawnPlanarThreeSATThree_costs (φ : Logic.PL.CNF ℕ) : have out := toDrawnPlanarThreeSATThree φ; have s := φ.numVars + List.length φ + φ.vars.length + 1; List.length out.formula ≤ 5000 * s ^ 2 ∧ out.formula.vars.length ≤ 10000 * s ^ 2 ∧ out.drawing.2.length ≤ 10000 * s ^ 2 ∧ Graph.drawingSegmentCount out.drawing ≤ 12000 * s ^ 2 ∧ Graph.drawingWireLength out.drawing ≤ 400000 * s ^ 2

Explicit quadratic formula, incidence-route, segment and Manhattan wire bounds.

def Cslib.Complexity.toDrawnPlanarThreeSAT (φ : Logic.PL.CNF ℕ) : DrawnPlanarThreeSATThreeInstance

The original 3SAT input first passes through the linear occurrence splitter.

def Cslib.Complexity.toPlanarThreeSAT (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF ℕ

Formula projection of the total compiler from original 3SAT instances.

theorem Cslib.Complexity.computableInPolyTime_toDrawnPlanarThreeSAT : Turing.MultiTapeTM.ComputableInPolyTime toDrawnPlanarThreeSAT encCNF encDrawnPlanarThreeSATThree

The composed compiler retains native polynomial time under binary input labels.

theorem Cslib.Complexity.computableInPolyTime_toPlanarThreeSAT : Turing.MultiTapeTM.ComputableInPolyTime toPlanarThreeSAT encCNF encCNF

Formula output from original 3SAT is computed in native polynomial time.

theorem Cslib.Complexity.modelCount_toPlanarThreeSAT (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) : (toPlanarThreeSAT φ).modelCount = φ.modelCount

Occurrence splitting and planarization preserve all models of width-three inputs.

theorem Cslib.Complexity.satisfiable_toPlanarThreeSAT_iff (φ : Logic.PL.CNF ℕ) : (toPlanarThreeSAT φ).Satisfiable ↔ φ ∈ ThreeSAT

The total output is satisfiable exactly when the original input belongs to 3SAT.

theorem Cslib.Complexity.isPlanarOrthogonalDrawing_toDrawnPlanarThreeSAT (φ : Logic.PL.CNF ℕ) : (SAT.incidenceGraph (toPlanarThreeSAT φ)).IsPlanarOrthogonalDrawing (toDrawnPlanarThreeSAT φ).drawing

The composed output has its actual orthogonal drawing for every original CNF input.

theorem Cslib.Complexity.mem_DrawnPlanarThreeSATThree_toDrawnPlanarThreeSAT_iff (φ : Logic.PL.CNF ℕ) : toDrawnPlanarThreeSAT φ ∈ DrawnPlanarThreeSATThree ↔ φ ∈ ThreeSAT

The original 3SAT language reduces to the supplied-drawing target by the composed compiler.

theorem Cslib.Complexity.mem_PlanarThreeSATThree_toPlanarThreeSAT_iff (φ : Logic.PL.CNF ℕ) : toPlanarThreeSAT φ ∈ PlanarThreeSATThree ↔ φ ∈ ThreeSAT

The composed formula output belongs to the existential-drawing target exactly on 3SAT.

theorem Cslib.Complexity.toDrawnPlanarThreeSAT_fits (φ : Logic.PL.CNF ℕ) : Graph.drawingFits (toDrawnPlanarThreeSAT φ).drawing (13440 * (List.length φ + φ.vars.length + 1)) (13440 * (List.length φ + φ.vars.length + 1))

Linear grid sides are measured against the original formula's clause/literal size.

theorem Cslib.Complexity.toDrawnPlanarThreeSAT_costs (φ : Logic.PL.CNF ℕ) : have out := toDrawnPlanarThreeSAT φ; have s := List.length φ + φ.vars.length + 1; List.length out.formula ≤ 245000 * s ^ 2 ∧ out.formula.vars.length ≤ 490000 * s ^ 2 ∧ out.drawing.2.length ≤ 490000 * s ^ 2 ∧ Graph.drawingSegmentCount out.drawing ≤ 588000 * s ^ 2 ∧ Graph.drawingWireLength out.drawing ≤ 19600000 * s ^ 2

All output formula and drawing costs are quadratic in the original clause/literal size.