[Rule] ThreeDimensionalMatching → ILP (direct)

[GiggleLiu]

Motivation

PR #1010 adds ThreeDimensionalMatching → ThreePartition, which creates an indirect ILP path:

3DM → ThreePartition → ResourceConstrainedScheduling → ILP

This chain has O(n^2) blowup: a 5-triple canonical example produces 114,075 binary ILP variables, causing HiGHS to hang and CI to time out (2+ hours).

A direct ThreeDimensionalMatching → ILP reduction produces 5 variables and 9 constraints for the same instance.

Source

ThreeDimensionalMatching

Target

ILP<bool>

Reference

Alexander Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 29.11. Book metadata: https://books.google.com/books?id=mqGeSQ6dJycC.

This is the standard textbook 0-1 ILP pattern for set packing / set covering / matching problems: use one binary variable per candidate set (here, per triple) and enforce incidence constraints so each required element is covered exactly once. The direct ThreeDimensionalMatching → ILP rule is exactly that formulation specialized to the three coordinate classes W, X, and Y.

Reduction Checklist

#	Item	Value
1	Source	ThreeDimensionalMatching
2	Target	ILP<bool>
3	Reduction	Let k = universe_size, let the triples be t_0, ..., t_{n-1} where n = num_triples, and create one binary variable x_j for each j in {0, ..., n-1}. For each element value in each dimension W, X, and Y, add an equality constraint requiring exactly one selected triple to contain that value in that dimension. This is a feasibility reduction with an empty objective.
4	Solution extraction	Identity: x_j = 1 means triple t_j is selected
5	Correctness	The W constraints force each W element to appear exactly once, the X constraints force each X element to appear exactly once, and the Y constraints force each Y element to appear exactly once. Therefore feasible ILP solutions are exactly perfect 3-dimensional matchings, and vice versa.
6	Overhead	num_vars = "num_triples", num_constraints = "3 * universe_size"
7	Example	For universe_size = 3 and triples [(0,1,2),(1,0,1),(2,2,0),(0,0,0),(1,2,2)], the target ILP has variables x_0, ..., x_4 and the 9 equality constraints listed below. Its unique feasible solution is x = [1,1,1,0,0], corresponding to triples t_0, t_1, t_2.
8	Solving	Direct ILP via HiGHS
9	Reference	Schrijver (2003), Combinatorial Optimization: Polyhedra and Efficiency, Section 29.11

Implementation Pattern

Follow src/rules/exactcoverby3sets_ilp.rs — nearly identical structure (binary variable per subset, exact-cover constraints per element). The only difference is 3 groups of constraints (one per dimension W, X, Y) instead of 1.

Reduction Algorithm

Given a ThreeDimensionalMatching instance:

• let k = universe_size
• let the triple list be M = {t_0, ..., t_{n-1}}, where n = num_triples
• write each triple as t_j = (a_j, b_j, c_j) with a_j, b_j, c_j in {0, ..., k-1}

Construct an ILP<bool> instance as follows:

1. Introduce one binary decision variable x_j in {0,1} for each triple index j in {0, ..., n-1}.
2. For each a in {0, ..., k-1}, add the W-dimension exact-cover constraint
   sum_{j : a_j = a} x_j = 1.
3. For each b in {0, ..., k-1}, add the X-dimension exact-cover constraint
   sum_{j : b_j = b} x_j = 1.
4. For each c in {0, ..., k-1}, add the Y-dimension exact-cover constraint
   sum_{j : c_j = c} x_j = 1.
5. Use an empty objective with ObjectiveSense::Minimize, since this is a pure feasibility problem.
6. Extract a source witness by selecting exactly those triples t_j with x_j = 1.

Size Overhead

Target metric	Formula
num_vars	n = num_triples
num_constraints	3k = 3 * universe_size

Validation Method

Validate the rule in three complementary ways:

1. Closed-loop witness check on the canonical example: solve the source ThreeDimensionalMatching instance by brute force, solve the reduced ILP instance with HiGHS, extract the selected triples, and confirm the extracted witness is a perfect 3-dimensional matching for the source.
2. Infeasible-instance check: use a small instance where some coordinate value cannot be covered exactly once and confirm that both the source problem and the reduced ILP instance are infeasible.
3. Cross-check against the existing indirect path: on small brute-force-solvable instances, compare the direct ThreeDimensionalMatching → ILP result against the current indirect path ThreeDimensionalMatching → ThreePartition → ResourceConstrainedScheduling → ILP to ensure both produce the same yes/no answer while the direct path has strictly smaller exported overhead.

Example

1. Source instance

Let k = 3 and let the triples be

• t_0 = (0,1,2)
• t_1 = (1,0,1)
• t_2 = (2,2,0)
• t_3 = (0,0,0)
• t_4 = (1,2,2)

So the source instance is:

ThreeDimensionalMatching::new(
    3,
    vec![(0,1,2), (1,0,1), (2,2,0), (0,0,0), (1,2,2)],
)

2. Construction

Create five binary ILP variables x_0, x_1, x_2, x_3, x_4, one for each triple.

