[Rule] VERTEX COVER to HAMILTONIAN CIRCUIT

[isPANN]

Source: VERTEX COVER (DecisionDecisionMinimumVertexCover)
Target: HAMILTONIAN CIRCUIT (HamiltonianCircuit)
Motivation: Establishes NP-completeness of HAMILTONIAN CIRCUIT by a gadget-based polynomial-time reduction from VERTEX COVER, enabling downstream reductions to HAMILTONIAN PATH, TSP, and other tour-finding problems. The source is Decision<DecisionMinimumVertexCover> which provides the bound parameter K needed by the construction.
Reference: Garey & Johnson, Computers and Intractability, Theorem 3.4, p.56-60

Reduction Algorithm

Theorem 3.4 HAMILTONIAN CIRCUIT is NP-complete
Proof: It is easy to see that HC E NP, because a nondeterministic algorithm need only guess an ordering of the vertices and check in polynomial time that all the required edges belong to the edge set of the given graph.

We transform VERTEX COVER to HC. Let an arbitrary instance of VC be given by the graph G = (V,E) and the positive integer K <= |V|. We must construct a graph G' = (V',E') such that G' has a Hamiltonian circuit if and only if G has a vertex cover of size K or less.

Once more our construction can be viewed in terms of components connected together by communication links. First, the graph G' has K "selector" vertices a1,a2, . . . , aK, which will be used to select K vertices from the vertex set V for G. Second, for each edge in E, G' contains a "cover-testing" component that will be used to ensure that at least one endpoint of that edge is among the selected K vertices. The component for e = {u,v} E E is illustrated in Figure 3.4. It has 12 vertices,

V'_e = {(u,e,i),(v,e,i): 1 <= i <= 6}

and 14 edges,

E'_e = {{(u,e,i),(u,e,i+1)},{(v,e,i),(v,e,i+1)}: 1 <= i <= 5}
U {{(u,e,3),(v,e,1)},{(v,e,3),(u,e,1)}}
U {{(u,e,6),(v,e,4)},{(v,e,6),(u,e,4)}}

In the completed construction, the only vertices from this cover-testing component that will be involved in any additional edges are (u,e,1), (v,e,1), (u,e,6), and (v,e,6). This will imply, as the reader may readily verify, that any Hamiltonian circuit of G' will have to meet the edges in E'_e in exactly one of the three configurations shown in Figure 3.5. Thus, for example, if the circuit "enters" this component at (u,e,1), it will have to "exit" at (u,e,6) and visit either all 12 vertices in the component or just the 6 vertices (u,e,i), 1 <= i <= 6.

Additional edges in our overall construction will serve to join pairs of cover-testing components or to join a cover-testing component to a selector vertex. For each vertex v E V, let the edges incident on v be ordered (arbitrarily) as e_{v[1]}, e_{v[2]}, . . . , e_{v[deg(v)]}, where deg(v) denotes the degree of v in G, that is, the number of edges incident on v. All the cover-testing components corresponding to these edges (having v as endpoint) are joined together by the following connecting edges:

E'v = {{(v,e{v[i]},6),(v,e_{v[i+1]},1)}: 1 <= i < deg(v)}

As shown in Figure 3.6, this creates a single path in G' that includes exactly those vertices (x,y,z) having x = v.

The final connecting edges in G' join the first and last vertices from each of these paths to every one of the selector vertices a1,a2, . . . , aK. These edges are specified as follows:

E'' = {{a_i,(v,e_{v[1]},1)},{a_i,(v,e_{v[deg(v)]},6)}: 1 <= i <= K, v E V}

The completed graph G' = (V',E') has

V' = {a_i: 1 <= i <= K} U (U_{e E E} V'_e)

and

