[Rule] PLANAR 3SAT to MinimumGeometricConnectedDominatingSet

[isPANN]

Source: PLANAR 3SAT (Planar3Satisfiability)
Target: MINIMUM GEOMETRIC CONNECTED DOMINATING SET (MinimumGeometricConnectedDominatingSet)
Motivation: Imports NP-hardness from Planar 3-SAT into the geometric connected dominating set problem via the construction of Lichtenstein 1982 §6, Theorem 5. pred path Planar3Satisfiability MinimumGeometricConnectedDominatingSet currently returns no path, and MinimumGeometricConnectedDominatingSet has zero incoming reductions, so this rule is the canonical witness-preserving entry point into that node.
Reference: Lichtenstein, D. (1982). Planar formulae and their uses. SIAM J. Comput. 11(2), 329–343 — specifically §6 "Geometric connected dominating set", Theorem 5 (p. 336) together with Lemma 1 (p. 339). PDF at docs/research/raw/lichtenstein1982.pdf; BibTeX key lichtenstein1982 in docs/paper/references.bib.

GJ-style Source Entry

GEOMETRIC CONNECTED DOMINATING SET (GCD)
INSTANCE: A finite set P ⊂ Q² of rational points in the plane, a positive integer K.
QUESTION: Is there a subset S ⊆ P with |S| ≤ K such that (1) every point of P \ S lies within Euclidean distance 1 of some point of S (domination), and (2) the subgraph of the unit-disk graph on P induced by S is connected?

Note: in our model MinimumGeometricConnectedDominatingSet the distance threshold is the explicit field radius. For this reduction radius = 1, matching Lichtenstein.

Source-model preconditions and corner cases

The source model Planar3Satisfiability (file src/models/formula/planar_3_satisfiability.rs) validates only

• each clause has exactly 3 literals, and
• every literal references a variable index in [1, num_vars].

In particular it accepts (i) num_clauses == 0, (ii) variables that occur in 0 clauses, (iii) variables with arbitrarily many occurrences, (iv) repeated literals inside a clause (e.g. (x ∨ x ∨ y)), (v) tautological clauses (e.g. (x ∨ ¬x ∨ y)), and (vi) instances whose variable–clause incidence graph is NOT planar (per its docstring: "Planarity of the incidence graph is NOT validated at construction time").

reduce_to handles these as follows:

• num_clauses == 0 (vacuously satisfiable). Skip Phases A and B entirely. Emit the trivial target instance MinimumGeometricConnectedDominatingSet::new(vec![(0.0, 0.0)], 1.0) with bound K = 1. The single-point set is its own connected dominating set of size 1 ≤ K, so the target is feasible at K, matching the always-satisfiable source. (This avoids the points must be non-empty panic in the target constructor.)
• Variable with m_i == 0 (unused). Phase A introduces 0 copies of v_i; Phase B emits no variable structure for it. Solution extraction sets v_i := false by default (any value is consistent because v_i does not appear in any clause).
• Repeated literals inside a clause. The Phase A rule "introduce one copy per literal-occurrence" counts each occurrence, so a clause like (x ∨ x ∨ y) contributes 2 occurrences to m_x and 1 to m_y. Phase B's clause tripod still has three branches; two of them point to (consecutive) positive copies of x, which is harmless. No special-casing is required.
• Tautological clause (x ∨ ¬x ∨ y). Two branches of the clause tripod target opposite columns of the same variable structure (one to the top column, one to the bottom). The Phase B geometry already places those columns at horizontal distance 1, so the two branches can both reach their literal copies without clashing. The clause is trivially satisfied; the round-trip identity still holds.
• Non-planar incidence graph. Lichtenstein's construction is undefined on non-planar inputs (Phase B needs a planar embedding of B' to lay out the variable ladders, ground, and tripods without crossing). The reduce_to implementation panics with a descriptive message when no planar embedding of the incidence graph of B' exists, mirroring the source model's "planarity is the user's responsibility" stance. (A future enhancement can add a try_reduce_to returning Result<_, ReductionError> to make this checked.) The implementation uses any standard linear-time planarity algorithm — e.g. Boyer–Myrvold (2004) or Hopcroft–Tarjan (1974) — both of which also produce a combinatorial embedding when one exists.

