Skip to content

Commit ac6ff0a

Browse files
GiggleLiuclaude
andcommitted
feat: add Clustering→ILP and MinimumFaultDetectionTestSet→ILP reductions
Clustering→ILP: binary assignment variables x[i,c], exact-one-cluster constraints per element, conflict constraints for violated distance pairs. Feasibility formulation (minimize 0). O(n·K) variables, O(n + n²·K) constraints. MinimumFaultDetectionTestSet→ILP: binary selection variables per input-output pair, covering constraints requiring each internal vertex appears in at least one selected pair's coverage set. Minimize total selected pairs. O(|I|·|O|) variables, O(internal vertices) constraints. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent dd714ee commit ac6ff0a

7 files changed

Lines changed: 508 additions & 0 deletions

File tree

docs/paper/reductions.typ

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15161,6 +15161,50 @@ The following table shows concrete variable overhead for example instances, take
1516115161
_Solution extraction._ Read the cluster label of each source vertex as its color label.
1516215162
]
1516315163

15164+
#let clustering_ilp = load-example("Clustering", "ILP")
15165+
#let clustering_ilp_sol = clustering_ilp.solutions.at(0)
15166+
#reduction-rule("Clustering", "ILP",
15167+
example: true,
15168+
example-caption: [4 elements, $K = 2$, $B = 1$ $arrow.r$ ILP with #clustering_ilp.target.instance.num_vars variables and #clustering_ilp.target.instance.constraints.len() constraints],
15169+
extra: [
15170+
#pred-commands(
15171+
"pred create --example " + problem-spec(clustering_ilp.source) + " -o clustering.json",
15172+
"pred reduce clustering.json --to " + target-spec(clustering_ilp) + " -o bundle.json",
15173+
"pred solve bundle.json",
15174+
"pred evaluate clustering.json --config " + clustering_ilp_sol.source_config.map(str).join(","),
15175+
)
15176+
15177+
#{
15178+
let n = clustering_ilp.source.instance.distances.len()
15179+
let k = clustering_ilp.source.instance.num_clusters
15180+
let b = clustering_ilp.source.instance.diameter_bound
15181+
let distances = clustering_ilp.source.instance.distances
15182+
let source-config = clustering_ilp_sol.source_config
15183+
[
15184+
*Step 1 -- Source instance.* The canonical source has $n = #n$ elements, cluster bound $K = #k$, and diameter bound $B = #b$. Its distance rows are #distances.map(row => "(" + row.map(str).join(", ") + ")").join("; "), so the only pairs above the bound are $(0, 2)$, $(0, 3)$, $(1, 2)$, and $(1, 3)$.
15185+
15186+
*Step 2 -- Build the ILP.* Introduce one binary variable $x_(i,c)$ for each element-cluster pair, giving $n K = #(n * k)$ variables. The $n = #n$ assignment equalities $sum_c x_(i,c) = 1$ force every element into exactly one cluster, and the four violating pairs contribute $4 dot K = #(4 * k)$ conflict inequalities. The stored target therefore has #clustering_ilp.target.instance.num_vars variables and #clustering_ilp.target.instance.constraints.len() constraints.
15187+
15188+
*Step 3 -- Verify the canonical witness.* The stored ILP vector is $(#clustering_ilp_sol.target_config.map(str).join(", "))$. Reading each block of $K = #k$ variables yields the clustering $(#source-config.map(str).join(", "))$, so cluster 0 contains elements ${#source-config.enumerate().filter(((i, c)) => c == 0).map(((i, c)) => str(i)).join(", ")}$ and cluster 1 contains elements ${#source-config.enumerate().filter(((i, c)) => c == 1).map(((i, c)) => str(i)).join(", ")}$. The only within-cluster distances are $d(0,1) = #distances.at(0).at(1)$ and $d(2,3) = #distances.at(2).at(3)$, both at most $B$ #sym.checkmark.
15189+
15190+
*Multiplicity:* The fixture stores one canonical witness. Swapping the two cluster labels gives an equivalent second witness because the ILP distinguishes clusters only by index.
15191+
]
15192+
}
15193+
],
15194+
)[
15195+
This direct $O(n^2 K)$ ILP encoding#footnote[Standard ILP formulation of diameter-bounded clustering; no specific literature key is currently registered in `references.bib`.] introduces one binary variable $x_(i,c)$ for each element $i$ and cluster $c$, forces every element into exactly one cluster, and forbids every pair with $d(i,j) > B$ from sharing a cluster ($n K$ variables and at most $n + n^2 K$ constraints).
15196+
][
15197+
_Construction._ Given a Clustering instance on elements $X = {0, dots, n - 1}$ with cluster bound $K$ and diameter bound $B$, create binary variables $x_(i,c) in {0, 1}$ for every element $i in X$ and cluster $c in {0, dots, K - 1}$. Interpret $x_(i,c) = 1$ iff element $i$ is assigned to cluster $c$.
15198+
15199+
For every element $i$, add the assignment constraint $sum_(c=0)^(K-1) x_(i,c) = 1$. For every pair $i < j$ with $d(i,j) > B$ and every cluster $c$, add the conflict constraint $x_(i,c) + x_(j,c) <= 1$. Use the zero objective and minimize it, so the target is a pure feasibility ILP.
15200+
15201+
_Correctness._ ($arrow.r.double$) If the source instance has a feasible clustering, set $x_(i,c) = 1$ exactly for the cluster assigned to element $i$. Every element is assigned once, so all assignment equalities hold. Whenever $d(i,j) > B$, the source clustering never puts $i$ and $j$ together, so for every cluster $c$ at least one of $x_(i,c)$ or $x_(j,c)$ is 0 and every conflict inequality holds. ($arrow.l.double$) If the ILP is feasible, the assignment equalities choose exactly one cluster for each element. If some extracted cluster contained a pair $i, j$ with $d(i,j) > B$, then for that cluster $c$ we would have $x_(i,c) = x_(j,c) = 1$, contradicting the conflict inequality. Hence every extracted cluster has diameter at most $B$, so the extracted assignment is a feasible clustering using at most $K$ clusters.
15202+
15203+
_Variable mapping._ The implementation stores variable $x_(i,c)$ at index $i dot K + c$, i.e.\ consecutive blocks of $K$ variables per element.
15204+
15205+
_Solution extraction._ For each element $i$, scan the block $(x_(i,0), dots, x_(i,K-1))$ and return the unique cluster $c$ with value 1.
15206+
]
15207+
1516415208
// 5. PartitionIntoCliques → MinimumCoveringByCliques (#889)
1516515209
#let pic_mcbc = load-example("PartitionIntoCliques", "MinimumCoveringByCliques")
1516615210
#let pic_mcbc_sol = pic_mcbc.solutions.at(0)