E' = (U_{e E E} E'e) U (U{v E V} E'_v) U E''

It is not hard to see that G' can be constructed from G and K in polynomial time.

We claim that G' has a Hamiltonian circuit if and only if G has a vertex cover of size K or less. Suppose <v1,v2, . . . , vn>, where n = |V'|, is a Hamiltonian circuit for G'. Consider any portion of this circuit that begins at a vertex in the set {a1,a2, . . . , aK}, ends at a vertex in {a1,a2, . . . , aK}, and that encounters no such vertex internally. Because of the previously mentioned restrictions on the way in which a Hamiltonian circuit can pass through a cover-testing component, this portion of the circuit must pass through a set of cover-testing components corresponding to exactly those edges from E that are incident on some one particular vertex v E V. Each of the cover-testing components is traversed in one of the modes (a), (b), or (c) of Figure 3.5, and no vertex from any other cover-testing component is encountered. Thus the K vertices from {a1,a2, . . . , aK} divide the Hamiltonian circuit into K paths, each path corresponding to a distinct vertex v E V. Since the Hamiltonian circuit must include all vertices from every one of the cover-testing components, and since vertices from the cover-testing component for edge e E E can be traversed only by a path corresponding to an endpoint of e, every edge in E must have at least one endpoint among those K selected vertices. Therefore, this set of K vertices forms the desired vertex cover for G.

Conversely, suppose V* ⊆ V is a vertex cover for G with |V*| <= K. We can assume that |V*| = K since additional vertices from V can always be added and we will still have a vertex cover. Let the elements of V* be labeled as v1,v2, . . . , vK. The following edges are chosen to be "in" the Hamiltonian circuit for G'. From the cover-testing component representing each edge e = {u,v} E E, choose the edges specified in Figure 3.5(a), (b), or (c) depending on whether {u,v} ∩ V* equals, respectively, {u}, {u,v}, or {v}. One of these three possibilities must hold since V* is a vertex cover for G. Next, choose all the edges in E'_{v_i} for 1 <= i <= K. Finally, choose the edges

{a_i,(v_i,e_{v_i[1]},1)}, 1 <= i <= K

{a_{i+1},(v_i,e_{v_i[deg(v_i)]},6)}, 1 <= i < K

and

{a_1,(v_K,e_{v_K[deg(v_K)]},6)}

We leave to the reader the task of verifying that this set of edges actually corresponds to a Hamiltonian circuit for G'.

Summary:
Given a DecisionMinimumVertexCover instance (G, K) where G = (V, E) with n = |V| vertices, m = |E| edges, and K the cover size bound, construct a HamiltonianCircuit instance G' = (V', E') as follows:

1. Selector vertices: Add K vertices a_1, ..., a_K representing "slots" for the K cover vertices.

2. Cover-testing gadgets: For each edge e = {u, v} ∈ E, add 12 vertices — (u,e,1)...(u,e,6) and (v,e,1)...(v,e,6) — connected by 14 internal edges forming two 6-chains with two cross-links at positions 3→1 and 6→4 (in both directions). Each gadget has exactly three valid traversal modes: pass through all 12 vertices (both u and v "selected"), pass through only the u-side (only u selected), or pass through only the v-side (only v selected).

3. Vertex path edges: For each vertex v ∈ V, chain together its incident gadgets in arbitrary order using edges {(v, e_{v[i]}, 6), (v, e_{v[i+1]}, 1)} for consecutive incident edges. This forms a single path through all gadget-vertices labelled with v.

4. Selector connection edges: For each selector a_i and each vertex v ∈ V, add edges {a_i, (v, e_{v[1]}, 1)} and {a_i, (v, e_{v[deg(v)]}, 6)} connecting the selector to both endpoints of v's vertex path. Total: 2kn edges.

5. Solution extraction: A Hamiltonian circuit in G' is divided by the K selector vertices into K sub-paths. Each sub-path traverses exactly the gadgets corresponding to edges incident on some vertex v; the K such vertices form the vertex cover. Conversely, given a vertex cover {v_1, ..., v_K}, assign a_i to v_i, traverse each gadget in mode (a/b/c) depending on cover membership, and connect using the selector edges to form the circuit.

Vertex count: 12m (gadgets) + k (selectors) = 12m + k
Edge count: 14m (gadget internal) + (2m − n) (vertex path chains) + 2kn (selector connections) = 16m − n + 2kn

Size Overhead

Symbols:

• n = num_vertices of source DecisionMinimumVertexCover instance (|V|)
• m = num_edges of source DecisionMinimumVertexCover instance (|E|)
• k = cover size bound parameter (K)

Target metric (code name)	Polynomial (using symbols above)
num_vertices	12 * num_edges + k
num_edges	16 * num_edges - num_vertices + 2 * k * num_vertices

Derivation:

• Vertices: each of the m edge gadgets has 12 vertices, plus k selector vertices → 12m + k
• Edges:
  • 14 per gadget (5+5 chain edges + 4 cross-links) × m gadgets = 14m
  • Vertex path edges: for each vertex v, deg(v)−1 chain edges; total = ∑_v (deg(v)−1) = 2m − n
  • Selector connections: k selectors × n vertices × 2 endpoints = 2kn
  • Total = 14m + (2m − n) + 2kn = 16m − n + 2kn

Validation Method

• Closed-loop test: reduce a small DecisionMinimumVertexCover instance (G, K) to HamiltonianCircuit G', solve G' with BruteForce, then verify that if a Hamiltonian circuit exists, the corresponding K vertices form a valid vertex cover of G, and vice versa.
• Test with a graph that has a known minimum vertex cover (e.g., a path graph P_n has minimum VC of size n−1) and verify the HC instance has a Hamiltonian circuit iff the cover size K ≥ minimum.
• Test with K < minimum VC size to confirm no Hamiltonian circuit is found.
• Verify vertex and edge counts in G' match the formulas: |V'| = 12m + k, |E'| = 16m − n + 2kn.

Example

Source instance (DecisionMinimumVertexCover):
Graph G with 4 vertices {0, 1, 2, 3} and 6 edges (K_4):

• Edges (indexed): e_0={0,1}, e_1={0,2}, e_2={0,3}, e_3={1,2}, e_4={1,3}, e_5={2,3}
• n = 4, m = 6, K = 3
• Minimum vertex cover of size 3: {0, 1, 2} covers all edges

Constructed target instance (HamiltonianCircuit):

• Vertex count: 12 × 6 + 3 = 75 vertices
• Edge count: 16 × 6 − 4 + 2 × 3 × 4 = 96 − 4 + 24 = 116 edges

Gadget for e_0 = {0,1}: vertices (0,e_0,1)...(0,e_0,6) and (1,e_0,1)...(1,e_0,6) with internal edges:

• Chains: {(0,e_0,i),(0,e_0,i+1)} and {(1,e_0,i),(1,e_0,i+1)} for i=1..5 (10 edges)
• Cross-links: {(0,e_0,3),(1,e_0,1)}, {(1,e_0,3),(0,e_0,1)}, {(0,e_0,6),(1,e_0,4)}, {(1,e_0,6),(0,e_0,4)} (4 edges)

Vertex path for vertex 0 (incident edges: e_0, e_1, e_2):

• Chain edges: {(0,e_0,6),(0,e_1,1)}, {(0,e_1,6),(0,e_2,1)} (2 edges)

Selector connections for a_1 and vertex 0:

• {a_1, (0,e_0,1)}, {a_1, (0,e_2,6)} (entry/exit of vertex 0's path)

Solution mapping (vertex cover {0,1,2} with K=3, assigning a_1↔0, a_2↔1, a_3↔2):

• For e_0={0,1}: both in cover → mode (b): traverse all 12 vertices of gadget e_0
• For e_3={1,2}: both in cover → mode (b): traverse all 12 vertices of gadget e_3
• For e_1={0,2}: both in cover → mode (b): traverse all 12 vertices of gadget e_1
• For e_2={0,3}: only 0 in cover → mode (a): traverse only the 0-side (6 vertices)
• For e_4={1,3}: only 1 in cover → mode (a): traverse only the 1-side (6 vertices)
• For e_5={2,3}: only 2 in cover → mode (a): traverse only the 2-side (6 vertices)
• Circuit: a_1 → [gadgets for vertex 0] → a_2 → [gadgets for vertex 1] → a_3 → [gadgets for vertex 2] → a_1
• All 75 vertices are visited exactly once ✓

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	⚠️ Warn	Target problem HamiltonianCircuit does not exist in the codebase yet
Non-trivial	✅ Pass	Genuine gadget construction with 12-vertex cover-testing components
Correctness	✅ Pass	Garey & Johnson Theorem 3.4 (pp. 56–60) is a well-known, verified reduction
Well-written	❌ Fail	Overhead uses undefined k; target problem has no model; several notation issues

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

The target problem HamiltonianCircuit does not exist in the reduction graph. There is no existing path from MinimumVertexCover to any Hamiltonian-type problem. This would be a novel reduction that connects vertex cover problems to tour-finding problems (HC, TSP, etc.).

However, the target model must be implemented first. A plan file already exists at docs/plans/2026-02-13-hamiltonian-cycle-model.md (named HamiltonianCycle there, not HamiltonianCircuit — naming should be reconciled). Until the target model exists, this rule cannot be implemented.

Verdict: Pass (novel reduction), but blocked on target model.

---

Non-trivial

The reduction constructs non-trivial structure:

• 12-vertex cover-testing gadgets for each edge, with internal cross-links that enforce exactly three traversal modes
• Vertex path chains linking gadgets incident on each vertex
• Selector vertices connected to all vertex paths
• Solution extraction requires interpreting Hamiltonian circuit sub-paths as vertex cover membership

This is a genuine gadget-based construction, not a variable substitution or type coercion. Pass.

---

Correctness

Reference verification:

• Garey & Johnson, Computers and Intractability (1979), Theorem 3.4, pp. 56–60 — this is the canonical NP-completeness proof for Hamiltonian Circuit via reduction from Vertex Cover. The book is already in the project bibliography as garey1979.
• The construction described in the issue (selector vertices, 12-vertex cover-testing gadgets with 14 internal edges, vertex path chains, selector connection edges) faithfully reproduces the textbook proof.
• The three traversal modes (a), (b), (c) matching Figure 3.5 of the book are correctly described.
• The correctness argument (both directions of the if-and-only-if) is included verbatim from the text.

Note: Karp's original reduction tree goes VC → Feedback Vertex Set → Directed HC → Undirected HC. Garey & Johnson provide this more direct construction that bypasses the intermediate problems. Both are valid; the direct construction is arguably more useful for this project since it avoids needing Feedback Vertex Set and Directed HC as intermediate models.

Verdict: Pass.

---

Well-written

Several issues need to be addressed:

4a: Information Completeness

All template sections are present and substantive. ✅

4b: Algorithm Completeness

The reduction algorithm is detailed and step-by-step, including the full textbook proof text plus a clear summary. The construction is implementable. ✅

4c: Symbol and Notation Consistency — ❌ FAIL

1. k is not a valid source metric. The overhead table uses k (the cover size bound), but MinimumVertexCover in this codebase is an optimization problem — it finds the minimum vertex cover by weight. There is no k parameter. The source problem's size_fields are only ["num_edges", "num_vertices"]. The overhead expressions 12 * num_edges + k and 16 * num_edges - num_vertices + 2 * k * num_vertices cannot be compiled because k is not a getter method on MinimumVertexCover.

   This is a fundamental issue: the Garey & Johnson reduction is from the decision version of Vertex Cover (given G and K, does a VC of size ≤ K exist?) to the decision version of Hamiltonian Circuit (does a HC exist?). But MinimumVertexCover in this codebase is the optimization version with no K parameter. The reduction as stated cannot be directly implemented without either:

   • (a) Adding a k parameter to MinimumVertexCover (breaking change), or
   • (b) Reformulating the reduction for the optimization setting (e.g., fixing K = minimum VC size, but this defeats the purpose), or
   • (c) Implementing Vertex Cover as a separate satisfaction/decision problem with a K parameter.

2. Target metric names are unverifiable. Since HamiltonianCircuit does not exist yet, the target metric code names (num_vertices, num_edges) cannot be validated against actual getter methods. The planned model (HamiltonianCycle in the existing plan) may use different field names.

3. Problem name mismatch. The issue title says "HAMILTONIAN CIRCUIT" but the existing model plan uses "HamiltonianCycle". These terms are sometimes used interchangeably in the literature (both refer to a cycle visiting all vertices exactly once), but the naming must be consistent with whatever model gets implemented.

4d: Example Quality

The K₄ example is reasonable (4 vertices, 6 edges, K=3), and the construction is fully worked through including gadget details, vertex paths, selector connections, and solution mapping. The resulting instance (75 vertices, 116 edges) is too large for hand verification but the step-by-step construction is clear. ⚠️ A smaller example (e.g., a triangle K₃ with K=2) would be more practical for manual verification.

---

Recommendations

1. Resolve the optimization vs. decision problem mismatch. This is the most critical issue. The reduction fundamentally requires a k parameter that doesn't exist on the optimization MinimumVertexCover. Consider whether this should reduce from a decision version of Vertex Cover, or whether the reduction can be reformulated to work with the optimization problem (e.g., by setting K = num_vertices as an upper bound, though this changes the overhead semantics).

2. Reconcile naming. Decide whether the target problem will be called HamiltonianCircuit or HamiltonianCycle, and align with the existing model plan.

3. Implement the target model first. This rule is blocked until HamiltonianCircuit/HamiltonianCycle exists as a problem model.

4. Consider a smaller worked example. K₃ with K=2 would give 39 vertices and be easier to verify by hand.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	HamiltonianCircuit does not exist in the reduction graph; no existing path from MinimumVertexCover to any Hamiltonian problem
Non-trivial	✅ Pass	12-vertex cover-testing gadget construction with cross-links and selector vertices is a genuine structural transformation
Correctness	✅ Pass	Garey & Johnson (1979) Theorem 3.4 is a well-known, verified result; book already in project bibliography as garey1979
Well-written	❌ Fail	Overhead table uses undefined variable k; reduction assumes decision-problem formulation incompatible with codebase's optimization model; see details below

Overall: 3 passed, 0 warnings, 1 failed

---

Usefulness

HamiltonianCircuit is not currently implemented in the codebase. Running pred list confirms no Hamiltonian problem exists. There is no existing path from MinimumVertexCover to any tour-related problem (the only targets are MaximumIndependentSet and MinimumSetCovering). This reduction would be novel and would connect the vertex cover family to Hamiltonian/tour problems, enabling downstream reductions to TSP and others.

Non-trivial

The reduction constructs 12-vertex cover-testing gadgets per edge with cross-links at positions 3-1 and 6-4, vertex path chaining edges, and selector vertices with full bipartite connections. This is a substantial structural transformation involving gadgets, not a variable substitution or subtype coercion.

Correctness

The reference is Garey & Johnson, Computers and Intractability, Theorem 3.4, pp. 56-60. This book is already in the project bibliography (garey1979 in docs/paper/references.bib). The reduction description in the issue is essentially a verbatim transcription of the theorem and proof from the book, including the gadget figures (3.4, 3.5, 3.6). The construction and correctness argument are well-established in the complexity theory literature and widely taught in algorithms courses.

The Karp reduction tree (per references.md) shows the classical chain VC -> Feedback Node Set -> Directed HC -> Undirected HC, but the Garey & Johnson direct reduction from VC to (undirected) HC is equally valid and well-known.

Well-written

Several issues need to be addressed:

1. Decision vs. Optimization Mismatch (critical)

The reduction is formulated as a decision problem: "Given graph G and integer K, does G have a vertex cover of size <= K?" mapped to "Does G' have a Hamiltonian circuit?" However, in this codebase, MinimumVertexCover is an optimization problem (OptimizationProblem with Metric = SolutionSize<W>), not a decision problem. There is no K parameter on the MinimumVertexCover struct.

The issue needs to explain how this decision-to-decision reduction maps onto the codebase's optimization-to-satisfaction framework. If the target HamiltonianCircuit is a SatisfactionProblem (Metric = bool), the reduction from an optimization source to a satisfaction target is unusual and would need careful design. The K parameter would need to come from somewhere — either the reduction creates a family of target instances, or the formulation needs rethinking.

2. Undefined Variable k in Overhead Table

The overhead table references k (the cover size bound), but MinimumVertexCover's size fields are only num_edges and num_vertices. The variable k is not a getter method on the source type and would cause a compile error in the #[reduction(overhead = {...})] macro. The overhead expressions must use only variables that correspond to actual getter methods.

Specifically:

• num_vertices = 12 * num_edges + k — k is undefined
• num_edges = 16 * num_edges - num_vertices + 2 * k * num_vertices — k is undefined

The issue must either (a) reformulate the overhead without k, or (b) explain how k will be exposed as a getter method.

3. Target Model Does Not Exist

HamiltonianCircuit is not implemented in the codebase. A [Model] issue for HamiltonianCircuit should be filed and implemented first before this rule can be added. The issue should reference the dependency.

4. Symbol Consistency

The algorithm section uses n = |V| and m = |E|, but the overhead table switches to num_vertices and num_edges without explicitly mapping between them. While this is inferable, the notation should be consistent per the template requirements.

5. Example is Adequate but Large

The K_4 example (75 vertices, 116 edges in the target) is too large to verify by hand but is structurally appropriate. A smaller example (e.g., a path P_3 or triangle) would be more useful for manual verification in tests.

Recommendations

• File a separate [Model] issue for HamiltonianCircuit first, defining it as a SatisfactionProblem.
• Reconsider the reduction formulation: either (a) add a cover_bound field to MinimumVertexCover (unlikely to be accepted since it changes the optimization model), or (b) reformulate as a reduction from a decision version of VertexCover, or (c) find an alternative encoding that avoids the parameter k entirely.
• Add a smaller worked example (e.g., triangle graph with K=2) for easier manual verification.
• Explicitly define the mapping between mathematical notation (n, m, K) and code getter names (num_vertices, num_edges) at the start of the Size Overhead section.

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Novel reduction; no existing path from MinimumVertexCover to HamiltonianCircuit
Non-trivial	✅ Pass	12-vertex cover-testing gadgets with cross-links and selector vertices
Correctness	❌ Fail	Overhead uses undefined variable k; source/target schema mismatch (optimization vs decision)
Well-written	❌ Fail	k not a valid source metric; optimization→decision formulation gap unaddressed

Overall: 2 passed, 0 warnings, 2 failed

---

Usefulness

No existing path from MinimumVertexCover to any Hamiltonian problem. pred path MinimumVertexCover HamiltonianCircuit returns no path. This would be a novel connection from the vertex cover family to tour-finding problems (HC, HP, TSP). Pass.

Non-trivial

The reduction constructs 12-vertex cover-testing gadgets per edge with internal cross-links at positions 3→1 and 6→4, vertex path chaining, and selector vertices with full bipartite connections. This is a genuine structural transformation — not a variable substitution, subtype coercion, or identity. Pass.

Correctness

Reference verification: ✅ Garey & Johnson, Computers and Intractability, Theorem 3.4, pp. 56–60. Already in the project bibliography as garey1979. The construction is a faithful transcription of the textbook proof, including gadget structure (Figures 3.4–3.6), traversal modes (a/b/c), and both directions of the if-and-only-if argument.

Example verification: ✅ Python brute-force script verified:

• K₄ minimum vertex cover is indeed size 3 (all 6 pairs of size 2 checked; none covers all edges)
• K₄ reduction: |V'| = 75, |E'| = 116 — matches the formulas 12m+k and 16m−n+2kn
• Hamiltonian circuit constructed from VC {0,1,2} visits all 75 vertices exactly once using only valid edges
• K₃ reduction (smaller example): |V'| = 38, |E'| = 57 — matches formulas; valid Hamiltonian circuit confirmed

Source/target definition match: ❌ The reduction is formulated as a decision problem: "Given G and integer K, does G have a vertex cover of size ≤ K?" → "Does G' have a Hamiltonian circuit?" However, in this codebase MinimumVertexCover is an optimization problem (OptimizationProblem with Metric = SolutionSize<i32>, direction = Minimize). It has no K parameter — its schema has fields graph and weights only (pred show MinimumVertexCover --json). The reduction as described cannot be implemented because the number of selector vertices depends on K, which doesn't exist on the source type.

Overhead expression correctness: ❌ The overhead table uses k:

• num_vertices = 12 * num_edges + k
• num_edges = 16 * num_edges - num_vertices + 2 * k * num_vertices

Variable k is not a getter method on MinimumVertexCover. Source size_fields are only ["num_edges", "num_vertices"]. These expressions would fail to compile in the #[reduction(overhead = {...})] macro, which validates variable names against actual getter methods at compile time.

Overall Correctness: Fail — the mathematical content (G&J Theorem 3.4) is correct and verified, but the adaptation to this codebase's type system is flawed. The reduction fundamentally requires a parameter K that doesn't exist on the optimization model.

Well-written

4a: Required sections: All present and substantive. ✅

4b: Algorithm completeness: Detailed step-by-step construction from the textbook, including the full verbatim proof and a clear summary. Implementable (for the decision version). ✅

4c: Symbol and notation consistency: ❌

1. k is not a valid source metric. The issue defines k as the "cover size bound parameter (K)" but MinimumVertexCover has no such parameter. The overhead expressions 12 * num_edges + k and 16 * num_edges - num_vertices + 2 * k * num_vertices cannot be compiled.
2. Optimization→satisfaction gap unaddressed. The issue doesn't discuss how this decision-to-decision reduction maps onto the codebase's optimization-to-satisfaction framework. If implemented as ReduceTo<HamiltonianCircuit<SimpleGraph>> for MinimumVertexCover<SimpleGraph, i32>, the reduce_to() method would need to choose a value for K — but there's no principled way to do this for an optimization problem without fundamentally changing the reduction's semantics.
3. Target size_fields is empty. pred show HamiltonianCircuit --json reports size_fields: [], though the model does have num_vertices() and num_edges() getter methods. The overhead target metric names (num_vertices, num_edges) reference valid getters, so this is a minor registration issue, not a blocker.

4d: Example quality: ✅ The K₄ example is fully worked through — gadget vertices and edges, vertex paths, selector connections, and solution mapping are all explicitly enumerated. Verified by Python script. A smaller K₃ example would be preferable for manual verification (38 vs 75 vertices), but the K₄ example is adequate.

Overall Well-written: Fail — due to the undefined k variable and the unaddressed formulation gap.

Recommendations

1. Resolve the optimization→decision mismatch. Options:

   • (a) Reformulate as a reduction from a decision version of Vertex Cover (a separate SatisfactionProblem with a bound field). This would require filing a [Model] issue for VertexCoverDecision or similar.
   • (b) Find an alternative encoding that avoids K — e.g., set K = n (always valid VC) but this makes the reduction trivially true and useless.
   • (c) Add a cover_bound field to MinimumVertexCover — unlikely to be accepted as it changes an established optimization model.

   Option (a) is the most architecturally sound approach.

2. Update overhead expressions to use only valid source getter names once the formulation is resolved.

3. Note the target size_fields gap — HamiltonianCircuit's size_fields is empty despite having num_vertices() and num_edges() getters. This may need a fix in the model before the reduction can register overhead metrics.