Remove unsound Planar3SAT->GCD rule (#377) + final-review cleanups

The Planar3Satisfiability -> MinimumGeometricConnectedDominatingSet
reduction emitted a geometrically disconnected target (point bands >=1.5
apart, copies/clauses spaced 3 apart, radius 1), so the unit-disk graph
admits no connected dominating set and every satisfiable source mapped to
an infeasible target. Confirmed unsound via /verify-reduction (6004
checks). Removed the rule, its test, mod.rs registration, example-spec
wiring, and the paper reduction-rule entry. The
MinimumGeometricConnectedDominatingSet model is retained as a sound orphan
node pending a correct reduction (+ a GCD->ILP rule for closed-loop tests);
#377 stays open.

Cleanups: dedupe PCSF feasibility into a shared forest_components() helper
(removing an unreachable branch); dedupe KColoring forward_witness between
rule and test; trim the oversized SCSS brute-force test; minor KISS nits
(eulerianpath y_idx wrapper, OLA is_valid_solution, CMO overhead).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: isPANN

docs/paper/reductions.typ

@@ -19717,33 +19717,6 @@ The following table shows concrete variable overhead for example instances, take
   _Solution extraction._ The Max-Cut partition vector is already a valid Graph Partitioning witness, so extraction is the identity map.
 ]
 
-#let p3sat_gcd = load-example("Planar3Satisfiability", "MinimumGeometricConnectedDominatingSet")
-#let p3sat_gcd_sol = p3sat_gcd.solutions.at(0)
-#reduction-rule("Planar3Satisfiability", "MinimumGeometricConnectedDominatingSet",
-  example: true,
-  example-caption: [trivial $m = 0$ corner case (vacuously satisfiable)],
-  extra: [
-    #pred-commands(
-      "pred create --example Planar3Satisfiability -o planar3sat.json",
-      "pred reduce planar3sat.json --to " + target-spec(p3sat_gcd) + " -o bundle.json",
-      "pred solve bundle.json",
-    )
-    Canonical fixture: the empty formula ($n = 0$, $m = 0$) is vacuously satisfiable, and the construction short-circuits to the single point $(0, 0)$ with radius $1$ and bound $K = 1$. The trivial connected dominating set is the singleton itself, witnessed by target config $(#p3sat_gcd_sol.target_config.map(str).join(", "))$ #sym.checkmark.
-
-    *Why the fixture is trivial.* The full Lichtenstein layout emits dozens of geometric points for even a one-clause input, which exceeds this codebase's $<= 16$ brute-force bound. We therefore use the $m = 0$ corner case as the canonical witness and rely on dedicated structural tests for non-trivial point emission. A full round-trip solve test will become feasible once a `MinimumGeometricConnectedDominatingSet -> ILP` rule is added.
-  ],
-)[
-  @lichtenstein1982 (Theorem 5, §6, combined with the bipolar refinement of Lemma 1.) The construction proceeds in two phases. _Phase A_ (Lemma 1) rewrites the Planar 3-SAT instance $phi$ into a _bipolar_ formula $phi'$ by replacing each variable $v_i$ with $m_i$ fresh copies arranged on a cycle and equating consecutive copies through chain clauses, so $phi'$ has $sum_i m_i = 3 m$ variables and $m_b = 4 m$ clauses with the property that every variable has all positive incidences on one side of the planar embedding and all negative incidences on the other. _Phase B_ (§6, Figures 12--15) embeds $phi'$ as a set of points in the plane: each copy variable becomes a "variable structure" (two parallel columns of rounds with square forcers at distance $1\/40$), a ground spine threads through the columns, and each bipolar clause becomes a tripod with three branches reaching the columns of its literal copies. With distance threshold $1$, the resulting Minimum Geometric Connected Dominating Set has solution $<= K = N_V + N_C + N_G + m_b$ if and only if $phi'$ (and hence $phi$) is satisfiable.
-][
-  _Construction (this implementation)._ We follow Lichtenstein's Phase A exactly --- count occurrences $m_i$, form $sum_i m_i = 3 m$ copy variables, build the bipolar formula $phi'$ with $m_b = m + sum_i m_i = 4 m$ clauses --- but we make one deliberate simplification in Phase B: instead of emitting Lichtenstein's full per-copy row stack of height $mu_u$, we _collapse the stack to a single row per copy_ ($mu_u = 1$). This emits $N_V = 4 m$ variable-structure rounds (top, bottom, top-partner, bottom-partner per copy) instead of $4 mu_u m$, while retaining the exact $K = N_V + N_C + N_G + m_b$ shape that Lichtenstein's analysis prescribes. The ground spine and clause tripods follow the original layout. The trivial corner case $m = 0$ short-circuits to a single point with $K = 1$.
-
-  _Why this simplification is faithful._ Lichtenstein's $mu_u$ is a scaling factor used to argue that a satisfying assignment forces _strictly fewer_ than $K + 1$ points into the dominating set; the same bipolar witness, when read off a single-row layout, still hits each variable-column anchor exactly once and dominates the ground spine and clause tripods. The simplification trades the original layout's exponential separation for a smaller point set; planarity, the bipolar property, and the bound shape are preserved. The rule's source-code docstring records this deviation explicitly.
-
-  _Correctness sketch._ ($arrow.r.double$) Given a satisfying assignment $bold(x)$ of $phi$, lift it to a consistent assignment of $phi'$ (each copy gets the value of its source variable). For each copy variable select the anchor round on the column matching the assigned polarity; for each clause tripod, the branch whose underlying literal is true points at a selected variable round, so picking the tripod root plus that branch dominates the tripod. The ground spine is connected by construction. Total selected rounds match $K$. ($arrow.l.double$) Any connected dominating set of size $<= K$ must, by Lichtenstein's gadget argument, select exactly one of the two column anchors per copy variable (the square forcers leave no other option), and the chain clauses of Phase A propagate this choice consistently across all copies of the same source variable. Reading off the column choice for each source variable's first occurrence gives a satisfying assignment of $phi$.
-
-  _Solution extraction._ For each source variable $v_i$, look up the recorded top-anchor index in the target point list. If the top-column anchor is selected, set $v_i$ to the polarity of its first occurrence (positive occurrence $arrow.r$ true); if the bottom anchor is selected, flip the polarity; if neither (variable does not occur), default to false. This is implemented in `ReductionPlanar3SATToGCD::extract_solution` and uses the auxiliary `first_occurrence_polarity` and `top_anchor_index` tables built during the reduction.
-]
-
 #let pcsf_st = load-example("PrizeCollectingSteinerForest", "SteinerTree")
 #let pcsf_st_sol = pcsf_st.solutions.at(0)
 #let pcsf_st_n = pcsf_st.source.instance.graph.num_vertices

