[Rule] MinimumHittingSet to MinimumSetCovering #1094

Activity

1. isPANN

   added

   ruleA new reduction rule to be added.A new reduction rule to be added.

   on Aug 1, 2026
2. github-project-automation

   added this to Good issueson Aug 1, 2026
3. isPANN commented on Aug 1, 2026

   

   isPANN

   on Aug 1, 2026

   CollaboratorAuthor

   More actions

   Issue Quality Check — Rule

   Check	Result	Details
   Usefulness	✅ Pass	pred path MinimumHittingSet MinimumSetCovering --json reports no path, so this adds a missing connection.
   Non-trivial	✅ Pass	The construction transposes the full element–set incidence relation and changes the target universe and set family; it is not a relabeling or subtype coercion.
   Correctness	✅ Pass	The cited Garey–Johnson definitions are genuine, and an independent source gives the same hitting-set-to-set-cover construction and optimal-solution correspondence.
   Completeness	❌ Fail	The combinatorial mapping handles the traced set-system edge cases, but MinimumSetCovering/i32 cannot preserve the full usize-cardinality source domain because its objective sum can overflow.
   Well-written	✅ Pass	Every required section is present; the construction, extraction map, symbols, target metric names, validation plan, and worked example are implementable as written.

   Overall: 4 passed, 1 failed, 0 warnings

   ---

   Usefulness

   Both endpoints resolve in the current registry:

   • MinimumHittingSet has size fields num_sets and universe_size.
   • MinimumSetCovering {weight: "i32"} has size fields num_sets and universe_size.

   pred path MinimumHittingSet MinimumSetCovering --json returns no reduction path. A redundancy analysis is therefore unnecessary under the check procedure. The motivation identifies the concrete missing graph connection between two fundamental covering formulations.

   Non-trivial

   For source incidence relation u ∈ C_j, the issue constructs the dual set system with target element j and target set D_u = {j : u ∈ C_j}. This transposes an m × n incidence relation into an n-set cover over m target elements and defines an explicit solution map. It is a genuine structural transformation.

   Correctness

   Reference verification:

   • Garey and Johnson, Computers and Intractability (1979), Appendix A3, pp. 222–223, contains [SP5] MINIMUM COVER and [SP8] HITTING SET. The entries define the same unrestricted finite-set-family incidence semantics used by the issue. The repository bibliography also contains this book as garey1979.
   • The issue carefully does not claim that Garey–Johnson states this direction as a named theorem. That qualification is accurate.
   • Independent cross-check: Yufei Tao's CSCI3160 Exercise 13 solution gives exactly the same bipartite-incidence construction: one set N_e for each source element, over the source-set vertices, and states that an optimal target cover maps to an optimal hitting set (solution, Problem 1).
   • A second independent account defines the dual set system (T, P*), where each source point p creates the set of ranges containing it, and states that a hitting set of the primal is a set cover of the dual (Definition 1.16, Section 1.3).

   Direct proof check: for every selection vector x ∈ {0,1}^n and target element j, j is covered iff some selected D_u contains j, iff some selected u lies in C_j, iff the corresponding source selection hits C_j. Because each selected source element corresponds to one unit-weight target set, the intended cardinalities agree whenever the target numeric sum is representable.

   No better-overhead construction was found: materializing the dual incidence relation is the standard direct construction, with exactly m target universe elements and n target sets.

   Completeness

   Literature scope: Garey–Johnson's [SP5] and [SP8] entries use arbitrary collections of subsets of finite sets; neither definition assumes connectedness, nonempty members, distinct members, or that every universe element occurs. The independent dual-set-system construction likewise imposes no structural precondition on the incidence relation.

   Codebase scope:

   • MinimumHittingSet::new accepts universe_size = 0, an empty outer family, empty member sets, repeated outer sets, and unused universe elements. It only rejects member indices outside 0..universe_size; it sorts/deduplicates elements within each member set.
   • Existing source rules minimumhittingset_ilp.rs and minimumvertexcover_minimumhittingset.rs preserve the same 1:1 source-variable interpretation and do not impose an additional source restriction.
   • MinimumSetCovering<i32>::evaluate accumulates selected unit weights in an i32 sum.

   Hand traces beyond the worked example:

   1. Empty family: take U={0,1,2} and C=[]. The construction produces target universe U'=∅ and three empty target sets. The empty target selection is feasible with value 0 and maps to the empty hitting set, which vacuously hits every source member. Unused source elements remain harmless empty target sets.
   2. Empty member: take U={0,1} and C=[∅,{0}]. The construction produces U'={0,1}, D_0={1}, and D_1=∅. Target element 0 cannot be covered, so the target is infeasible; the source is also infeasible because no selection can hit the empty member.
   3. Repeated members: repeated source sets become distinct target elements with identical incidence neighborhoods. Covering both is equivalent to hitting the repeated source member, and the configuration extraction remains 1:1.

   The failure is the claimed complete source domain with the fixed i32 target variant. MinimumHittingSet measures cardinality in usize, while MinimumSetCovering/i32 sums unit weights in i32. For example, the source model can represent universe_size = 2^31 with an empty family. Its dual has 2^31 empty target sets. Since the target universe is empty, selecting all those sets is a feasible target configuration, but adding 2^31 unit i32 weights overflows (panic with overflow checks; wrapped value otherwise). Thus the target objective is not a valid cardinality-preserving image for every legitimate source configuration, and a solver can no longer rely on the claimed equal objective/order.

   This must be resolved by using a target weight/sum type that represents the full source cardinality domain, or by exposing a genuine source restriction supported by the codebase. The current issue may not claim full-domain preservation with MinimumSetCovering/i32.

   Well-written

   All required template sections are substantive. Symbols U, n, C, m, U', and D_u are defined before use. The overhead names match the target's actual size_fields, and the exact counts are correct: target universe_size = num_sets and target num_sets = universe_size. The extraction map is explicit. The five-element/four-member example is non-degenerate and contains feasible selections of different cardinalities, so it can support a meaningful closed-loop test.

   Recommendations

   • Change the target numeric variant (and, if needed, add the corresponding model support) so that unit-weight sums cannot overflow relative to MinimumHittingSet::Value = Min<usize>.
   • Keep the empty-family, empty-member, repeated-member, and unused-element cases as explicit closed-loop tests; they exercise the completeness claims well.