Throughout the rest of this issue we assume num_clauses ≥ 1 and the incidence graph of the source is planar.

Reduction Algorithm

Let n = num_vars, m = num_clauses of the source Planar3Satisfiability instance. The construction has two phases: (A) bipolarize via Lichtenstein's Lemma 1, then (B) embed the bipolar instance per Figs. 12–15.

Phase A — Bipolarize (Lichtenstein Lemma 1, p. 339)

Lichtenstein's §6 geometric construction is not from arbitrary Planar 3-SAT. It requires the bipolar refinement of Lemma 1:

"Planar satisfiability is still NP-complete even when, at every variable node, all the arcs representing positive instances of the variable are incident to one side of the node and all the arcs representing negative instances are incident to the other side." — Lichtenstein 1982, Lemma 1, p. 339.

Lichtenstein's proof of Lemma 1 (p. 339): take the planar embedding of the incidence graph of B, and for every variable v_i with m_i ≥ 1 occurrences, replace v_i with a cycle of m_i fresh copies v_i^{(1)}, …, v_i^{(m_i)} arranged clockwise around the original variable node. Add, for each consecutive pair (v_i^{(j)}, v_i^{(j+1)}) along the cycle (with indices mod m_i), the implication clause (¬v_i^{(j)} ∨ v_i^{(j+1)}). Padded to width 3 these become the 3-CNF clauses

(¬v_i^{(j)} ∨ v_i^{(j+1)} ∨ v_i^{(j+1)}) for each j ∈ {1, …, m_i} (indices mod m_i).

Around a closed cycle these implications form v_i^{(1)} → v_i^{(2)} → … → v_i^{(m_i)} → v_i^{(1)}, which forces all copies equal. (Note: only one chain clause per consecutive pair is needed, because the cycle closes; this differs from acyclic-chain equality encodings that need a pair of implications per consecutive index.)

Each original clause c_j is then rewritten to use the specific copy v_i^{(k)} corresponding to its k-th occurrence of v_i in the clockwise traversal — positive occurrences attach to one side of the cycle, negative to the other, yielding the bipolar property.

Counting rule. "Occurrence" means literal-slot: a clause (v_i ∨ v_i ∨ ¬v_i) contributes 3 occurrences to m_i. Therefore Σ_i m_i = 3m exactly (each of the m clauses contributes 3 literal slots).

The resulting bipolar 3-CNF formula B' has

• n' = Σ_i m_i + |{i : m_i = 0}| · 0 = Σ_i m_i ≤ 3m copy variables,
• m' = m_b = m + Σ_i m_i = m + 3m = 4m clauses (m rewritten originals + one chain clause per cycle edge, summed over variables equals Σ_i m_i = 3m),
• the bipolar property required by §6,
• as a property of B' (not of B): each copy variable v_i^{(k)} occurs in exactly 3 clauses (two chain clauses (¬v_i^{(k-1)} ∨ v_i^{(k)} ∨ v_i^{(k)}) and (¬v_i^{(k)} ∨ v_i^{(k+1)} ∨ v_i^{(k+1)}), plus the one original clause it was inserted into). This is the per-variable degree-3 bound on the bipolar formula that Lichtenstein invokes when sizing the geometric construction.

This is a polynomial-time, satisfiability-preserving rewrite. From a satisfying assignment of B' we recover one for the original B by reading off any single copy of each variable (the cycle forces all copies equal). Variables of B with m_i = 0 get a default value (e.g. false) since B' contains no constraint on them.

Phase B — Geometric embedding (Figs. 12, 13, 15)

