Positive exact-one SAT after parsimonious planarization

The compiler first uses the existing parsimonious planar 3SAT-3 construction and then the constant-factor positive exact-three replacement. The emitted integer orthogonal drawing has the actual output incidence graph. All route contacts concern full real supports.

Relative to a supplied planar drawing, the new replacement changes grid sides and all drawing costs by fixed constants. Relative to the original 3SAT instance, the full composition has linear grid sides and quadratic formula, vertex, route, segment and Manhattan wire costs. Models are counted only on occurring variables, and every ordinary source model has a unique extension.

Main definitions

• DrawnPlanarPositiveOneInExactThreeSATThreeInstance, encDrawnPlanarPositiveOneInExactThreeSATThree: supplied-drawing instances and binary encoding.
• PlanarPositiveOneInExactThreeSATThree: the existential orthogonal-drawing language.
• DrawnPlanarPositiveOneInExactThreeSATThree: the supplied-drawing language.
• SharpPlanarPositiveOneInExactThreeSATThree, SharpDrawnPlanarPositiveOneInExactThreeSATThree: the positive exact-one model counts guarded by the existence, respectively the validity, of a planar orthogonal incidence drawing.
• toPlanarPositiveOneInExactThreeSATThree, toDrawnPlanarPositiveOneInExactThreeSATThree: the actual formula and supplied-drawing compilers.

Main results

• oneModelCount_toPlanarPositiveOneInExactThreeSATThree: preservation of model counts.
• parsimoniousReducible_SharpThreeSAT_SharpPlanarPositiveOneInExactThreeSATThree, parsimoniousReducible_SharpThreeSAT_SharpDrawnPlanarPositiveOneInExactThreeSATThree: native parsimonious reductions from #3SAT to the planarity-guarded counts.
• PlanarPositiveOneInExactThreeSATThree_npHard, PlanarPositiveOneInThreeSATThree_npHard, DrawnPlanarPositiveOneInExactThreeSATThree_npHard: NP-hardness of the planar positive variants, including the version with the actual drawing supplied.
• computableInPolyTime_toDrawnPlanarPositiveOneInExactThreeSATThree: native polynomial-time computation of both the actual formula and its drawing.
• toDrawnPlanarPositiveOneInExactThreeSATThree_fits, toDrawnPlanarPositiveOneInExactThreeSATThree_costs: explicit linear grid sides and quadratic formula and drawing bounds.

References

The local clause gadgets are from [HuntMaratheRadhakrishnanStearns1998, Theorem 3.8]. The quantitative composition is original.

structure Cslib.Complexity.DrawnPlanarPositiveOneInExactThreeSATThreeInstance : Type

An instance of DrawnPlanarPositiveOneInExactThreeSATThree: a positive 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.DrawnPlanarPositiveOneInExactThreeSATThreeInstance.ext {x y : DrawnPlanarPositiveOneInExactThreeSATThreeInstance} (formula : x.formula = y.formula) (drawing : x.drawing = y.drawing) : x = y

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

def Cslib.Complexity.instDecidableEqDrawnPlanarPositiveOneInExactThreeSATThreeInstance.decEq (x✝ x✝¹ : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqDrawnPlanarPositiveOneInExactThreeSATThreeInstance : DecidableEq DrawnPlanarPositiveOneInExactThreeSATThreeInstance

def Cslib.Complexity.instReprDrawnPlanarPositiveOneInExactThreeSATThreeInstance.repr : DrawnPlanarPositiveOneInExactThreeSATThreeInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instReprDrawnPlanarPositiveOneInExactThreeSATThreeInstance : Repr DrawnPlanarPositiveOneInExactThreeSATThreeInstance

@[instance_reducible]

instance Cslib.Complexity.instInhabitedDrawnPlanarPositiveOneInExactThreeSATThreeInstance : Inhabited DrawnPlanarPositiveOneInExactThreeSATThreeInstance

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

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

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) => (a.formula, a.drawing)) encDrawnPlanarPositiveOneInExactThreeSATThree encDrawnPlanarPositiveOneInExactThreeSATThreeFields 1 1

def Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree : DrawnPlanarPositiveOneInExactThreeSATThreeInstance ↪ List Bool

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

@[reducible, inline]

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

The tuple of the fields of encDrawnPlanarPositiveOneInExactThreeSATThree.

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_formula_inO : Turing.MultiTapeTM.ComputableInO DrawnPlanarPositiveOneInExactThreeSATThreeInstance.formula encDrawnPlanarPositiveOneInExactThreeSATThree encCNF (fun (a : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) => (encDrawnPlanarPositiveOneInExactThreeSATThree a).length) fun (a : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) => (encDrawnPlanarPositiveOneInExactThreeSATThree a).length

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_formula_deg : Turing.MultiTapeTM.ComputableInDegree DrawnPlanarPositiveOneInExactThreeSATThreeInstance.formula encDrawnPlanarPositiveOneInExactThreeSATThree encCNF 1 1