src/models/graph/optimal_linear_arrangement.rs

@@ -93,7 +93,7 @@ impl<G: Graph> OptimalLinearArrangement<G> {
 
     /// Check if a configuration is a valid permutation.
     pub fn is_valid_solution(&self, config: &[usize]) -> bool {
-        self.total_edge_length(config).is_some()
+        self.is_valid_permutation(config)
     }
 
     /// Check if a configuration forms a valid permutation of {0, ..., n-1}.

src/models/graph/prize_collecting_steiner_forest.rs

@@ -186,7 +186,7 @@ impl<G: Graph, W: WeightElement> PrizeCollectingSteinerForest<G, W> {
     /// Whether this configuration is a feasible forest (selected edges only
     /// touch selected vertices and induce an acyclic subgraph).
     pub fn is_valid_solution(&self, config: &[usize]) -> bool {
-        is_feasible_forest(&self.graph, config)
+        forest_components(&self.graph, config).is_some()
     }
 }
 
@@ -208,81 +208,10 @@ where
 
     fn evaluate(&self, config: &[usize]) -> Min<W::Sum> {
         let n = self.graph.num_vertices();
-        let m = self.graph.num_edges();
-        if config.len() != n + m {
-            return Min(None);
-        }
-        let edges = self.graph.edges();
-
-        // Feasibility: selected edges must be incident only to selected
-        // vertices, and the resulting subgraph must be acyclic.
-        let mut adj: Vec<Vec<(usize, usize)>> = vec![Vec::new(); n];
-        let mut selected_edge_count = 0usize;
-        for (i, &(u, v)) in edges.iter().enumerate() {
-            let y_e = config[n + i];
-            if y_e == 0 {
-                continue;
-            }
-            if y_e != 1 {
-                return Min(None);
-            }
-            let x_u = config[u];
-            let x_v = config[v];
-            if x_u != 1 || x_v != 1 {
-                return Min(None);
-            }
-            adj[u].push((v, i));
-            adj[v].push((u, i));
-            selected_edge_count += 1;
-        }
-
-        // Acyclicity via BFS on the selected subgraph restricted to selected
-        // vertices. We also count tree components: a selected vertex with no
-        // incident selected edges is one singleton tree.
-        let mut visited = vec![false; n];
-        let mut kappa: usize = 0;
-        let mut total_tree_edges: usize = 0;
-        for start in 0..n {
-            if config[start] != 1 || visited[start] {
-                continue;
-            }
-            // Discovered a fresh component containing `start`.
-            kappa += 1;
-            visited[start] = true;
-            let mut comp_edges: usize = 0;
-            // Parent edge index per vertex inside this BFS, used to detect
-            // back-edges (cycles).
-            let mut parent_edge: Vec<Option<usize>> = vec![None; n];
-            let mut queue: VecDeque<usize> = VecDeque::new();
-            queue.push_back(start);
-            while let Some(u) = queue.pop_front() {
-                for &(w, edge_idx) in &adj[u] {
-                    if parent_edge[u] == Some(edge_idx) {
-                        // Skip the edge we came in on.
-                        continue;
-                    }
-                    if visited[w] {
-                        // Back-edge inside this component => cycle.
-                        return Min(None);
-                    }
-                    visited[w] = true;
-                    parent_edge[w] = Some(edge_idx);
-                    comp_edges += 1;
-                    queue.push_back(w);
-                }
-            }
-            // Each discovered tree edge is counted once via BFS discovery. If
-            // we did not pick up an extra back-edge (which would have
-            // triggered the cycle return above), the selected-edge subgraph
-            // restricted to this component is a tree.
-            total_tree_edges += comp_edges;
-        }
-        // Sanity: every selected edge must have been visited as a tree edge.
-        // If it was not, both endpoints would have been in distinct
-        // components, which is impossible by construction.
-        if total_tree_edges != selected_edge_count {
-            return Min(None);
-        }
+        let kappa = match forest_components(&self.graph, config) {
+            Some(kappa) => kappa,
+            None => return Min(None),
+        };
 
         // Objective: beta * sum_{v notin V_F} p(v)
         //          + sum_{e in E_F} c(e)
@@ -322,13 +251,15 @@ where
     }
 }
 