4. isPANN

   added

   IncompleteReduction doesn't cover all source instances (Rule Check 5)Reduction doesn't cover all source instances (Rule Check 5)

   on Aug 1, 2026
5. isPANN

   moved this to Backlog in Good issueson Aug 1, 2026
6. isPANN

   moved this from Backlog to OnHold in Good issueson Aug 1, 2026
7. isPANN commented on Aug 1, 2026

   

   isPANN

   on Aug 1, 2026

   CollaboratorAuthor

   More actions

   Rule Fix -- Failed

   Checklist results:

   #	Check	Verdict	Reason
   1	Reduction direction	PASS	The construction maps a MinimumHittingSet instance to a MinimumSetCovering instance by transposing the incidence relation.
   2	Forward proof	PASS	Every hitting set selects the corresponding dual sets and covers every target element.
   3	Backward proof	PASS	Every target cover selects source elements intersecting every source member.
   4	Gadget completeness	PASS	The dual incidence sets enforce exactly the source hitting constraints.
   5	Solution extraction	PASS	The configuration vectors have the same universe_size length and the identity map is explicit.
   6	Polynomial time	PASS	Materializing the transposed incidence relation is polynomial in the source representation and output size.
   7	Overhead consistency	PASS	The target has exactly num_sets universe elements and universe_size sets.
   8	Example correctness	PASS	Exhaustive enumeration confirms the worked example has optimum 2 on both sides.
   9	Type compatibility	FAIL	The source value is Min<usize>, while MinimumSetCovering/i32 has value Min<i32>; the target cannot represent all source cardinalities.
   10	Objective/bound preservation	FAIL	For sufficiently large instances, summing unit i32 weights overflows instead of preserving the usize optimum.
   11	Target-instance validity	PASS	The transposed sets contain only valid target-universe indices, including empty and repeated-set cases.
   12	Undirected rerouting vulnerability	PASS	This is a set-system reduction, not an undirected path-gadget construction.

   Literature findings:

   • Yufei Tao's CSCI3160 Exercise 13 solution gives the same canonical construction: create one target set N_e for each source element, over the source-set vertices, and map an optimal cover back to the corresponding hitting set: https://www.cse.cuhk.edu.hk/~taoyf/course/3160/24-fall/ex/ex13-sol.pdf
   • Definition 1.16 and Section 1.3 of the cited dual-set-system treatment define (T, P*) with one dual set for each primal point and state that a primal hitting set is a dual set cover: https://pure.mpg.de/rest/items/item_2169875_4/component/file_2169879/content
   • The issue matches the canonical combinatorial construction. The divergence is repository-specific: its concrete target variant accumulates weights in i32, whereas the source cardinality is usize.

   Failing instance:

   • Source: universe_size = 2,147,483,648 and the singleton family C = ({u} : 0 <= u < universe_size).
   • Construction: the dual target has the same number of singleton sets, each with weight 1.
   • Expected: the unique source and target optimum is 2,147,483,648.
   • Actual: MinimumSetCovering/i32 cannot represent that objective; evaluation overflows (panic with overflow checks, wrapping otherwise).

   Smoke test:

   • 133 checks exercised the issue's YES example, a NO example, five edge cases, 38 small set systems, solution extraction, target validity, exact overhead, and the full-domain boundary.
   • All small combinatorial checks passed; the full-domain objective/type check failed.

   Attempts: No rewrite attempt was made. The fix-rule-issue workflow classifies type incompatibility as outside the fixable issue-body scope. Manual intervention is required: first provide an existing MinimumSetCovering variant whose accumulated objective represents the full usize cardinality domain, then retarget this rule to that variant.
8. isPANN commented on Nov 3, 2026

   

   isPANN

   on Nov 3, 2026

   CollaboratorAuthor

   More actions

   Please kindly check the following items (PR #1232):

   • Paper (PDF): check definition, proof sketch, example figure, and reproducible pred commands
   • Implementation (Optional): spot-check the source files changed in this PR for correctness

   Join the discussion on Zulip — feel free to ask questions or leave feedback there.