@[simp]

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_apply (a : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) : encDrawnPlanarPositiveOneInExactThreeSATThree a = encDrawnPlanarPositiveOneInExactThreeSATThreeFields (a.formula, a.drawing)

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

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

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_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 encDrawnPlanarPositiveOneInExactThreeSATThree (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_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 encDrawnPlanarPositiveOneInExactThreeSATThree

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_drawing_deg : Turing.MultiTapeTM.ComputableInDegree DrawnPlanarPositiveOneInExactThreeSATThreeInstance.drawing encDrawnPlanarPositiveOneInExactThreeSATThree Graph.encOrthogonalDrawing 1 1

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_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 encDrawnPlanarPositiveOneInExactThreeSATThree budget

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

theorem Cslib.Complexity.encDrawnPlanarPositiveOneInExactThreeSATThree_drawing_inO : Turing.MultiTapeTM.ComputableInO DrawnPlanarPositiveOneInExactThreeSATThreeInstance.drawing encDrawnPlanarPositiveOneInExactThreeSATThree Graph.encOrthogonalDrawing (fun (a : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) => (encDrawnPlanarPositiveOneInExactThreeSATThree a).length) fun (a : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) => (encDrawnPlanarPositiveOneInExactThreeSATThree a).length

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

Positive exact-three, occurrence-three exact-one formulas with an integer orthogonal incidence drawing whose full real segments meet only at common incident endpoints.

def Cslib.Complexity.DrawnPlanarPositiveOneInExactThreeSATThree : Set DrawnPlanarPositiveOneInExactThreeSATThreeInstance

The same language with its finite integer incidence drawing supplied as input.

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

The width-at-most-three positive planar variant, without requiring ternary clauses.

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

Count positive exact-three, occurrence-three exact-one models of formulas that have a planar orthogonal incidence drawing; return zero otherwise.

noncomputable def Cslib.Complexity.SharpDrawnPlanarPositiveOneInExactThreeSATThree (x : DrawnPlanarPositiveOneInExactThreeSATThreeInstance) : ℕ

Count positive exact-three, occurrence-three exact-one models when the supplied drawing is a planar orthogonal incidence drawing of the formula; return zero otherwise.

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

Apply only the constant-factor positive compiler after the existing planarization.

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

Compute the actual positive incidence drawing by replacing each planar source clause box.

theorem Cslib.Complexity.computableInPolyTime_toPlanarPositiveOneInExactThreeSATThree : Turing.MultiTapeTM.ComputableInPolyTime toPlanarPositiveOneInExactThreeSATThree encCNF encCNF

The positive formula is produced in native polynomial time.

theorem Cslib.Complexity.exactClauses_toPlanarPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) (c : Logic.PL.Clause ℕ) : c ∈ toPlanarPositiveOneInExactThreeSATThree φ → List.length c = 3 ∧ (List.map Prod.fst c).Nodup

Every output clause has three distinct variables.

theorem Cslib.Complexity.positive_toPlanarPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) : OneSAT.positiveCheck (toPlanarPositiveOneInExactThreeSATThree φ) = true

There are no negative output literals.

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

The local replacements retain the planar compiler's three-occurrence restriction.

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

Counts on occurring variables agree with the original ordinary 3SAT instance.

theorem Cslib.Complexity.oneSatisfiable_toPlanarPositiveOneInExactThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : (toPlanarPositiveOneInExactThreeSATThree φ).OneSatisfiable ↔ φ ∈ ThreeSAT

Total correctness of the formula compiler, including ordinary syntax rejection.

theorem Cslib.Complexity.size_toPlanarPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) : have s := List.length φ + φ.vars.length + 1; List.length (toPlanarPositiveOneInExactThreeSATThree φ) ≤ 41405000 * s ^ 2 ∧ (toPlanarPositiveOneInExactThreeSATThree φ).vars.length ≤ 124215000 * s ^ 2

The new constant-factor replacements retain quadratic growth relative to original 3SAT.

theorem Cslib.Complexity.isPlanarOrthogonalDrawing_toDrawnPlanarPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) : (SAT.incidenceGraph (toPlanarPositiveOneInExactThreeSATThree φ)).IsPlanarOrthogonalDrawing (toDrawnPlanarPositiveOneInExactThreeSATThree φ).drawing

Every total output has its actual positive exact-one incidence drawing.

theorem Cslib.Complexity.mem_PositiveOneInExactThreeSATThree_toPlanarPositiveOneInExactThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toPlanarPositiveOneInExactThreeSATThree φ ∈ PositiveOneInExactThreeSATThree ↔ φ ∈ ThreeSAT

Membership in the strongest positive target agrees exactly with original 3SAT.

theorem Cslib.Complexity.mem_DrawnPlanarPositiveOneInExactThreeSATThree_toDrawn_iff (φ : Logic.PL.CNF ℕ) : toDrawnPlanarPositiveOneInExactThreeSATThree φ ∈ DrawnPlanarPositiveOneInExactThreeSATThree ↔ φ ∈ ThreeSAT

