Skip to content

Commit f65dc61

Browse files
isPANNclaude
andcommitted
Fix nits: ExactCoverBy3Sets -> BoundedDiameterSpanningTree (#913)
- Add `q()` helper on ExactCoverBy3Sets and use it in the rule and tests instead of recomputing `universe_size / 3`. - Add a `debug_assert!` in `reduce_to` confirming that root-to-set edges occupy indices 2..2+m, so a future reordering will surface a failure in `extract_solution`. - Simplify the `no_instance` test: drop the duplicate assertion and the `unwrap_or_default` fallback; assert directly that `find_witness` is `None` and that the brute-force aggregate is `Or(false)` for an infeasible Or-valued target. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
1 parent 5f348a8 commit f65dc61

3 files changed

Lines changed: 25 additions & 16 deletions

File tree

src/models/set/exact_cover_by_3_sets.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,14 @@ impl ExactCoverBy3Sets {
109109
self.subsets.len()
110110
}
111111

112+
/// Get q = universe_size / 3, the number of subsets in any exact cover.
113+
///
114+
/// `ExactCoverBy3Sets::new` enforces `universe_size % 3 == 0`, so this
115+
/// division is always exact.
116+
pub fn q(&self) -> usize {
117+
self.universe_size / 3
118+
}
119+
112120
/// Get the number of sets in the collection.
113121
pub fn num_sets(&self) -> usize {
114122
self.num_subsets()

src/rules/exactcoverby3sets_boundeddiameterspanningtree.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ impl ReduceTo<BoundedDiameterSpanningTree<SimpleGraph, i32>> for ExactCoverBy3Se
8787
fn reduce_to(&self) -> Self::Result {
8888
let universe_size = self.universe_size();
8989
let m = self.num_subsets();
90-
let q = universe_size / 3;
90+
let q = self.q();
9191

9292
// Vertex indexing matches the docstring.
9393
let s_index = |i: usize| 3 + i;
@@ -108,6 +108,13 @@ impl ReduceTo<BoundedDiameterSpanningTree<SimpleGraph, i32>> for ExactCoverBy3Se
108108
edges.push((0, s_index(i)));
109109
weights.push(2);
110110
}
111+
// Invariant: extract_solution reads edges[2..2 + m] to recover the
112+
// selected subsets. If this loop is ever reordered or moved, the
113+
// extractor must be updated to match.
114+
debug_assert!(
115+
(0..m).all(|i| edges[2 + i] == (0, s_index(i))),
116+
"root-to-set edges must occupy indices 2..2+m for extract_solution to work"
117+
);
111118

112119
// Set-to-element edges. Subsets are already sorted in `ExactCoverBy3Sets::new`.
113120
for (i, subset) in self.subsets().iter().enumerate() {

src/unit_tests/rules/exactcoverby3sets_boundeddiameterspanningtree.rs

Lines changed: 9 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
use super::*;
22
use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target;
3-
use crate::solvers::BruteForce;
3+
use crate::solvers::{BruteForce, Solver};
44
use crate::topology::Graph;
5-
use crate::traits::Problem;
65
use crate::types::Or;
76

87
/// q = 2, m = 2: X = {0..5} with C = [{0,1,2}, {3,4,5}].
@@ -36,7 +35,7 @@ fn test_exactcoverby3sets_to_boundeddiameterspanningtree_structure() {
3635
let target = reduction.target_problem();
3736

3837
let m = source.num_subsets();
39-
let q = source.universe_size() / 3;
38+
let q = source.q();
4039
// n = 3 + m + 3q
4140
assert_eq!(target.num_vertices(), 3 + m + source.universe_size());
4241
// Expected edge count: 2 forced + m root-to-set + 3m set-to-element + m(m-1)/2 clique.
@@ -91,16 +90,11 @@ fn test_exactcoverby3sets_to_boundeddiameterspanningtree_no_instance() {
9190
let target = reduction.target_problem();
9291

9392
// The target should be infeasible: no spanning tree satisfies both weight
94-
// bound B = 4q + m + 2 = 12 and diameter bound D = 4.
95-
let witness = BruteForce::new().find_witness(target);
96-
assert_eq!(
97-
target.evaluate(&witness.clone().unwrap_or_default()),
98-
Or(false)
99-
);
100-
// BruteForce::find_witness returns the lexicographically-first optimal
101-
// assignment; for an Or-valued infeasible target, even that witness
102-
// evaluates to false.
103-
if let Some(w) = witness {
104-
assert!(!target.evaluate(&w).0);
105-
}
93+
// bound B = 4q + m + 2 = 12 and diameter bound D = 4. For an Or-valued
94+
// problem with no satisfying configuration, BruteForce::find_witness
95+
// returns None (witnesses are configs that evaluate to Or(true), and none
96+
// exist here). Equivalently, the brute-force aggregate evaluates to
97+
// Or(false).
98+
assert!(BruteForce::new().find_witness(target).is_none());
99+
assert_eq!(BruteForce::new().solve(target), Or(false));
106100
}

0 commit comments

Comments
 (0)