-/// Decide feasibility of a `(V_F, E_F)` configuration: selected edges only
-/// touch selected vertices and induce an acyclic subgraph.
-fn is_feasible_forest<G: Graph>(graph: &G, config: &[usize]) -> bool {
+/// Validate a `(V_F, E_F)` configuration and, if feasible, return the number of
+/// tree components `kappa(F)` among the selected vertices. Feasible means every
+/// selected edge is incident only to selected vertices and the selected
+/// subgraph is acyclic. Returns `None` for any infeasible configuration.
+fn forest_components<G: Graph>(graph: &G, config: &[usize]) -> Option<usize> {
     let n = graph.num_vertices();
     let m = graph.num_edges();
     if config.len() != n + m {
-        return false;
+        return None;
     }
     let edges = graph.edges();
     let mut adj: Vec<Vec<(usize, usize)>> = vec![Vec::new(); n];
@@ -338,19 +269,21 @@ fn is_feasible_forest<G: Graph>(graph: &G, config: &[usize]) -> bool {
             continue;
         }
         if y_e != 1 {
-            return false;
+            return None;
         }
         if config[u] != 1 || config[v] != 1 {
-            return false;
+            return None;
         }
         adj[u].push((v, i));
         adj[v].push((u, i));
     }
     let mut visited = vec![false; n];
+    let mut kappa: usize = 0;
     for start in 0..n {
         if config[start] != 1 || visited[start] {
             continue;
         }
+        kappa += 1;
         visited[start] = true;
         let mut parent_edge: Vec<Option<usize>> = vec![None; n];
         let mut queue: VecDeque<usize> = VecDeque::new();
@@ -361,15 +294,15 @@ fn is_feasible_forest<G: Graph>(graph: &G, config: &[usize]) -> bool {
                     continue;
                 }
                 if visited[w] {
-                    return false; // back-edge inside the component => cycle
+                    return None; // back-edge inside the component => cycle
                 }
                 visited[w] = true;
                 parent_edge[w] = Some(edge_idx);
                 queue.push_back(w);
             }
         }
     }