We embed B' in the plane at rational coordinates with denominator 80 (or any common refinement of 1/40, 1/10, 1/80). All distances quoted below are exact; the resulting point set lives in Q² so the construction is polynomial-bit.

B.1 Distance threshold. radius = 1. Verbatim from Lichtenstein p. 336: "an arc is drawn between all pairs of points no greater than distance 1." All subsequent geometric numbers (1, 1/10, 1/40, 1/80, 9/10) are calibrated to this threshold.

B.2 Variable structure for each copy variable u of B' (Fig. 12, p. 337). Let μ_u denote the number of clauses of B' in which u appears; by the bipolar property of B' and the degree-3 bound, μ_u ≤ 3. Place μ_u "round-pair rows" stacked vertically, with the rows separated by vertical distance 1. Each row k ∈ {1, …, μ_u} consists of four points:

• top-round R^+_{u,k} (a literal-true witness for u),
• bottom-round R^-_{u,k} (a literal-false witness for u) at horizontal distance 1 from R^+_{u,k},
• top-square S^+_{u,k} at distance 1/40 from R^+_{u,k}, vertically offset 1/10 from the round-pair row centre,
• bottom-square S^-_{u,k} symmetric to S^+_{u,k} on the bottom column.

The two columns of round nodes — all R^+_{u,k} and all R^-_{u,k} — form two parallel vertical ladders separated by horizontal distance 1. Consecutive round nodes in the same column are at Euclidean distance 1. The square forcers are placed so that:

• the only round nodes within distance 1 of S^+_{u,k} are R^+_{u,k} (at distance 1/40) and R^+_{u,k+1} (at distance ≤ √((1/40)² + (9/10)²) < 1); analogously for S^-_{u,k},
• no round of the opposite column is within distance 1 of a square (horizontal gap 1 + 1/40 > 1).

Thus each square forces at least one of its two adjacent same-column round nodes into any connected dominating set (Lichtenstein p. 336: "The square nodes force at least one of the two nodes adjacent to it into any cds"). The most economical choice picks every node in one column (either all R^+_{u,*} or all R^-_{u,*}), encoding u = T (top selected) or u = F (bottom selected). By the bipolar property of B', all positive-occurrence clauses of u attach to the top column and all negative-occurrence clauses attach to the bottom column.

B.3 Ground (Fig. 13, p. 337). A "ground" path threads through the planar embedding of B' following the route of the A_2 arcs (the arcs along which the planar embedding can be traversed as a Hamiltonian line through all variable structures). Concretely, between any two consecutive variable structures (and between a variable structure and the clause structures attached to it), insert a chain of round-square pairs:

• ground rounds spaced at Euclidean distance 1,
• each ground round paired with a square forcer at distance 1/10,
• consecutive squares far enough apart (≥ 1) that each square forces exactly its own pair.

The ground is necessary because "otherwise the forcers would be near the ground, and would not force at least of the two nearby nodes from the variable into the cds" (p. 337). After Lichtenstein's standard planar grid embedding of B' (p. 339: "the entire graph can be embedded in the plane in such a way that nodes are at rational points whose precision is bounded by a polynomial in the size of the number of points"), the ground has G = c_g · m_b ground rounds for an embedding-determined constant c_g ≤ 4.

B.4 Clause structure (Fig. 15, p. 338). Each bipolar clause c_j = (ℓ_1 ∨ ℓ_2 ∨ ℓ_3) is realised by a "tripod" with three branches meeting at a base triangle. Each branch is a column of round nodes spaced at distance 1, with squares (forcers) at distance 1/40 placed between consecutive rounds in the standard Fig. 15 pattern. The top round of branch t — drawn circled in Fig. 15 — is positioned within distance 1 of R^{σ}_{u_t, k_t}, where u_t = v_{i_t}^{(k_t)} is the bipolar copy corresponding to ℓ_t and σ = + if ℓ_t is a positive literal, σ = - otherwise. The base of the tripod attaches to the ground.