src/rules/clustering_ilp.rs

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
//! Reduction from Clustering to ILP (Integer Linear Programming).
2+
//!
3+
//! Use one binary assignment variable `x_{i,c}` for each element `i` and
4+
//! cluster `c`. Equality constraints force every element into exactly one
5+
//! cluster, and conflict constraints forbid any pair with distance above the
6+
//! diameter bound from sharing a cluster.
7+
8+
use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
9+
use crate::models::misc::Clustering;
10+
use crate::reduction;
11+
use crate::rules::traits::{ReduceTo, ReductionResult};
12+
13+
/// Result of reducing Clustering to ILP.
14+
#[derive(Debug, Clone)]
15+
pub struct ReductionClusteringToILP {
16+
target: ILP<bool>,
17+
num_elements: usize,
18+
num_clusters: usize,
19+
}
20+
21+
impl ReductionClusteringToILP {
22+
fn var_index(&self, element: usize, cluster: usize) -> usize {
23+
element * self.num_clusters + cluster
24+
}
25+
}
26+
27+
impl ReductionResult for ReductionClusteringToILP {
28+
type Source = Clustering;
29+
type Target = ILP<bool>;
30+
31+
fn target_problem(&self) -> &Self::Target {
32+
&self.target
33+
}
34+
35+
fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
36+
(0..self.num_elements)
37+
.map(|element| {
38+
(0..self.num_clusters)
39+
.find(|&cluster| {
40+
let idx = self.var_index(element, cluster);
41+
idx < target_solution.len() && target_solution[idx] == 1
42+
})
43+
.unwrap_or(0)
44+
})
45+
.collect()
46+
}
47+
}
48+
49+
#[reduction(
50+
overhead = {
51+
num_vars = "num_elements * num_clusters",
52+
num_constraints = "num_elements + num_elements^2 * num_clusters",
53+
}
54+
)]
55+
impl ReduceTo<ILP<bool>> for Clustering {
56+
type Result = ReductionClusteringToILP;
57+
58+
fn reduce_to(&self) -> Self::Result {
59+
let num_elements = self.num_elements();
60+
let num_clusters = self.num_clusters();
61+
let num_vars = num_elements * num_clusters;
62+
let mut constraints = Vec::new();
63+
64+
let var_index =
65+
|element: usize, cluster: usize| -> usize { element * num_clusters + cluster };
66+
67+
for element in 0..num_elements {
68+
let terms: Vec<(usize, f64)> = (0..num_clusters)
69+
.map(|cluster| (var_index(element, cluster), 1.0))
70+
.collect();
71+
constraints.push(LinearConstraint::eq(terms, 1.0));
72+
}
73+
74+
let distances = self.distances();
75+
let diameter_bound = self.diameter_bound();
76+
for (i, row) in distances.iter().enumerate() {
77+
for (j, &distance) in row.iter().enumerate().skip(i + 1) {
78+
if distance > diameter_bound {
79+
for cluster in 0..num_clusters {
80+
constraints.push(LinearConstraint::le(
81+
vec![(var_index(i, cluster), 1.0), (var_index(j, cluster), 1.0)],
82+
1.0,
83+
));
84+
}
85+
}
86+
}
87+
}
88+
89+
ReductionClusteringToILP {
90+
target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize),
91+
num_elements,
92+
num_clusters,
93+
}
94+
}
95+
}
96+
97+
#[cfg(feature = "example-db")]
98+
pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
99+
use crate::export::SolutionPair;
100+
101+
vec![crate::example_db::specs::RuleExampleSpec {
102+
id: "clustering_to_ilp",
103+
build: || {
104+
let source = Clustering::new(
105+
vec![
106+
vec![0, 1, 3, 3],
107+
vec![1, 0, 3, 3],
108+
vec![3, 3, 0, 1],
109+
vec![3, 3, 1, 0],
110+
],
111+
2,
112+
1,
113+
);
114+
crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
115+
source,
116+
SolutionPair {
117+
source_config: vec![0, 0, 1, 1],
118+
target_config: vec![1, 0, 1, 0, 0, 1, 0, 1],
119+
},
120+
)
121+
},
122+
}]
123+
}
124+
125+
#[cfg(test)]
126+
#[path = "../unit_tests/rules/clustering_ilp.rs"]
127+
mod tests;
Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
//! Reduction from MinimumFaultDetectionTestSet to ILP.
2+
//!
3+
//! Each input-output pair becomes a binary decision variable. For every
4+
//! internal vertex, the ILP requires at least one selected pair whose coverage
5+
//! set contains that vertex. Minimizing the sum of the pair variables therefore
6+
//! recovers the minimum-size covering test set.
7+
8+
use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
9+
use crate::models::misc::MinimumFaultDetectionTestSet;
10+
use crate::reduction;
11+
use crate::rules::traits::{ReduceTo, ReductionResult};
12+
use std::collections::VecDeque;
13+
14+
/// Result of reducing MinimumFaultDetectionTestSet to ILP<bool>.
15+
#[derive(Debug, Clone)]
16+
pub struct ReductionMFDTSToILP {
17+
target: ILP<bool>,
18+
}
19+
20+
impl ReductionResult for ReductionMFDTSToILP {
21+
type Source = MinimumFaultDetectionTestSet;
22+
type Target = ILP<bool>;
23+
24+
fn target_problem(&self) -> &ILP<bool> {
25+
&self.target
26+
}
27+
28+
fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
29+
target_solution.to_vec()
30+
}
31+
}
32+
33+
#[reduction(overhead = {
34+
num_vars = "num_inputs * num_outputs",
35+
num_constraints = "num_vertices",
36+
})]
37+
impl ReduceTo<ILP<bool>> for MinimumFaultDetectionTestSet {
38+
type Result = ReductionMFDTSToILP;
39+
40+
fn reduce_to(&self) -> Self::Result {
41+
fn reachable(adj: &[Vec<usize>], start: usize) -> Vec<bool> {
42+
let mut seen = vec![false; adj.len()];
43+
let mut queue = VecDeque::new();
44+
seen[start] = true;
45+
queue.push_back(start);
46+
47+
while let Some(vertex) = queue.pop_front() {
48+
for &next in &adj[vertex] {
49+
if !seen[next] {
50+
seen[next] = true;
51+
queue.push_back(next);
52+
}
53+
}
54+
}
55+
56+
seen
57+
}
58+
59+
let mut adj = vec![Vec::new(); self.num_vertices()];
60+
let mut rev_adj = vec![Vec::new(); self.num_vertices()];
61+
for &(tail, head) in self.arcs() {
62+
adj[tail].push(head);
63+
rev_adj[head].push(tail);
64+
}
65+
66+
let input_reachability: Vec<Vec<bool>> = self
67+
.inputs()
68+
.iter()
69+
.map(|&input| reachable(&adj, input))
70+
.collect();
71+
let output_reachability: Vec<Vec<bool>> = self
72+
.outputs()
73+
.iter()
74+
.map(|&output| reachable(&rev_adj, output))
75+
.collect();
76+
77+
let mut boundary = vec![false; self.num_vertices()];
78+
for &input in self.inputs() {
79+
boundary[input] = true;
80+
}
81+
for &output in self.outputs() {
82+
boundary[output] = true;
83+
}
84+
85+
let num_pairs = self.num_inputs() * self.num_outputs();
86+
let internal_vertices: Vec<usize> = (0..self.num_vertices())
87+
.filter(|&vertex| !boundary[vertex])
88+
.collect();
89+
90+
let constraints: Vec<LinearConstraint> = internal_vertices
91+
.into_iter()
92+
.map(|vertex| {
93+
let mut terms = Vec::new();
94+
for (input_idx, input_cov) in input_reachability.iter().enumerate() {
95+
for (output_idx, output_cov) in output_reachability.iter().enumerate() {
96+
if input_cov[vertex] && output_cov[vertex] {
97+
let pair_idx = input_idx * self.num_outputs() + output_idx;
98+
terms.push((pair_idx, 1.0));
99+
}
100+
}
101+
}
102+
LinearConstraint::ge(terms, 1.0)
103+
})
104+
.collect();
105+
106+
let objective = (0..num_pairs).map(|pair_idx| (pair_idx, 1.0)).collect();
107+
108+
ReductionMFDTSToILP {
109+
target: ILP::new(num_pairs, constraints, objective, ObjectiveSense::Minimize),
110+
}
111+
}
112+
}
113+
114+
#[cfg(feature = "example-db")]
115+
pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
116+
vec![crate::example_db::specs::RuleExampleSpec {
117+
id: "minimumfaultdetectiontestset_to_ilp",
118+
build: || {
119+
let source = MinimumFaultDetectionTestSet::new(
120+
7,
121+
vec![
122+
(0, 2),
123+
(0, 3),
124+
(1, 3),
125+
(1, 4),
126+
(2, 5),
127+
(3, 5),
128+
(3, 6),
129+
(4, 6),
130+
],
131+
vec![0, 1],
132+
vec![5, 6],
133+
);
134+
crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
135+
},
136+
}]
137+
}
138+
139+
#[cfg(test)]
140+
#[path = "../unit_tests/rules/minimumfaultdetectiontestset_ilp.rs"]
141+
mod tests;