Correctness for the target with its actual drawing supplied.

theorem Cslib.Complexity.mem_PlanarPositiveOneInExactThreeSATThree_toPlanar_iff (φ : Logic.PL.CNF ℕ) : toPlanarPositiveOneInExactThreeSATThree φ ∈ PlanarPositiveOneInExactThreeSATThree ↔ φ ∈ ThreeSAT

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

theorem Cslib.Complexity.PlanarPositiveOneInExactThreeSATThree_npHard : NPHard encCNF PlanarPositiveOneInExactThreeSATThree

Positive exact-three, occurrence-three planar exact-one SAT is NP-hard.

theorem Cslib.Complexity.mem_PlanarPositiveOneInThreeSATThree_toPlanar_iff (φ : Logic.PL.CNF ℕ) : toPlanarPositiveOneInExactThreeSATThree φ ∈ PlanarPositiveOneInThreeSATThree ↔ φ ∈ ThreeSAT

Correctness of the same compiler for the positive width-three planar variant.

theorem Cslib.Complexity.PlanarPositiveOneInThreeSATThree_npHard : NPHard encCNF PlanarPositiveOneInThreeSATThree

Positive width-three, occurrence-three planar exact-one SAT is NP-hard.

theorem Cslib.Complexity.sharpPositiveOneInExactThreeSATThree_toPlanarPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) : SharpPositiveOneInExactThreeSATThree (toPlanarPositiveOneInExactThreeSATThree φ) = SharpThreeSAT φ

The positive planar compiler preserves syntax-guarded counts on every source input.

theorem Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpPlanarPositiveOneInExactThreeSATThree : ParsimoniousReducible encCNF encCNF SharpThreeSAT SharpPlanarPositiveOneInExactThreeSATThree

The planar formula compiler is a native parsimonious reduction to the planarity-guarded count: every output has a planar orthogonal incidence drawing, so the guard never discards a model.

theorem Cslib.Complexity.toDrawnPlanarPositiveOneInExactThreeSATThree_fits (φ : Logic.PL.CNF ℕ) : have s := List.length φ + φ.vars.length + 1; Graph.drawingFits (toDrawnPlanarPositiveOneInExactThreeSATThree φ).drawing (14516280000 * s) (14516280000 * s)

The full compiler retains linear grid sides relative to the original ordinary 3SAT input.

theorem Cslib.Complexity.toDrawnPlanarPositiveOneInExactThreeSATThree_costs (φ : Logic.PL.CNF ℕ) : have out := toDrawnPlanarPositiveOneInExactThreeSATThree φ; have s := List.length φ + φ.vars.length + 1; List.length out.formula ≤ 41405000 * s ^ 2 ∧ out.formula.vars.length ≤ 124215000 * s ^ 2 ∧ out.drawing.1.length ≤ 165620000 * s ^ 2 ∧ out.drawing.2.length ≤ 124215000 * s ^ 2 ∧ Graph.drawingSegmentCount out.drawing ≤ 141463000 * s ^ 2 ∧ Graph.drawingWireLength out.drawing ≤ 31029887000000 * s ^ 2

The actual output formula and drawing all have quadratic size relative to the original ordinary 3SAT input. Segment and wire costs refer to the emitted full routes.

theorem Cslib.Complexity.computableInPolyTime_toDrawnPlanarPositiveOneInExactThreeSATThree : Turing.MultiTapeTM.ComputableInPolyTime toDrawnPlanarPositiveOneInExactThreeSATThree encCNF encDrawnPlanarPositiveOneInExactThreeSATThree

Formula labels, vertex coordinates and route coordinates are all computed in native polynomial time under their ordinary binary encodings.

theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_DrawnPlanarPositiveOneInExactThreeSATThree : PolyTimeReducible encCNF encDrawnPlanarPositiveOneInExactThreeSATThree ThreeSAT DrawnPlanarPositiveOneInExactThreeSATThree

Ordinary 3SAT reduces natively to the positive target with its actual drawing supplied.

theorem Cslib.Complexity.DrawnPlanarPositiveOneInExactThreeSATThree_npHard : NPHard encDrawnPlanarPositiveOneInExactThreeSATThree DrawnPlanarPositiveOneInExactThreeSATThree

Supplied-drawing planar positive exact-three, occurrence-three exact-one SAT is NP-hard.

theorem Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpDrawnPlanarPositiveOneInExactThreeSATThree : ParsimoniousReducible encCNF encDrawnPlanarPositiveOneInExactThreeSATThree SharpThreeSAT SharpDrawnPlanarPositiveOneInExactThreeSATThree

Supplying the emitted drawing gives a native parsimonious reduction to the count guarded by the validity of the supplied drawing: the emitted drawing is always a planar orthogonal incidence drawing of the emitted formula.