-    true
+    Some(kappa)
 }
 
 crate::declare_variants! {

src/rules/eulerianpath_ilp.rs

@@ -51,10 +51,6 @@ pub struct ReductionEulerianPathToILP {
 }
 
 impl ReductionEulerianPathToILP {
-    fn y_idx(&self, k: usize) -> usize {
-        k
-    }
-
     fn s_idx(&self, a: usize) -> usize {
         self.pairs.len() + a
     }
@@ -111,7 +107,7 @@ impl ReductionResult for ReductionEulerianPathToILP {
                 .iter()
                 .enumerate()
                 .find(|&(k, &(a, _))| {
-                    a == current && target_solution.get(self.y_idx(k)).copied().unwrap_or(0) == 1
+                    a == current && target_solution.get(k).copied().unwrap_or(0) == 1
                 })
                 .map(|(_, &(_, b))| b);
 

src/rules/kcoloring_bicliquecover.rs

@@ -223,8 +223,11 @@ impl ReduceTo<BicliqueCover> for KColoring<KN, SimpleGraph> {
 /// `coloring[v]` must be in `0..q`. The order of color bicliques is the
 /// order of first appearance of each color along `0..n`, so unused colors
 /// at the tail produce empty bicliques.
-#[cfg(feature = "example-db")]
-fn forward_witness(source: &KColoring<KN, SimpleGraph>, coloring: &[usize]) -> Vec<usize> {
+#[cfg(any(test, feature = "example-db"))]
+pub(crate) fn forward_witness(
+    source: &KColoring<KN, SimpleGraph>,
+    coloring: &[usize],
+) -> Vec<usize> {
     let n = source.graph().num_vertices();
     let q = source.num_colors();
     let k = n + q;

src/rules/maximumcontactmapoverlap_ilp.rs

@@ -63,7 +63,7 @@ impl ReductionResult for ReductionCMOToILP {
 #[reduction(
     overhead = {
         num_vars = "num_vertices_1 * num_vertices_2 + num_contacts_1 * num_contacts_2",
-        num_constraints = "num_vertices_1 + num_vertices_2 + num_vertices_1 * num_vertices_1 * num_vertices_2 * num_vertices_2 + 2 * num_contacts_1 * num_contacts_2",
+        num_constraints = "num_vertices_1 + num_vertices_2 + num_vertices_1 * (num_vertices_1 - 1) / 2 * num_vertices_2 * (num_vertices_2 + 1) / 2 + 2 * num_contacts_1 * num_contacts_2",
     }
 )]
 impl ReduceTo<ILP<bool>> for MaximumContactMapOverlap {

src/rules/mod.rs

@@ -124,7 +124,6 @@ pub(crate) mod partition_subsetsum;
 pub(crate) mod partition_sumofsquarespartition;
 pub(crate) mod partitionintocliques_minimumcoveringbycliques;
 pub(crate) mod partitionintopathsoflength2_boundedcomponentspanningforest;
-pub(crate) mod planar3satisfiability_minimumgeometricconnecteddominatingset;
 pub(crate) mod prizecollectingsteinerforest_steinertree;
 pub(crate) mod rootedtreearrangement_rootedtreestorageassignment;
 pub(crate) mod sat_circuitsat;
@@ -489,10 +488,6 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(minimumdiscreteplanarinversekinematics_qubo::canonical_rule_example_specs());
     specs.extend(minimummultiwaycut_qubo::canonical_rule_example_specs());
     specs.extend(paintshop_qubo::canonical_rule_example_specs());
-    specs.extend(
-        planar3satisfiability_minimumgeometricconnecteddominatingset::canonical_rule_example_specs(
-        ),
-    );
     specs.extend(prizecollectingsteinerforest_steinertree::canonical_rule_example_specs());
     specs.extend(partition_cosineproductintegration::canonical_rule_example_specs());
     specs.extend(partition_integralflowwithmultipliers::canonical_rule_example_specs());