The uncircled (forced) round nodes in each branch are forced into any cds by their adjacent squares. The circled tops are not forced; selecting at least one circled top per clause is required for connectivity, and by Fig. 15's geometry, the only way to connect a circled top into the rest of the cds is via a chain that uses one of the variable column nodes adjacent to it — i.e. via a literal ℓ_t that the variable's truth assignment has marked live.

B.5 Total point set P. P is the union over all copy variables of their round + square nodes, the ground rounds + squares, and the clause-structure rounds + squares. The coordinates are computed in polynomial time from the planar embedding of B'.

Distance threshold

radius = 1. (Constant, matching d = 1 in Lichtenstein.)

Bound K (Lichtenstein p. 339)

Define the following exact construction-time counts on the bipolar instance B':

• NV = (1/3) of the total number of round nodes in all variable structures. Each row of each copy variable's structure contributes 4 rounds (top-round + bottom-round + their 2 partners). Summed over all copy variables, the total round count in variable structures is 4 · Σ_u μ_u = 4 · 3 m_b = 12 m_b, so NV = (1/3) · 12 m_b = 4 m_b. (Lichtenstein's (1/3) factor reflects that the optimum cds selects exactly one of three "classes" — top column, bottom column, or unforced slack — per variable structure, per p. 339.)
• NC = the number of forced (square-adjacent uncircled) round nodes in all clause structures. From Fig. 15 each clause tripod contributes exactly c_C forced rounds for a fixed Fig. 15 constant c_C (with c_C ≤ 12, footnote: Lichtenstein's Fig. 15 has three branches each with at most 4 forced rounds). Thus NC = c_C · m_b.
• NG = the number of forced round nodes on the ground. After embedding, NG = c_g · m_b for the embedding constant c_g ≤ 4 mentioned in B.3.
• m_b = number of clauses of the bipolar instance B' = 4 m.

Then

K = NV + NC + NG + m_b

This formula appears verbatim at Lichtenstein p. 339 (with his m being the bipolar clause count m_b here). The constants c_C, c_g are determined entirely by Phase B and do not depend on the source instance.

Solution extraction

Given a connected dominating set S ⊆ P of |S| ≤ K:

1. For each copy variable u of B', look at its round-node columns. By the bound K and the forcer argument, exactly one column is selected entirely; set u = T if the top column is selected, u = F if the bottom column is selected. (Per Lichtenstein's ⇒ direction on p. 339: "every variable has either the entire top row live, or the entire bottom row live".)
2. For each variable v_i of the original instance B:
   • if m_i ≥ 1, set v_i := u where u = v_i^{(1)} (all copies of v_i in B' are forced equal by the cycle clauses, so the choice of copy is irrelevant);
   • if m_i == 0, set v_i := false (default; no constraint).
3. Output the assignment to B. By Lichtenstein's proof, this assignment satisfies B.

For the num_clauses == 0 trivial case, return the all-false assignment of length n (or empty if n == 0); the source is vacuously satisfied.

Correctness

Lichtenstein 1982 §6 (pp. 336–339) gives the complete ⇐ / ⇒ proof:

• (⇐) Given a satisfying assignment of B', select all top-column rounds of true copy variables, all bottom-column rounds of false copy variables, all forced uncircled clause-structure rounds, all forced ground rounds, and one circled clause top per clause (the one matching a true literal). The total size is NV + NC + NG + m_b = K. Domination and connectivity are verified by Fig. 12–15 geometry; the bipolar property of B' is essential here so that a satisfied literal's circled top actually sits within distance 1 of a selected variable-column round.
• (⇒) Given a cds of size ≤ K, the forcer squares force at least NV + NC + NG round nodes; the remaining budget m_b is just enough to add one circled clause top per clause. Lichtenstein shows on p. 339 that "some variable switches from true to false at least once" would require a path of two live circled nodes inside a single clause, which the bound forbids, so each copy variable has a consistent column choice, and each clause must have at least one live circled top → at least one satisfied literal. Reading off literal-copy values and projecting via the cycle clauses recovers a satisfying assignment of B.

Size Overhead

Target field (getter)	Closed-form expression over source getters
num_points	100 * num_clauses + 10 * num_vars
radius	constant 1 (set in reduce_to, not size-dependent)

Justification of the num_points bound (all bounds depend only on the bipolar formula B' and on n, m of the source):

• Phase A produces a bipolar formula B' with n' = Σ_i m_i = 3m copy variables and m_b = 4m clauses. (Each of the m source clauses contributes 3 literal slots, so Σ_i m_i = 3m exactly, regardless of any per-variable occurrence count in the source.)
• Variable structures contribute 4 points per row × Σ_u μ_u = 3 m_b = 12m rows = 48 m points. (Note: this bound uses only Σ_u μ_u = 3 m_b, which is a property of B'; it does NOT invoke any per-variable degree-3 bound on the source B.)
• Ground contributes c_g · m_b ≤ 4 · 4m = 16m points (with the embedding constant c_g ≤ 4).
• Clause structures contribute (c_C rounds + c_C squares) · m_b ≤ 2 · 12 · 4m / 4 ≤ 36m points per the Fig. 15 layout.
• Plus a small additive term for the m_i = 0 and any n > Σ_i m_i / 3 slack: ≤ 10 n. (For instances where most variables are unused, this term keeps the overhead expression valid; it never dominates for typical instances.)

Total ≤ (48 + 16 + 36) m + 10 n = 100 m + 10 n points, parseable as 100 * num_clauses + 10 * num_vars in the #[reduction(overhead = …)] macro against the source getters num_clauses() and num_vars().

(The constant is generous; a tighter analysis can fit inside 60 * num_clauses + 4 * num_vars. We keep the slack so that emitting the trivial 1-point instance in the num_clauses == 0 corner case still respects the bound, since 1 ≤ 100 · 0 + 10 · num_vars holds whenever num_vars ≥ 1; if num_vars == 0 as well, the source is empty and we still emit 1 point, so the implementation guards this corner separately rather than relying on the asymptotic bound.)

Example

Example 1 — satisfiable

Source B: n = 3, m = 2, clauses

• C_1 = (x_1 ∨ x_2 ∨ x_3),
• C_2 = (x_1 ∨ ¬x_2 ∨ ¬x_3).

The incidence graph (3 variable nodes + 2 clause nodes + 6 edges) is planar. (T, T, T) satisfies C_1 (via any literal) and C_2 (via x_1); (T, F, F) and (T, T, F) also satisfy. So B is satisfiable.

Phase A (Lemma 1).

Occurrence counts: m_1 = 2 (one positive in C_1, one positive in C_2), m_2 = 2 (one positive in C_1, one negative in C_2), m_3 = 2 (one positive in C_1, one negative in C_2).

Introduce copies: x_1^{(1)}, x_1^{(2)}, x_2^{(1)}, x_2^{(2)}, x_3^{(1)}, x_3^{(2)}. For each variable add the cycle of m_i implication clauses (padded to width 3):

• For x_1 (cycle of length 2): (¬x_1^{(1)} ∨ x_1^{(2)} ∨ x_1^{(2)}) and (¬x_1^{(2)} ∨ x_1^{(1)} ∨ x_1^{(1)}). Together these force x_1^{(1)} = x_1^{(2)} (mutual implication around the 2-cycle).
• For x_2: (¬x_2^{(1)} ∨ x_2^{(2)} ∨ x_2^{(2)}) and (¬x_2^{(2)} ∨ x_2^{(1)} ∨ x_2^{(1)}). Force x_2^{(1)} = x_2^{(2)}.
• For x_3: (¬x_3^{(1)} ∨ x_3^{(2)} ∨ x_3^{(2)}) and (¬x_3^{(2)} ∨ x_3^{(1)} ∨ x_3^{(1)}). Force x_3^{(1)} = x_3^{(2)}.

Rewrite the original clauses using the appropriate copies (positive occurrences attach to one side of the cycle, negative to the other):

• C_1 = (x_1^{(1)} ∨ x_2^{(1)} ∨ x_3^{(1)}) (all three positive occurrences),
• C_2 = (x_1^{(2)} ∨ ¬x_2^{(2)} ∨ ¬x_3^{(2)}) (one positive x_1 occurrence + two negative).

The result B' has n' = 6, m_b = 6 + 2 = 8 clauses, and is bipolar: each copy variable's positive incidences all attach to one cycle side and negatives to the other.

Phase B: embed B'; the target GCD instance has roughly

• variable structures: 6 copy variables × ~4 points per row × ~2 rows ≈ 48 points (loose),
• clause tripods: 2 clauses × ~12 points ≈ 24 points,
• ground: ~16 points,

≈ 88 points, well within 100 · 2 + 10 · 3 = 230.

Round-trip: any cds of size K selects a column per copy variable; projecting via the cycle equalities recovers e.g. x_1 = T, x_2 = T, x_3 = T, which satisfies B.

Example 2 — unsatisfiable

Source B: n = 1, m = 4, clauses

• C_1 = (x_1 ∨ x_1 ∨ x_1),
• C_2 = (x_1 ∨ x_1 ∨ x_1),
• C_3 = (¬x_1 ∨ ¬x_1 ∨ ¬x_1),
• C_4 = (¬x_1 ∨ ¬x_1 ∨ ¬x_1).

x_1 = T satisfies C_1, C_2 but falsifies C_3, C_4; x_1 = F satisfies C_3, C_4 but falsifies C_1, C_2. So B is unsatisfiable.

Phase A applies the "count each occurrence" rule: m_1 = 3 + 3 + 3 + 3 = 12, so introduce 12 copies and a 12-cycle of implication clauses (each padded (¬x_1^{(j)} ∨ x_1^{(j+1)} ∨ x_1^{(j+1)}) for j = 1, …, 12 cyclically). All copies are forced equal. Each original clause is rewritten using three consecutive copies of the same polarity.

Phase B produces a GCD instance whose minimum connected dominating set has size strictly greater than K, since the bound K permits selecting only one column per copy variable, and any single-column choice corresponds to a single Boolean value for x_1, which leaves at least two unsatisfied clauses whose circled tops cannot all be connected through the cds within the remaining m_b-token budget. The closed-loop test confirms reduce(B).solve() > K, hence B is reported unsatisfiable.

Example 3 — non-trivial satisfiable instance for the closed-loop test

Source B: n = 4, m = 4, clauses

• C_1 = (x_1 ∨ x_2 ∨ x_3),
• C_2 = (¬x_1 ∨ x_2 ∨ x_4),
• C_3 = (x_1 ∨ ¬x_3 ∨ x_4),
• C_4 = (¬x_2 ∨ x_3 ∨ ¬x_4).

The incidence graph (4 + 4 = 8 nodes, 12 edges) is planar (this is the canonical example used by Planar3Satisfiability::canonical_model_example_specs). (T, T, T, F) satisfies all clauses, and several other assignments also satisfy, so the source has multiple satisfying witnesses — the round-trip test verifies that the recovered assignment is some satisfying one, not necessarily the canonical witness.

Implementation Notes

• No MinimumGeometricConnectedDominatingSet → ILP rule is required by this issue, in line with the project rule "one item per PR" (.claude/CLAUDE.md). Solving the target side via brute force is sufficient for the closed-loop test on small example instances (≤ 16 points). A separate [Rule] MinimumGeometricConnectedDominatingSet → ILP issue should be filed if witness-mode ILP solving is desired downstream.
• reduce_to performs Phase A internally; no separate BipolarPlanar3Satisfiability source model is introduced. Documenting Phase A clearly in the rule's reduce_to docstring (and citing Lichtenstein Lemma 1) keeps the source-model surface minimal.
• Coordinate emission: emit all points at exact f64 rationals with denominator a power of 2 · 5 = 10 so that distance comparisons against radius = 1 are exact. (Lichtenstein uses denominator 80; f64 represents 1/80, 1/40, 1/10, 9/10 exactly; alternatively, multiply all coordinates by 80 and use radius = 80 for integer coordinates.)
• Planarity testing: call Boyer–Myrvold (or any linear-time planarity tester that also yields a combinatorial embedding) on the incidence graph of B' before Phase B. Panic with a descriptive error if no planar embedding exists. (Planar3Satisfiability does not pre-validate planarity, but Phase A preserves planarity: replacing each variable node with a cycle of m_i nodes is a planar local replacement when the cycle is laid out around the original variable node, so B' is planar iff B is.)
• Corner-case dispatch: at the top of reduce_to, branch on source.num_clauses() == 0 and return the trivial 1-point instance with K = 1 before invoking Phases A and B.

Validation Method

• Closed-loop test test_planar3satisfiability_to_minimumgeometricconnecteddominatingset_closed_loop:
  1. Construct a small Planar3Satisfiability instance (Examples 1, 2, or 3 above).
  2. Apply the reduction to obtain a MinimumGeometricConnectedDominatingSet instance with radius = 1.
  3. Solve the target via BruteForce (size ≤ 16 points; otherwise pick a smaller worked example).
  4. Compare target_value ≤ K against source.evaluate(witness).
  5. For satisfiable sources, extract the assignment via the copy-projection of Solution extraction step 2 and verify source.is_satisfying(assignment).
• Round-trip on both Example 1 (satisfiable) and Example 2 (unsatisfiable) so the test exercises both branches of the ⇔ claim.
• Corner-case tests:
  • m = 0: Planar3Satisfiability::new(2, vec![]) → reduction returns the trivial 1-point target with K = 1; assert target.num_points() == 1, target.radius() == 1.0, solve(target) == Min(Some(1)).
  • m_i = 0 for some i: construct e.g. Planar3Satisfiability::new(3, vec![CNFClause::new(vec![1, 2, 1])]); assert reduce_to succeeds and the extracted assignment for x_3 is false (default).
• Mechanical sanity: assert target.radius() == 1.0 and target.num_points() ≤ 100 * num_clauses + 10 * num_vars.

References

• Lichtenstein, D. (1982). Planar formulae and their uses. SIAM J. Comput. 11(2), 329–343. §6 "Geometric connected dominating set" (pp. 336–339), Theorem 5, with the bipolar precondition in Lemma 1 (p. 339). PDF: docs/research/raw/lichtenstein1982.pdf. BibTeX: lichtenstein1982.
• Boyer, J. M., & Myrvold, W. J. (2004). On the cutting edge: simplified O(n) planarity by edge addition. J. Graph Algorithms Appl. 8(3), 241–273 — referenced for the linear-time planarity test + combinatorial embedding used in Phase B.
• Clark, B. N., Colbourn, C. J., & Johnson, D. S. (1990). Unit disk graphs. Discrete Math. 86, 165–177 — cited in docs/paper/reductions.typ for the MinimumGeometricConnectedDominatingSet problem definition; provides an alternative route through unit-disk MIS / dominating set.

[GiggleLiu]

fix-issue changelog:

• Expanded from 721-char stub to full issue body with geometric construction
• Added variable gadgets (true/false points), clause gadgets (center + bridge points), distance threshold B=2.5
• Added example: n=3 vars, m=1 clause with concrete point coordinates and bridge chains
• Noted overhead has no clean closed-form (depends on planar embedding distances and bridge point count)
• Noted MinimumGeometricConnectedDominatingSet -> ILP companion rule needed
• Flagged Codex verification needed: geometric separation hypotheses not fully proved
• Removed specialization note (Planar3Satisfiability model exists in codebase)