The exact-cover constraints are:

W-dimension constraints

1. value 0 appears in t_0 and t_3: x_0 + x_3 = 1
2. value 1 appears in t_1 and t_4: x_1 + x_4 = 1
3. value 2 appears only in t_2: x_2 = 1

X-dimension constraints

4. value 0 appears in t_1 and t_3: x_1 + x_3 = 1
5. value 1 appears only in t_0: x_0 = 1
6. value 2 appears in t_2 and t_4: x_2 + x_4 = 1

Y-dimension constraints

7. value 0 appears in t_2 and t_3: x_2 + x_3 = 1
8. value 1 appears only in t_1: x_1 = 1
9. value 2 appears in t_0 and t_4: x_0 + x_4 = 1

The ILP uses an empty objective because it is only checking feasibility.

3. Target instance

The resulting target problem is an ILP<bool> instance with:

• num_vars = 5
• num_constraints = 9
• objective = []
• sense = ObjectiveSense::Minimize

Solving the constraints forces:

• x_0 = 1 from constraint 5
• x_1 = 1 from constraint 8
• x_2 = 1 from constraint 3
• x_3 = 0 from constraints 1, 4, or 7
• x_4 = 0 from constraints 2, 6, or 9

Hence the extracted witness is the triple set {t_0, t_1, t_2}, which covers each value in W, X, and Y exactly once, so it is a perfect 3-dimensional matching.

Files to Create/Modify

• src/rules/threedimensionalmatching_ilp.rs — reduction implementation
• src/unit_tests/rules/threedimensionalmatching_ilp.rs — tests (closed-loop, structure, infeasible case)
• src/rules/mod.rs — add mod threedimensionalmatching_ilp; (feature-gated ilp-solver)
• src/example_db/rule_builders.rs — add canonical example builder
• docs/paper/reductions.typ — add reduction-rule entry
• Run cargo run --example export_graph and make regenerate-fixtures

Priority

Blocks PR #1010 — without this, CI hangs for 2+ hours because model_specs_are_optimal tries the indirect 3-step path.

BibTeX

@book{schrijver2003combinatorial,
  author = {Schrijver, Alexander},
  title = {Combinatorial Optimization: Polyhedra and Efficiency},
  publisher = {Springer},
  year = {2003},
  isbn = {9783540443896}
}

[GiggleLiu]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No direct ThreeDimensionalMatching -> ILP rule exists. The current path is ThreeDimensionalMatching -> ThreePartition -> SequencingWithReleaseTimesAndDeadlines -> ILP, and the existing ThreeDimensionalMatching -> ThreePartition step already has quadratic overhead in num_triples, so the proposed direct rule would materially improve the graph if implemented as written.
Non-trivial	✅ Pass	This is a genuine structural encoding: one binary variable per triple plus exact-cover constraints across all three dimensions. It is not a rename, subtype coercion, or identity reduction.
Correctness	❌ Fail	The cited reference Garey & Johnson, 1979 is real and is already in docs/paper/references.bib, but I could not verify it as a source for this specific direct ThreeDimensionalMatching -> ILP construction. The project knowledge base confirms 3DM and 0-1 Integer Programming as classical NP-complete problems, not this particular reduction.
Well-written	❌ Fail	The issue is close to implementable, but it is missing the required Validation Method section from the rule template, the worked example does not spell out the concrete 9 ILP constraints, and the notation is slightly inconsistent (j = 0..num_triples in the checklist vs. x_0, ..., x_{n-1} later).

Overall: 2 passed, 2 failed

---

Usefulness

pred path ThreeDimensionalMatching ILP --json finds an existing 3-step path:

ThreeDimensionalMatching -> ThreePartition -> SequencingWithReleaseTimesAndDeadlines -> ILP<bool>

The current first step already expands as:

• num_elements = 24 * num_triples^2 - 3 * num_triples
• num_groups = 8 * num_triples^2 - num_triples

(from src/rules/threedimensionalmatching_threepartition.rs), so the existing path is clearly superlinear before the scheduling-to-ILP step is even applied. By contrast, the proposed rule claims:

• num_vars = num_triples
• num_constraints = 3 * universe_size

That is a meaningful improvement, so this issue passes the usefulness check.

Non-trivial

The proposed mapping constructs a new ILP instance with:

• one decision variable per source triple,
• equality constraints for each element in W, X, and Y,
• witness extraction by reading back the selected variables.

That is a bona fide reduction with structural transformation. It is also closely aligned with the existing ExactCoverBy3Sets -> ILP pattern in the repo, which supports the judgment that this is non-trivial rather than a restatement.

Correctness

I verified the cited source exists:

• docs/paper/references.bib already contains @book{garey1979, ...}
• .claude/skills/check-issue/references.md lists both 3-Dimensional Matching and Integer Programming as classical Garey-Johnson problems

What I could not verify is the specific claim that this direct ILP formulation is sourced from that reference. The issue currently cites only:

Standard ILP formulation of exact matching (Garey & Johnson, 1979)