src/rules/mod.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,8 @@ pub(crate) mod capacityassignment_ilp;
164164
#[cfg(feature = "ilp-solver")]
165165
pub(crate) mod circuit_ilp;
166166
#[cfg(feature = "ilp-solver")]
167+
pub(crate) mod clustering_ilp;
168+
#[cfg(feature = "ilp-solver")]
167169
pub(crate) mod coloring_ilp;
168170
#[cfg(feature = "ilp-solver")]
169171
pub(crate) mod consecutiveblockminimization_ilp;
@@ -248,6 +250,8 @@ pub(crate) mod minimumedgecostflow_ilp;
248250
#[cfg(feature = "ilp-solver")]
249251
pub(crate) mod minimumexternalmacrodatacompression_ilp;
250252
#[cfg(feature = "ilp-solver")]
253+
pub(crate) mod minimumfaultdetectiontestset_ilp;
254+
#[cfg(feature = "ilp-solver")]
251255
pub(crate) mod minimumfeedbackarcset_ilp;
252256
#[cfg(feature = "ilp-solver")]
253257
pub(crate) mod minimumfeedbackvertexset_ilp;
@@ -531,6 +535,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
531535
specs.extend(boundedcomponentspanningforest_ilp::canonical_rule_example_specs());
532536
specs.extend(capacityassignment_ilp::canonical_rule_example_specs());
533537
specs.extend(circuit_ilp::canonical_rule_example_specs());
538+
specs.extend(clustering_ilp::canonical_rule_example_specs());
534539
specs.extend(coloring_ilp::canonical_rule_example_specs());
535540
specs.extend(consecutiveblockminimization_ilp::canonical_rule_example_specs());
536541
specs.extend(consecutiveonesmatrixaugmentation_ilp::canonical_rule_example_specs());
@@ -574,6 +579,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
574579
specs.extend(minimumcoveringbycliques_ilp::canonical_rule_example_specs());
575580
specs.extend(minimumedgecostflow_ilp::canonical_rule_example_specs());
576581
specs.extend(minimumexternalmacrodatacompression_ilp::canonical_rule_example_specs());
582+
specs.extend(minimumfaultdetectiontestset_ilp::canonical_rule_example_specs());
577583
specs.extend(minimuminternalmacrodatacompression_ilp::canonical_rule_example_specs());
578584
specs.extend(minimumfeedbackarcset_ilp::canonical_rule_example_specs());
579585
specs.extend(minimumfeedbackvertexset_ilp::canonical_rule_example_specs());

src/unit_tests/reduction_graph.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
//! Tests for ReductionGraph: discovery, path finding, and typed API.
22
3+
#[cfg(feature = "ilp-solver")]
4+
use crate::models::algebraic::ILP;
35
use crate::models::decision::Decision;
46
use crate::models::formula::KSatisfiability;
57
use crate::models::misc::Clustering;
@@ -39,6 +41,14 @@ fn test_reduction_graph_discovers_k3coloring_to_clustering() {
3941
assert!(graph.has_direct_reduction::<KColoring<K3, SimpleGraph>, Clustering>());
4042
}
4143

44+
#[cfg(feature = "ilp-solver")]
45+
#[test]
46+
fn test_reduction_graph_discovers_clustering_to_ilp() {
47+
let graph = ReductionGraph::new();
48+
49+
assert!(graph.has_direct_reduction::<Clustering, ILP<bool>>());
50+
}
51+
4252
// ---- Path finding (by name) ----
4353

4454
#[test]

0 commit comments

Comments
 (0)