That is too vague for a correctness pass. The repo-local knowledge base supports the problem background, but not this exact formulation or a theorem/page pointer for it. Under this skill's rules, an unverifiable literature claim is a failure.

Well-written

The issue is mathematically close to implementable, but it does not fully satisfy the rule template:

• The template requires a ## Validation Method section; the issue has Solving: Direct ILP via HiGHS, which is a solver choice, not a validation method.
• The example identifies the source instance and intended witness, but it does not show the resulting target ILP constraints explicitly. For a paper/test fixture, the 9 equality constraints should be listed.
• The checklist says j = 0..num_triples, while the later construction uses x_0, ..., x_{n-1}. That should be normalized to one indexing convention.

The positive side is that the metric names are valid:

• target metrics num_vars and num_constraints both exist on ILP
• source getters universe_size and num_triples both exist on ThreeDimensionalMatching

Recommendations

• Replace the current reference with a source that explicitly states this exact 3DM / exact-cover ILP formulation, or add a precise theorem/page pointer if Garey & Johnson really is the intended source.
• Add a real Validation Method section, for example: compare direct-ILP solutions against brute-force 3DM on the canonical example and on an infeasible instance, and cross-check small cases against the existing indirect path.
• Expand the worked example by listing all 9 equality constraints for the 5-triple instance.
• Normalize the indexing notation to j in {0, ..., n-1} throughout.

[GiggleLiu]

Issue Quality Check — Rule (Re-check)

Previous report on 2026-04-06: 2 passed, 2 failed.

Current report: 4 passed, 0 failed, 0 warnings.

Check	Result	Details
Usefulness	✅ Pass	No direct ThreeDimensionalMatching -> ILP rule exists, and pred path ThreeDimensionalMatching ILP --json still shows only the larger 3-step indirect path through ThreePartition and ResourceConstrainedScheduling.
Non-trivial	✅ Pass	The issue specifies a genuine structural encoding: one binary variable per triple and three families of exact-cover equality constraints, one for each coordinate class.
Correctness	✅ Pass	The vague Garey & Johnson citation has been replaced with a precise textbook reference to Schrijver (2003), Section 29.11, and the issue now states the claim at the right level: this rule is a direct specialization of the standard 0-1 ILP formulation pattern for set packing / set covering / matching problems.
Well-written	✅ Pass	The missing Validation Method section has been added, the worked example now lists all 9 ILP constraints explicitly, and the indexing / symbol definitions are consistent throughout.

Overall: 4 passed, 0 failed

---

Usefulness

pred path ThreeDimensionalMatching ILP --json still finds only the indirect path

ThreeDimensionalMatching -> ThreePartition -> ResourceConstrainedScheduling -> ILP<bool>

with quadratic blowup already present in the first step. The proposed direct rule remains clearly useful because it targets

• num_vars = num_triples
• num_constraints = 3 * universe_size

instead of the substantially larger composite path.

Non-trivial

This is still a bona fide reduction rather than a relabeling:

• the source triples become ILP decision variables,
• the target introduces three separate exact-cover constraint families,
• witness extraction is specified explicitly by reading back the selected variables.

That is enough structural transformation for a clean pass.

Correctness

I re-checked the revised citation and the claim it is being used to support.

• The issue now cites a specific textbook source: Alexander Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Section 29.11.
• The body no longer makes the vague claim that Garey & Johnson directly contains this exact ThreeDimensionalMatching -> ILP construction.
• Instead, it cites Schrijver for the standard incidence-based 0-1 ILP formulation pattern for covering / packing / matching problems and then specializes that pattern to 3DM.

That is the right level of literature support for this issue. The last step is an inference from the issue's construction, not a verbatim theorem statement from the book, and the revised text now makes that inference explicit instead of overstating the source.

Well-written

The previous writing failures are resolved:

• ## Validation Method is now present and describes three concrete verification strategies.
• The worked example now shows the full target instance, including all 9 equality constraints.
• Symbols are defined before use (k = universe_size, n = num_triples) and indexing is normalized to j in {0, ..., n-1} throughout.

No further mechanical issues are blocking implementation.

[GiggleLiu]

Fix-issue changelog

• Added explicit Source, Target, Reference, Reduction Algorithm, Size Overhead, Validation Method, and Example sections so the issue matches the rule template.
• Replaced the vague Garey & Johnson, 1979 correctness citation with a precise textbook reference to Schrijver (2003), Section 29.11.
• Normalized the indexing notation to j in {0, ..., n-1} and defined k = universe_size, n = num_triples in the algorithm.
• Expanded the worked example into the full 5-variable, 9-constraint ILP and spelled out the extracted witness.
• Added a concrete validation plan covering closed-loop testing, infeasible cases, and cross-checks against the existing indirect ILP path.

Applied by /fix-issue.

[GiggleLiu]

Implemented in PR #1010 as src/rules/threedimensionalmatching_ilp.rs. The direct ILP formulation produces 5 variables / 9 constraints for the canonical example vs 114K variables via the indirect path.