From af1497eed070f0106e988e687bf64f4bd7a156af Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 16:38:47 +0800 Subject: [PATCH 1/6] Add plan for #416: [Model] SparseMatrixCompression --- ...6-03-22-sparse-matrix-compression-model.md | 351 ++++++++++++++++++ 1 file changed, 351 insertions(+) create mode 100644 docs/plans/2026-03-22-sparse-matrix-compression-model.md diff --git a/docs/plans/2026-03-22-sparse-matrix-compression-model.md b/docs/plans/2026-03-22-sparse-matrix-compression-model.md new file mode 100644 index 000000000..14c2c1cf7 --- /dev/null +++ b/docs/plans/2026-03-22-sparse-matrix-compression-model.md @@ -0,0 +1,351 @@ +# Sparse Matrix Compression Implementation Plan + +> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. + +**Goal:** Implement `SparseMatrixCompression` as a new algebraic satisfaction model, register it for CLI/example-db/paper workflows, and preserve the issue's verified `4 x 4`, `K = 2` example and complexity metadata. + +**Architecture:** Represent configurations as row-shift assignments only, one variable per matrix row with domain `0..bound_k-1`. `evaluate()` should build the implied storage vector internally and reject configurations whose shifted supports collide. This keeps brute-force search at `bound_k ^ num_rows`, matching the issue and avoiding a much larger search space from enumerating storage-vector entries explicitly. Batch 1 delivers code, tests, registry wiring, CLI creation, and the canonical example. Batch 2 adds the paper entry after the example fixture is available. + +**Tech Stack:** Rust workspace, serde, inventory registry, `pred` CLI, Typst paper + +--- + +## Issue Packet + +| Item | Decision | +|---|---| +| Issue | `#416` — `[Model] SparseMatrixCompression` | +| Repo skill | `.claude/skills/add-model/SKILL.md` | +| Category | `src/models/algebraic/` | +| Problem type | Satisfaction (`Metric = bool`) | +| Type parameters | None | +| Core fields | `matrix: Vec>`, `bound_k: usize` | +| Search space | `vec![bound_k; num_rows]` | +| Complexity string | `"(bound_k ^ num_rows) * num_rows * num_cols"` | +| Solver strategy for this PR | Brute-force over row shifts only | +| Associated rule | `Graph 3-Colorability -> SparseMatrixCompression` (issue crossref `R107`) | +| Important issue comments | Preserve the fixed approximation note, concrete complexity string, and the clean unique-solution example from the `/fix-issue` changelog | + +## Batch Layout + +- **Batch 1:** add model code, tests, registry/module wiring, canonical example, and CLI creation/help. +- **Batch 2:** add the paper `problem-def(...)` entry after Batch 1 is green. + +## Design Notes + +- The mathematical definition mentions both row shifts `s(i)` and storage-vector entries `b_j`, but the implementation should not enumerate `b_j` in `dims()`. Instead, it should construct the unique implied storage vector for a chosen shift assignment and check whether every `1` lands on an empty slot or the same row label. +- Use zero-based config values for solver compatibility. The issue's satisfying shift assignment `s = (2, 2, 2, 1)` should therefore appear in code as config `[1, 1, 1, 0]`. +- Keep the storage vector representation explicit in helper methods and tests because the issue's expected outcome includes `b = (4, 1, 2, 3, 1, 0)`. +- Do **not** add an ILP reduction in this PR. The issue already supplies a valid brute-force solver path, and this PR should stay a model-only change. + +### Task 1: Lock Down Model Behavior with Failing Tests + +**Files:** +- Create: `src/unit_tests/models/algebraic/sparse_matrix_compression.rs` +- Modify: `problemreductions-cli/src/commands/create.rs` + +**Step 1: Write the failing model tests** + +Add a new unit test file for the exact issue example matrix: + +```rust +fn issue_example_matrix() -> Vec> { + vec![ + vec![true, false, false, true], + vec![false, true, false, false], + vec![false, false, true, false], + vec![true, false, false, false], + ] +} +``` + +Cover these behaviors: +- constructor/getters: `num_rows() == 4`, `num_cols() == 4`, `bound_k() == 2`, `storage_len() == 6`, `dims() == vec![2; 4]` +- satisfying config: `[1, 1, 1, 0]` evaluates to `true` +- implied storage vector: `[1, 1, 1, 0]` produces `vec![4, 1, 2, 3, 1, 0]` +- unsatisfying configs from the issue: `[0, 0, 0, 0]`, `[0, 1, 1, 1]`, `[1, 1, 1, 1]` +- brute-force uniqueness: exactly one satisfying config, and it is `[1, 1, 1, 0]` +- serde shape: JSON uses `matrix` and `bound_k` +- metadata check: registry complexity string is `"(bound_k ^ num_rows) * num_rows * num_cols"` +- constructor guards: ragged rows panic; `bound_k == 0` panics + +**Step 2: Run the model tests to verify they fail** + +Run: + +```bash +cargo test sparse_matrix_compression --lib +``` + +Expected: FAIL because the model file and registrations do not exist yet. + +**Step 3: Write the failing CLI creation test** + +In `problemreductions-cli/src/commands/create.rs`, add a focused test that creates the issue example via CLI: + +```rust +#[test] +fn test_create_sparse_matrix_compression_json() { /* parse --matrix and --bound */ } +``` + +Assert: +- output `type == "SparseMatrixCompression"` +- serialized data contains the `4 x 4` matrix +- serialized `bound_k == 2` + +Also add one negative test that omits `--bound` and confirms the usage message mentions `SparseMatrixCompression requires --matrix and --bound`. + +**Step 4: Run the CLI tests to verify they fail** + +Run: + +```bash +cargo test -p problemreductions-cli sparse_matrix_compression +``` + +Expected: FAIL because the CLI arm/import/help text do not exist yet. + +### Task 2: Implement the Model and Registry Wiring + +**Files:** +- Create: `src/models/algebraic/sparse_matrix_compression.rs` +- Modify: `src/models/algebraic/mod.rs` +- Modify: `src/models/mod.rs` +- Modify: `src/lib.rs` + +**Step 1: Write the minimal model implementation** + +Create `src/models/algebraic/sparse_matrix_compression.rs` with: +- `inventory::submit!` `ProblemSchemaEntry` +- `#[derive(Debug, Clone, Serialize, Deserialize)]` +- constructor `new(matrix, bound_k)` with rectangular-row and positive-`bound_k` checks +- getters: `matrix()`, `bound_k()`, `num_rows()`, `num_cols()`, `storage_len()` +- helper(s): + - `decode_shifts(config) -> Option>` or equivalent + - `storage_vector(config) -> Option>` that returns the implied `b` vector when the overlay is valid +- `Problem` impl: + - `NAME = "SparseMatrixCompression"` + - `Metric = bool` + - `dims() = vec![self.bound_k; self.num_rows()]` + - `evaluate(config)` returns `self.storage_vector(config).is_some()` + - `variant() = crate::variant_params![]` +- `SatisfactionProblem` impl +- `declare_variants!`: + +```rust +crate::declare_variants! { + default sat SparseMatrixCompression => "(bound_k ^ num_rows) * num_rows * num_cols", +} +``` + +- `#[cfg(feature = "example-db")] canonical_model_example_specs()` using the issue's fixed example and `optimal_config: vec![1, 1, 1, 0]` +- test link: + +```rust +#[cfg(test)] +#[path = "../../unit_tests/models/algebraic/sparse_matrix_compression.rs"] +mod tests; +``` + +**Step 2: Register the model** + +Update: +- `src/models/algebraic/mod.rs` + - add module + public re-export + - extend `canonical_model_example_specs()` with `sparse_matrix_compression::canonical_model_example_specs()` +- `src/models/mod.rs` + - add `SparseMatrixCompression` to the algebraic re-export list +- `src/lib.rs` + - add `SparseMatrixCompression` to `prelude` + +**Step 3: Run the model tests again** + +Run: + +```bash +cargo test sparse_matrix_compression --lib +``` + +Expected: the new model tests pass, or fail only on CLI/paper gaps not yet implemented. + +**Step 4: Commit the model slice** + +```bash +git add src/models/algebraic/sparse_matrix_compression.rs \ + src/models/algebraic/mod.rs \ + src/models/mod.rs \ + src/lib.rs \ + src/unit_tests/models/algebraic/sparse_matrix_compression.rs +git commit -m "Add SparseMatrixCompression model" +``` + +### Task 3: Wire CLI Creation and Help + +**Files:** +- Modify: `problemreductions-cli/src/commands/create.rs` +- Modify: `problemreductions-cli/src/cli.rs` + +**Step 1: Implement the CLI create arm** + +In `problemreductions-cli/src/commands/create.rs`: +- import `SparseMatrixCompression` +- add `example_for("SparseMatrixCompression")` +- add a `help_flag_name()` override so schema field `bound_k` maps to CLI flag `--bound` +- add a `help_flag_hint()` override so `matrix` is documented as semicolon-separated `0/1` rows +- add a `"SparseMatrixCompression"` create arm that: + - uses `parse_bool_matrix(args)?` + - requires `--bound` + - converts `bound` to `usize` + - serializes `SparseMatrixCompression::new(matrix, bound)` + +Use this usage string: + +```text +Usage: pred create SparseMatrixCompression --matrix "1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0" --bound 2 +``` + +**Step 2: Update top-level CLI help** + +In `problemreductions-cli/src/cli.rs`, add: + +```text +SparseMatrixCompression --matrix (0/1), --bound +``` + +to the "Flags by problem type" table. + +**Step 3: Re-run the targeted CLI tests** + +Run: + +```bash +cargo test -p problemreductions-cli sparse_matrix_compression +``` + +Expected: the new create tests pass. + +**Step 4: Commit the CLI slice** + +```bash +git add problemreductions-cli/src/commands/create.rs problemreductions-cli/src/cli.rs +git commit -m "Add CLI support for SparseMatrixCompression" +``` + +### Task 4: Verify Batch 1 End-to-End + +**Files:** +- Reference: `src/models/algebraic/sparse_matrix_compression.rs` +- Reference: `src/unit_tests/models/algebraic/sparse_matrix_compression.rs` +- Reference: `problemreductions-cli/src/commands/create.rs` + +**Step 1: Run focused verification** + +Run: + +```bash +cargo test sparse_matrix_compression --lib +cargo test -p problemreductions-cli sparse_matrix_compression +``` + +Expected: PASS. + +**Step 2: Run project verification for code changes** + +Run: + +```bash +make test clippy +``` + +Expected: PASS. + +**Step 3: Inspect the canonical example through the CLI** + +Run: + +```bash +pred create --example SparseMatrixCompression -o /tmp/smc-example.json +pred evaluate /tmp/smc-example.json --config 1,1,1,0 +pred solve /tmp/smc-example.json +``` + +Expected: +- example JSON matches the issue matrix and `bound_k = 2` +- `pred evaluate` returns `true` +- `pred solve` finds the unique satisfying config + +### Task 5: Add the Paper Entry (Batch 2) + +**Files:** +- Modify: `docs/paper/reductions.typ` + +**Step 1: Write the paper entry after code is green** + +Add a display-name entry: + +```typst +"SparseMatrixCompression": [Sparse Matrix Compression], +``` + +Add a `#problem-def("SparseMatrixCompression")[...][...]` block that: +- states the formal row-overlay definition +- explains that the implementation searches over shifts and reconstructs the storage vector internally +- cites the Garey & Johnson catalog entry and the practical DFA/parser-table motivation +- uses `load-model-example("SparseMatrixCompression")` +- explains that stored config `[1, 1, 1, 0]` encodes shifts `(2, 2, 2, 1)` +- shows the resulting storage vector `(4, 1, 2, 3, 1, 0)` +- states that the fixture has exactly one satisfying shift assignment +- includes a `pred-commands(...)` block derived from the loaded example + +**Step 2: Build the paper** + +Run: + +```bash +make paper +``` + +Expected: PASS. + +**Step 3: Re-run final repo verification** + +Run: + +```bash +make test clippy +``` + +Expected: PASS. + +**Step 4: Commit the documentation slice** + +```bash +git add docs/paper/reductions.typ +git commit -m "Document SparseMatrixCompression" +``` + +### Task 6: Final Push and Cleanup + +**Files:** +- Modify: `docs/plans/2026-03-22-sparse-matrix-compression-model.md` (remove at the end per pipeline workflow) + +**Step 1: Summarize deviations before push** + +Record whether any of these changed during implementation: +- field names (`bound_k` vs `bound`) +- helper method names +- exact paper example wording + +**Step 2: Push implementation commits** + +```bash +git push +``` + +**Step 3: Remove the plan file after implementation** + +```bash +git rm docs/plans/2026-03-22-sparse-matrix-compression-model.md +git commit -m "chore: remove plan file after implementation" +git push +``` From a5822bdadec4e5db9ebaf85965faf5868ebb2261 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 16:50:07 +0800 Subject: [PATCH 2/6] Implement #416: [Model] SparseMatrixCompression --- docs/paper/reductions.typ | 105 +++++++++++ problemreductions-cli/src/cli.rs | 1 + problemreductions-cli/src/commands/create.rs | 82 +++++++- src/lib.rs | 2 +- src/models/algebraic/mod.rs | 4 + .../algebraic/sparse_matrix_compression.rs | 175 ++++++++++++++++++ src/models/mod.rs | 2 +- .../algebraic/sparse_matrix_compression.rs | 122 ++++++++++++ src/unit_tests/registry/problem_type.rs | 7 + 9 files changed, 497 insertions(+), 3 deletions(-) create mode 100644 src/models/algebraic/sparse_matrix_compression.rs create mode 100644 src/unit_tests/models/algebraic/sparse_matrix_compression.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index eba813fd8..97a032e73 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -135,6 +135,7 @@ "ConjunctiveBooleanQuery": [Conjunctive Boolean Query], "ConsecutiveBlockMinimization": [Consecutive Block Minimization], "ConsecutiveOnesSubmatrix": [Consecutive Ones Submatrix], + "SparseMatrixCompression": [Sparse Matrix Compression], "DirectedTwoCommodityIntegralFlow": [Directed Two-Commodity Integral Flow], "IntegralFlowHomologousArcs": [Integral Flow with Homologous Arcs], "IntegralFlowWithMultipliers": [Integral Flow With Multipliers], @@ -5900,6 +5901,110 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], ] } +#{ + let x = load-model-example("SparseMatrixCompression") + let A = x.instance.matrix + let m = A.len() + let n = if m > 0 { A.at(0).len() } else { 0 } + let K = x.instance.bound_k + let cfg = x.optimal_config + let shifts = cfg.map(v => v + 1) + let storage = (4, 1, 2, 3, 1, 0) + let A-int = A.map(row => row.map(v => if v { 1 } else { 0 })) + let row-colors = ( + graph-colors.at(0), + rgb("#f28e2b"), + rgb("#76b7b2"), + rgb("#e15759"), + ) + [ + #problem-def("SparseMatrixCompression")[ + Given an $m times n$ binary matrix $A$ and a positive integer $K$, determine whether there exist a shift function $s: \{1, dots, m\} -> \{1, dots, K\}$ and a storage vector $b in \{0, 1, dots, m\}^{n + K}$ such that, for every row $i$ and column $j$, $A_(i j) = 1$ if and only if $b_(s(i) + j - 1) = i$. + ][ + Sparse Matrix Compression appears as problem SR13 in Garey and Johnson @garey1979. It models row-overlay compression for sparse lookup tables: rows may share storage positions only when their shifted 1-entries never demand different row labels from the same slot. The implementation in this crate searches over row shifts only, then reconstructs the implied storage vector internally. This yields the direct exact bound $O(K^m dot m dot n)$ for $m$ rows and $n$ columns.#footnote[The storage vector is not enumerated as part of the configuration space. Once the shifts are fixed, every occupied slot is forced by the 1-entries of the shifted rows.] + + *Example.* Let $A = mat(#A-int.map(row => row.map(v => str(v)).join(", ")).join("; "))$ and $K = #K$. The stored config $(#cfg.map(str).join(", "))$ encodes the one-based shifts $s = (#shifts.map(str).join(", "))$. These shifts place the four row supports at positions $\{2, 5\}$, $\{3\}$, $\{4\}$, and $\{1\}$ respectively, so the supports are pairwise disjoint. The implied overlay vector is therefore $b = (#storage.map(str).join(", "))$, and this is the unique satisfying shift assignment among the $2^4 = 16$ configs in the canonical fixture. + + #pred-commands( + "pred create --example " + problem-spec(x) + " -o sparse-matrix-compression.json", + "pred solve sparse-matrix-compression.json", + "pred evaluate sparse-matrix-compression.json --config " + x.optimal_config.map(str).join(","), + ) + + #figure( + canvas(length: 0.7cm, { + import draw: * + let cell-size = 0.9 + let gap = 0.08 + let storage-x = 6.2 + + for i in range(m) { + for j in range(n) { + let val = A-int.at(i).at(j) + let fill = if val == 1 { + row-colors.at(i).transparentize(30%) + } else { + white + } + rect( + (j * cell-size, -i * cell-size), + (j * cell-size + cell-size - gap, -i * cell-size - cell-size + gap), + fill: fill, + stroke: 0.3pt + luma(180), + ) + content( + (j * cell-size + (cell-size - gap) / 2, -i * cell-size - (cell-size - gap) / 2), + text(8pt, str(val)), + ) + } + content( + (-0.55, -i * cell-size - (cell-size - gap) / 2), + text(7pt)[$r_#(i + 1)$], + ) + content( + (4.6, -i * cell-size - (cell-size - gap) / 2), + text(7pt)[$s_#(i + 1) = #shifts.at(i)$], + ) + } + + for j in range(n) { + content( + (j * cell-size + (cell-size - gap) / 2, 0.45), + text(7pt)[$c_#(j + 1)$], + ) + } + + content((5.45, -1.35), text(8pt, weight: "bold")[overlay]) + + for j in range(storage.len()) { + let label = storage.at(j) + let fill = if label == 0 { + white + } else { + row-colors.at(label - 1).transparentize(30%) + } + rect( + (storage-x + j * cell-size, -1.5 * cell-size), + (storage-x + j * cell-size + cell-size - gap, -2.5 * cell-size + gap), + fill: fill, + stroke: 0.3pt + luma(180), + ) + content( + (storage-x + j * cell-size + (cell-size - gap) / 2, -2.0 * cell-size + gap / 2), + text(8pt, str(label)), + ) + content( + (storage-x + j * cell-size + (cell-size - gap) / 2, -0.8 * cell-size), + text(7pt)[$b_#(j + 1)$], + ) + } + }), + caption: [Canonical Sparse Matrix Compression YES instance. Row-colored 1-entries on the left are shifted into the overlay vector on the right, producing $b = (4, 1, 2, 3, 1, 0)$.], + ) + ] + ] +} + // Completeness check: warn about problem types in JSON but missing from paper #{ let json-models = { diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index 4fe588faa..39341f047 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -265,6 +265,7 @@ Flags by problem type: BMF --matrix (0/1), --rank ConsecutiveBlockMinimization --matrix (JSON 2D bool), --bound-k ConsecutiveOnesSubmatrix --matrix (0/1), --k + SparseMatrixCompression --matrix (0/1), --bound SteinerTree --graph, --edge-weights, --terminals MultipleCopyFileAllocation --graph, --usage, --storage, --bound AcyclicPartition --arcs [--weights] [--arc-costs] --weight-bound --cost-bound [--num-vertices] diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 005fbc713..ff8f5c6a2 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -8,7 +8,8 @@ use crate::util; use anyhow::{bail, Context, Result}; use problemreductions::export::{ModelExample, ProblemRef, ProblemSide, RuleExample}; use problemreductions::models::algebraic::{ - ClosestVectorProblem, ConsecutiveBlockMinimization, ConsecutiveOnesSubmatrix, BMF, + ClosestVectorProblem, ConsecutiveBlockMinimization, ConsecutiveOnesSubmatrix, + SparseMatrixCompression, BMF, }; use problemreductions::models::formula::Quantifier; use problemreductions::models::graph::{ @@ -668,6 +669,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str { "ConsecutiveBlockMinimization" => { "--matrix '[[true,false,true],[false,true,true]]' --bound 2" } + "SparseMatrixCompression" => { + "--matrix \"1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0\" --bound 2" + } "ConjunctiveBooleanQuery" => { "--domain-size 6 --relations \"2:0,3|1,3|2,4;3:0,1,5|1,2,5\" --conjuncts-spec \"0:v0,c3;0:v1,c3;1:v0,v1,c5\"" } @@ -712,6 +716,7 @@ fn help_flag_name(canonical: &str, field_name: &str) -> String { ("PrimeAttributeName", "query_attribute") => return "query".to_string(), ("MixedChinesePostman", "arc_weights") => return "arc-costs".to_string(), ("ConsecutiveOnesSubmatrix", "bound") => return "bound".to_string(), + ("SparseMatrixCompression", "bound_k") => return "bound".to_string(), ("StackerCrane", "edges") => return "graph".to_string(), ("StackerCrane", "arc_lengths") => return "arc-costs".to_string(), ("StackerCrane", "edge_lengths") => return "edge-lengths".to_string(), @@ -796,6 +801,7 @@ fn help_flag_hint( "semicolon-separated arc-index paths: \"0,2,5,8;1,4,7,9\"" } ("ConsecutiveOnesSubmatrix", "matrix") => "semicolon-separated 0/1 rows: \"1,0;0,1\"", + ("SparseMatrixCompression", "matrix") => "semicolon-separated 0/1 rows: \"1,0;0,1\"", ("TimetableDesign", "craftsman_avail") | ("TimetableDesign", "task_avail") => { "semicolon-separated 0/1 rows: \"1,1,0;0,1,1\"" } @@ -2684,6 +2690,22 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { ) } + // SparseMatrixCompression + "SparseMatrixCompression" => { + let matrix = parse_bool_matrix(args)?; + let usage = "Usage: pred create SparseMatrixCompression --matrix \"1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0\" --bound 2"; + let bound = args.bound.ok_or_else(|| { + anyhow::anyhow!( + "SparseMatrixCompression requires --matrix and --bound\n\n{usage}" + ) + })?; + let bound = parse_nonnegative_usize_bound(bound, "SparseMatrixCompression", usage)?; + ( + ser(SparseMatrixCompression::new(matrix, bound))?, + resolved_variant.clone(), + ) + } + // LongestCommonSubsequence "LongestCommonSubsequence" => { let usage = @@ -7290,4 +7312,62 @@ mod tests { "unexpected error: {err}" ); } + + #[test] + fn test_create_sparse_matrix_compression_json() { + use crate::dispatch::ProblemJsonOutput; + + let mut args = empty_args(); + args.problem = Some("SparseMatrixCompression".to_string()); + args.matrix = Some("1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0".to_string()); + args.bound = Some(2); + + let output_path = std::env::temp_dir() + .join(format!("smc-create-{}.json", std::process::id())); + let out = OutputConfig { + output: Some(output_path.clone()), + quiet: true, + json: false, + auto_json: false, + }; + + create(&args, &out).unwrap(); + + let json = std::fs::read_to_string(&output_path).unwrap(); + let created: ProblemJsonOutput = serde_json::from_str(&json).unwrap(); + assert_eq!(created.problem_type, "SparseMatrixCompression"); + assert!(created.variant.is_empty()); + assert_eq!( + created.data, + serde_json::json!({ + "matrix": [ + [true, false, false, true], + [false, true, false, false], + [false, false, true, false], + [true, false, false, false], + ], + "bound_k": 2, + }) + ); + + let _ = std::fs::remove_file(output_path); + } + + #[test] + fn test_create_sparse_matrix_compression_requires_bound() { + let mut args = empty_args(); + args.problem = Some("SparseMatrixCompression".to_string()); + args.matrix = Some("1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0".to_string()); + + let out = OutputConfig { + output: None, + quiet: true, + json: false, + auto_json: false, + }; + + let err = create(&args, &out).unwrap_err().to_string(); + assert!(err.contains("SparseMatrixCompression requires --matrix and --bound")); + assert!(err.contains("Usage: pred create SparseMatrixCompression")); + } } diff --git a/src/lib.rs b/src/lib.rs index 458193d8d..c74729d95 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -42,7 +42,7 @@ pub mod variant; /// Prelude module for convenient imports. pub mod prelude { // Problem types - pub use crate::models::algebraic::{QuadraticAssignment, BMF, QUBO}; + pub use crate::models::algebraic::{QuadraticAssignment, SparseMatrixCompression, BMF, QUBO}; pub use crate::models::formula::{ CNFClause, CircuitSAT, KSatisfiability, NAESatisfiability, QuantifiedBooleanFormulas, Satisfiability, diff --git a/src/models/algebraic/mod.rs b/src/models/algebraic/mod.rs index e375ab814..f5aaff91e 100644 --- a/src/models/algebraic/mod.rs +++ b/src/models/algebraic/mod.rs @@ -8,6 +8,7 @@ //! - [`ConsecutiveBlockMinimization`]: Consecutive Block Minimization //! - [`ConsecutiveOnesSubmatrix`]: Consecutive Ones Submatrix (column selection with C1P) //! - [`QuadraticAssignment`]: Quadratic Assignment Problem +//! - [`SparseMatrixCompression`]: Sparse Matrix Compression by row overlay pub(crate) mod bmf; pub(crate) mod closest_vector_problem; @@ -16,6 +17,7 @@ pub(crate) mod consecutive_ones_submatrix; pub(crate) mod ilp; pub(crate) mod quadratic_assignment; pub(crate) mod qubo; +pub(crate) mod sparse_matrix_compression; pub use bmf::BMF; pub use closest_vector_problem::{ClosestVectorProblem, VarBounds}; @@ -24,6 +26,7 @@ pub use consecutive_ones_submatrix::ConsecutiveOnesSubmatrix; pub use ilp::{Comparison, LinearConstraint, ObjectiveSense, VariableDomain, ILP}; pub use quadratic_assignment::QuadraticAssignment; pub use qubo::QUBO; +pub use sparse_matrix_compression::SparseMatrixCompression; #[cfg(feature = "example-db")] pub(crate) fn canonical_model_example_specs() -> Vec { @@ -35,5 +38,6 @@ pub(crate) fn canonical_model_example_specs() -> Vec>", description: "m x n binary matrix A" }, + FieldInfo { name: "bound_k", type_name: "usize", description: "Maximum shift range K" }, + ], + } +} + +/// Sparse Matrix Compression. +/// +/// A configuration assigns one zero-based shift value to each row. The +/// implementation reconstructs the implied storage vector internally instead of +/// enumerating storage-vector entries directly, so brute-force search runs over +/// `bound_k ^ num_rows` shift assignments. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct SparseMatrixCompression { + matrix: Vec>, + bound_k: usize, +} + +impl SparseMatrixCompression { + /// Create a new SparseMatrixCompression instance. + /// + /// # Panics + /// + /// Panics if `bound_k == 0` or if the matrix rows are ragged. + pub fn new(matrix: Vec>, bound_k: usize) -> Self { + assert!(bound_k > 0, "bound_k must be positive"); + + let num_cols = matrix.first().map_or(0, Vec::len); + for row in &matrix { + assert_eq!(row.len(), num_cols, "All rows must have the same length"); + } + + Self { matrix, bound_k } + } + + /// Return the binary matrix. + pub fn matrix(&self) -> &[Vec] { + &self.matrix + } + + /// Return the shift bound `K`. + pub fn bound_k(&self) -> usize { + self.bound_k + } + + /// Return the number of rows `m`. + pub fn num_rows(&self) -> usize { + self.matrix.len() + } + + /// Return the number of columns `n`. + pub fn num_cols(&self) -> usize { + self.matrix.first().map_or(0, Vec::len) + } + + /// Return the storage-vector length `n + K`. + pub fn storage_len(&self) -> usize { + self.num_cols() + self.bound_k + } + + /// Decode a zero-based config into the one-based shifts used in the + /// mathematical definition. + pub fn decode_shifts(&self, config: &[usize]) -> Option> { + if config.len() != self.num_rows() || config.iter().any(|&shift| shift >= self.bound_k) { + return None; + } + + Some(config.iter().map(|&shift| shift + 1).collect()) + } + + /// Construct the implied storage vector for a shift assignment. + /// + /// Returns `None` if the shifts are malformed or if the overlay is invalid. + /// Row labels are stored as `1..=m`; `0` denotes an unused storage slot. + pub fn storage_vector(&self, config: &[usize]) -> Option> { + let shifts = self.decode_shifts(config)?; + let mut storage = vec![0; self.storage_len()]; + + for (row_idx, row) in self.matrix.iter().enumerate() { + let row_label = row_idx + 1; + let shift_offset = shifts[row_idx] - 1; + + for (col_idx, &entry) in row.iter().enumerate() { + if !entry { + continue; + } + + let slot_idx = shift_offset + col_idx; + let slot = &mut storage[slot_idx]; + if *slot != 0 && *slot != row_label { + return None; + } + *slot = row_label; + } + } + + for (row_idx, row) in self.matrix.iter().enumerate() { + let row_label = row_idx + 1; + let shift_offset = shifts[row_idx] - 1; + + for (col_idx, &entry) in row.iter().enumerate() { + let matches_row = storage[shift_offset + col_idx] == row_label; + if entry != matches_row { + return None; + } + } + } + + Some(storage) + } +} + +impl Problem for SparseMatrixCompression { + const NAME: &'static str = "SparseMatrixCompression"; + type Metric = bool; + + fn dims(&self) -> Vec { + vec![self.bound_k; self.num_rows()] + } + + fn evaluate(&self, config: &[usize]) -> bool { + self.storage_vector(config).is_some() + } + + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![] + } +} + +impl SatisfactionProblem for SparseMatrixCompression {} + +crate::declare_variants! { + default sat SparseMatrixCompression => "(bound_k ^ num_rows) * num_rows * num_cols", +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_model_example_specs() -> Vec { + vec![crate::example_db::specs::ModelExampleSpec { + id: "sparse_matrix_compression", + instance: Box::new(SparseMatrixCompression::new( + vec![ + vec![true, false, false, true], + vec![false, true, false, false], + vec![false, false, true, false], + vec![true, false, false, false], + ], + 2, + )), + optimal_config: vec![1, 1, 1, 0], + optimal_value: serde_json::json!(true), + }] +} + +#[cfg(test)] +#[path = "../../unit_tests/models/algebraic/sparse_matrix_compression.rs"] +mod tests; diff --git a/src/models/mod.rs b/src/models/mod.rs index 97a533e65..dfe9d4a5b 100644 --- a/src/models/mod.rs +++ b/src/models/mod.rs @@ -11,7 +11,7 @@ pub mod set; // Re-export commonly used types pub use algebraic::{ ClosestVectorProblem, ConsecutiveBlockMinimization, ConsecutiveOnesSubmatrix, - QuadraticAssignment, BMF, ILP, QUBO, + QuadraticAssignment, SparseMatrixCompression, BMF, ILP, QUBO, }; pub use formula::{ CNFClause, CircuitSAT, KSatisfiability, NAESatisfiability, QuantifiedBooleanFormulas, diff --git a/src/unit_tests/models/algebraic/sparse_matrix_compression.rs b/src/unit_tests/models/algebraic/sparse_matrix_compression.rs new file mode 100644 index 000000000..63f47320c --- /dev/null +++ b/src/unit_tests/models/algebraic/sparse_matrix_compression.rs @@ -0,0 +1,122 @@ +use super::*; +use crate::registry::VariantEntry; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; + +fn issue_example_matrix() -> Vec> { + vec![ + vec![true, false, false, true], + vec![false, true, false, false], + vec![false, false, true, false], + vec![true, false, false, false], + ] +} + +#[test] +fn test_sparse_matrix_compression_basic() { + let problem = SparseMatrixCompression::new(issue_example_matrix(), 2); + + assert_eq!(problem.matrix(), issue_example_matrix().as_slice()); + assert_eq!(problem.num_rows(), 4); + assert_eq!(problem.num_cols(), 4); + assert_eq!(problem.bound_k(), 2); + assert_eq!(problem.storage_len(), 6); + assert_eq!(problem.dims(), vec![2; 4]); + assert_eq!( + ::NAME, + "SparseMatrixCompression" + ); + assert_eq!(::variant(), vec![]); +} + +#[test] +fn test_sparse_matrix_compression_issue_example_is_satisfying() { + let problem = SparseMatrixCompression::new(issue_example_matrix(), 2); + + assert!(problem.evaluate(&[1, 1, 1, 0])); + assert_eq!( + problem + .storage_vector(&[1, 1, 1, 0]) + .expect("issue example should produce an overlay"), + vec![4, 1, 2, 3, 1, 0] + ); +} + +#[test] +fn test_sparse_matrix_compression_issue_unsatisfying_examples() { + let problem = SparseMatrixCompression::new(issue_example_matrix(), 2); + + assert!(!problem.evaluate(&[0, 0, 0, 0])); + assert!(!problem.evaluate(&[0, 1, 1, 1])); + assert!(!problem.evaluate(&[1, 1, 1, 1])); +} + +#[test] +fn test_sparse_matrix_compression_rejects_bad_configs() { + let problem = SparseMatrixCompression::new(issue_example_matrix(), 2); + + assert!(!problem.evaluate(&[1, 1, 1])); + assert!(!problem.evaluate(&[1, 1, 1, 0, 0])); + assert!(!problem.evaluate(&[2, 1, 1, 0])); + assert!(problem.storage_vector(&[2, 1, 1, 0]).is_none()); +} + +#[test] +fn test_sparse_matrix_compression_bruteforce_finds_unique_solution() { + let problem = SparseMatrixCompression::new(issue_example_matrix(), 2); + let solver = BruteForce::new(); + + let solution = solver + .find_satisfying(&problem) + .expect("issue example should be satisfiable"); + assert_eq!(solution, vec![1, 1, 1, 0]); + + let all = solver.find_all_satisfying(&problem); + assert_eq!(all, vec![vec![1, 1, 1, 0]]); +} + +#[test] +fn test_sparse_matrix_compression_serialization() { + let problem = SparseMatrixCompression::new(issue_example_matrix(), 2); + + let json = serde_json::to_value(&problem).unwrap(); + assert_eq!( + json, + serde_json::json!({ + "matrix": [ + [true, false, false, true], + [false, true, false, false], + [false, false, true, false], + [true, false, false, false], + ], + "bound_k": 2, + }) + ); + + let restored: SparseMatrixCompression = serde_json::from_value(json).unwrap(); + assert_eq!(restored.num_rows(), 4); + assert_eq!(restored.num_cols(), 4); + assert_eq!(restored.bound_k(), 2); +} + +#[test] +fn test_sparse_matrix_compression_complexity_metadata_matches_evaluator() { + let entry = inventory::iter::() + .into_iter() + .find(|entry| entry.name == "SparseMatrixCompression") + .expect("SparseMatrixCompression variant entry should exist"); + + assert_eq!(entry.complexity, "(bound_k ^ num_rows) * num_rows * num_cols"); +} + +#[test] +#[should_panic(expected = "bound_k")] +fn test_sparse_matrix_compression_rejects_zero_bound() { + let _ = SparseMatrixCompression::new(issue_example_matrix(), 0); +} + +#[test] +#[should_panic(expected = "same length")] +fn test_sparse_matrix_compression_rejects_ragged_matrix() { + let _ = SparseMatrixCompression::new(vec![vec![true, false], vec![true]], 2); +} diff --git a/src/unit_tests/registry/problem_type.rs b/src/unit_tests/registry/problem_type.rs index 6215bda0e..6ca8cfdb3 100644 --- a/src/unit_tests/registry/problem_type.rs +++ b/src/unit_tests/registry/problem_type.rs @@ -45,6 +45,13 @@ fn find_problem_type_by_alias_matches_canonical_name() { assert_eq!(problem.canonical_name, "MaximumIndependentSet"); } +#[test] +fn find_problem_type_by_alias_matches_sparse_matrix_compression() { + let problem = find_problem_type_by_alias("SparseMatrixCompression") + .expect("SparseMatrixCompression should be registered"); + assert_eq!(problem.canonical_name, "SparseMatrixCompression"); +} + #[test] fn problem_types_returns_all_registered() { let types = problem_types(); From 013d5d69ee120987d92419fa7b006279a5c4d8ef Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 16:50:19 +0800 Subject: [PATCH 3/6] chore: remove plan file after implementation --- ...6-03-22-sparse-matrix-compression-model.md | 351 ------------------ 1 file changed, 351 deletions(-) delete mode 100644 docs/plans/2026-03-22-sparse-matrix-compression-model.md diff --git a/docs/plans/2026-03-22-sparse-matrix-compression-model.md b/docs/plans/2026-03-22-sparse-matrix-compression-model.md deleted file mode 100644 index 14c2c1cf7..000000000 --- a/docs/plans/2026-03-22-sparse-matrix-compression-model.md +++ /dev/null @@ -1,351 +0,0 @@ -# Sparse Matrix Compression Implementation Plan - -> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. - -**Goal:** Implement `SparseMatrixCompression` as a new algebraic satisfaction model, register it for CLI/example-db/paper workflows, and preserve the issue's verified `4 x 4`, `K = 2` example and complexity metadata. - -**Architecture:** Represent configurations as row-shift assignments only, one variable per matrix row with domain `0..bound_k-1`. `evaluate()` should build the implied storage vector internally and reject configurations whose shifted supports collide. This keeps brute-force search at `bound_k ^ num_rows`, matching the issue and avoiding a much larger search space from enumerating storage-vector entries explicitly. Batch 1 delivers code, tests, registry wiring, CLI creation, and the canonical example. Batch 2 adds the paper entry after the example fixture is available. - -**Tech Stack:** Rust workspace, serde, inventory registry, `pred` CLI, Typst paper - ---- - -## Issue Packet - -| Item | Decision | -|---|---| -| Issue | `#416` — `[Model] SparseMatrixCompression` | -| Repo skill | `.claude/skills/add-model/SKILL.md` | -| Category | `src/models/algebraic/` | -| Problem type | Satisfaction (`Metric = bool`) | -| Type parameters | None | -| Core fields | `matrix: Vec>`, `bound_k: usize` | -| Search space | `vec![bound_k; num_rows]` | -| Complexity string | `"(bound_k ^ num_rows) * num_rows * num_cols"` | -| Solver strategy for this PR | Brute-force over row shifts only | -| Associated rule | `Graph 3-Colorability -> SparseMatrixCompression` (issue crossref `R107`) | -| Important issue comments | Preserve the fixed approximation note, concrete complexity string, and the clean unique-solution example from the `/fix-issue` changelog | - -## Batch Layout - -- **Batch 1:** add model code, tests, registry/module wiring, canonical example, and CLI creation/help. -- **Batch 2:** add the paper `problem-def(...)` entry after Batch 1 is green. - -## Design Notes - -- The mathematical definition mentions both row shifts `s(i)` and storage-vector entries `b_j`, but the implementation should not enumerate `b_j` in `dims()`. Instead, it should construct the unique implied storage vector for a chosen shift assignment and check whether every `1` lands on an empty slot or the same row label. -- Use zero-based config values for solver compatibility. The issue's satisfying shift assignment `s = (2, 2, 2, 1)` should therefore appear in code as config `[1, 1, 1, 0]`. -- Keep the storage vector representation explicit in helper methods and tests because the issue's expected outcome includes `b = (4, 1, 2, 3, 1, 0)`. -- Do **not** add an ILP reduction in this PR. The issue already supplies a valid brute-force solver path, and this PR should stay a model-only change. - -### Task 1: Lock Down Model Behavior with Failing Tests - -**Files:** -- Create: `src/unit_tests/models/algebraic/sparse_matrix_compression.rs` -- Modify: `problemreductions-cli/src/commands/create.rs` - -**Step 1: Write the failing model tests** - -Add a new unit test file for the exact issue example matrix: - -```rust -fn issue_example_matrix() -> Vec> { - vec![ - vec![true, false, false, true], - vec![false, true, false, false], - vec![false, false, true, false], - vec![true, false, false, false], - ] -} -``` - -Cover these behaviors: -- constructor/getters: `num_rows() == 4`, `num_cols() == 4`, `bound_k() == 2`, `storage_len() == 6`, `dims() == vec![2; 4]` -- satisfying config: `[1, 1, 1, 0]` evaluates to `true` -- implied storage vector: `[1, 1, 1, 0]` produces `vec![4, 1, 2, 3, 1, 0]` -- unsatisfying configs from the issue: `[0, 0, 0, 0]`, `[0, 1, 1, 1]`, `[1, 1, 1, 1]` -- brute-force uniqueness: exactly one satisfying config, and it is `[1, 1, 1, 0]` -- serde shape: JSON uses `matrix` and `bound_k` -- metadata check: registry complexity string is `"(bound_k ^ num_rows) * num_rows * num_cols"` -- constructor guards: ragged rows panic; `bound_k == 0` panics - -**Step 2: Run the model tests to verify they fail** - -Run: - -```bash -cargo test sparse_matrix_compression --lib -``` - -Expected: FAIL because the model file and registrations do not exist yet. - -**Step 3: Write the failing CLI creation test** - -In `problemreductions-cli/src/commands/create.rs`, add a focused test that creates the issue example via CLI: - -```rust -#[test] -fn test_create_sparse_matrix_compression_json() { /* parse --matrix and --bound */ } -``` - -Assert: -- output `type == "SparseMatrixCompression"` -- serialized data contains the `4 x 4` matrix -- serialized `bound_k == 2` - -Also add one negative test that omits `--bound` and confirms the usage message mentions `SparseMatrixCompression requires --matrix and --bound`. - -**Step 4: Run the CLI tests to verify they fail** - -Run: - -```bash -cargo test -p problemreductions-cli sparse_matrix_compression -``` - -Expected: FAIL because the CLI arm/import/help text do not exist yet. - -### Task 2: Implement the Model and Registry Wiring - -**Files:** -- Create: `src/models/algebraic/sparse_matrix_compression.rs` -- Modify: `src/models/algebraic/mod.rs` -- Modify: `src/models/mod.rs` -- Modify: `src/lib.rs` - -**Step 1: Write the minimal model implementation** - -Create `src/models/algebraic/sparse_matrix_compression.rs` with: -- `inventory::submit!` `ProblemSchemaEntry` -- `#[derive(Debug, Clone, Serialize, Deserialize)]` -- constructor `new(matrix, bound_k)` with rectangular-row and positive-`bound_k` checks -- getters: `matrix()`, `bound_k()`, `num_rows()`, `num_cols()`, `storage_len()` -- helper(s): - - `decode_shifts(config) -> Option>` or equivalent - - `storage_vector(config) -> Option>` that returns the implied `b` vector when the overlay is valid -- `Problem` impl: - - `NAME = "SparseMatrixCompression"` - - `Metric = bool` - - `dims() = vec![self.bound_k; self.num_rows()]` - - `evaluate(config)` returns `self.storage_vector(config).is_some()` - - `variant() = crate::variant_params![]` -- `SatisfactionProblem` impl -- `declare_variants!`: - -```rust -crate::declare_variants! { - default sat SparseMatrixCompression => "(bound_k ^ num_rows) * num_rows * num_cols", -} -``` - -- `#[cfg(feature = "example-db")] canonical_model_example_specs()` using the issue's fixed example and `optimal_config: vec![1, 1, 1, 0]` -- test link: - -```rust -#[cfg(test)] -#[path = "../../unit_tests/models/algebraic/sparse_matrix_compression.rs"] -mod tests; -``` - -**Step 2: Register the model** - -Update: -- `src/models/algebraic/mod.rs` - - add module + public re-export - - extend `canonical_model_example_specs()` with `sparse_matrix_compression::canonical_model_example_specs()` -- `src/models/mod.rs` - - add `SparseMatrixCompression` to the algebraic re-export list -- `src/lib.rs` - - add `SparseMatrixCompression` to `prelude` - -**Step 3: Run the model tests again** - -Run: - -```bash -cargo test sparse_matrix_compression --lib -``` - -Expected: the new model tests pass, or fail only on CLI/paper gaps not yet implemented. - -**Step 4: Commit the model slice** - -```bash -git add src/models/algebraic/sparse_matrix_compression.rs \ - src/models/algebraic/mod.rs \ - src/models/mod.rs \ - src/lib.rs \ - src/unit_tests/models/algebraic/sparse_matrix_compression.rs -git commit -m "Add SparseMatrixCompression model" -``` - -### Task 3: Wire CLI Creation and Help - -**Files:** -- Modify: `problemreductions-cli/src/commands/create.rs` -- Modify: `problemreductions-cli/src/cli.rs` - -**Step 1: Implement the CLI create arm** - -In `problemreductions-cli/src/commands/create.rs`: -- import `SparseMatrixCompression` -- add `example_for("SparseMatrixCompression")` -- add a `help_flag_name()` override so schema field `bound_k` maps to CLI flag `--bound` -- add a `help_flag_hint()` override so `matrix` is documented as semicolon-separated `0/1` rows -- add a `"SparseMatrixCompression"` create arm that: - - uses `parse_bool_matrix(args)?` - - requires `--bound` - - converts `bound` to `usize` - - serializes `SparseMatrixCompression::new(matrix, bound)` - -Use this usage string: - -```text -Usage: pred create SparseMatrixCompression --matrix "1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0" --bound 2 -``` - -**Step 2: Update top-level CLI help** - -In `problemreductions-cli/src/cli.rs`, add: - -```text -SparseMatrixCompression --matrix (0/1), --bound -``` - -to the "Flags by problem type" table. - -**Step 3: Re-run the targeted CLI tests** - -Run: - -```bash -cargo test -p problemreductions-cli sparse_matrix_compression -``` - -Expected: the new create tests pass. - -**Step 4: Commit the CLI slice** - -```bash -git add problemreductions-cli/src/commands/create.rs problemreductions-cli/src/cli.rs -git commit -m "Add CLI support for SparseMatrixCompression" -``` - -### Task 4: Verify Batch 1 End-to-End - -**Files:** -- Reference: `src/models/algebraic/sparse_matrix_compression.rs` -- Reference: `src/unit_tests/models/algebraic/sparse_matrix_compression.rs` -- Reference: `problemreductions-cli/src/commands/create.rs` - -**Step 1: Run focused verification** - -Run: - -```bash -cargo test sparse_matrix_compression --lib -cargo test -p problemreductions-cli sparse_matrix_compression -``` - -Expected: PASS. - -**Step 2: Run project verification for code changes** - -Run: - -```bash -make test clippy -``` - -Expected: PASS. - -**Step 3: Inspect the canonical example through the CLI** - -Run: - -```bash -pred create --example SparseMatrixCompression -o /tmp/smc-example.json -pred evaluate /tmp/smc-example.json --config 1,1,1,0 -pred solve /tmp/smc-example.json -``` - -Expected: -- example JSON matches the issue matrix and `bound_k = 2` -- `pred evaluate` returns `true` -- `pred solve` finds the unique satisfying config - -### Task 5: Add the Paper Entry (Batch 2) - -**Files:** -- Modify: `docs/paper/reductions.typ` - -**Step 1: Write the paper entry after code is green** - -Add a display-name entry: - -```typst -"SparseMatrixCompression": [Sparse Matrix Compression], -``` - -Add a `#problem-def("SparseMatrixCompression")[...][...]` block that: -- states the formal row-overlay definition -- explains that the implementation searches over shifts and reconstructs the storage vector internally -- cites the Garey & Johnson catalog entry and the practical DFA/parser-table motivation -- uses `load-model-example("SparseMatrixCompression")` -- explains that stored config `[1, 1, 1, 0]` encodes shifts `(2, 2, 2, 1)` -- shows the resulting storage vector `(4, 1, 2, 3, 1, 0)` -- states that the fixture has exactly one satisfying shift assignment -- includes a `pred-commands(...)` block derived from the loaded example - -**Step 2: Build the paper** - -Run: - -```bash -make paper -``` - -Expected: PASS. - -**Step 3: Re-run final repo verification** - -Run: - -```bash -make test clippy -``` - -Expected: PASS. - -**Step 4: Commit the documentation slice** - -```bash -git add docs/paper/reductions.typ -git commit -m "Document SparseMatrixCompression" -``` - -### Task 6: Final Push and Cleanup - -**Files:** -- Modify: `docs/plans/2026-03-22-sparse-matrix-compression-model.md` (remove at the end per pipeline workflow) - -**Step 1: Summarize deviations before push** - -Record whether any of these changed during implementation: -- field names (`bound_k` vs `bound`) -- helper method names -- exact paper example wording - -**Step 2: Push implementation commits** - -```bash -git push -``` - -**Step 3: Remove the plan file after implementation** - -```bash -git rm docs/plans/2026-03-22-sparse-matrix-compression-model.md -git commit -m "chore: remove plan file after implementation" -git push -``` From aa58f0d60b3119bf0604b136ac466246f27c2e8b Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Mon, 23 Mar 2026 01:07:55 +0800 Subject: [PATCH 4/6] fix: cargo fmt after merge with main --- problemreductions-cli/src/commands/create.rs | 8 +++----- .../models/algebraic/sparse_matrix_compression.rs | 5 ++++- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 7174c622c..88c947a79 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -2793,9 +2793,7 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { let matrix = parse_bool_matrix(args)?; let usage = "Usage: pred create SparseMatrixCompression --matrix \"1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0\" --bound 2"; let bound = args.bound.ok_or_else(|| { - anyhow::anyhow!( - "SparseMatrixCompression requires --matrix and --bound\n\n{usage}" - ) + anyhow::anyhow!("SparseMatrixCompression requires --matrix and --bound\n\n{usage}") })?; let bound = parse_nonnegative_usize_bound(bound, "SparseMatrixCompression", usage)?; ( @@ -7835,8 +7833,8 @@ mod tests { args.matrix = Some("1,0,0,1;0,1,0,0;0,0,1,0;1,0,0,0".to_string()); args.bound = Some(2); - let output_path = std::env::temp_dir() - .join(format!("smc-create-{}.json", std::process::id())); + let output_path = + std::env::temp_dir().join(format!("smc-create-{}.json", std::process::id())); let out = OutputConfig { output: Some(output_path.clone()), quiet: true, diff --git a/src/unit_tests/models/algebraic/sparse_matrix_compression.rs b/src/unit_tests/models/algebraic/sparse_matrix_compression.rs index 63f47320c..a6095d630 100644 --- a/src/unit_tests/models/algebraic/sparse_matrix_compression.rs +++ b/src/unit_tests/models/algebraic/sparse_matrix_compression.rs @@ -106,7 +106,10 @@ fn test_sparse_matrix_compression_complexity_metadata_matches_evaluator() { .find(|entry| entry.name == "SparseMatrixCompression") .expect("SparseMatrixCompression variant entry should exist"); - assert_eq!(entry.complexity, "(bound_k ^ num_rows) * num_rows * num_cols"); + assert_eq!( + entry.complexity, + "(bound_k ^ num_rows) * num_rows * num_cols" + ); } #[test] From 1bead2abd47b8837cfbe81319b3d42cc1869ac34 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Mon, 23 Mar 2026 01:22:48 +0800 Subject: [PATCH 5/6] fix: reject --bound 0 in CLI instead of panicking SparseMatrixCompression::new() asserts bound_k > 0, but the CLI's parse_nonnegative_usize_bound() accepted 0 and passed it through, causing a panic. Add an explicit check before construction. Co-Authored-By: Claude Opus 4.6 (1M context) --- problemreductions-cli/src/commands/create.rs | 21 ++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 88c947a79..4abe9ee30 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -2796,6 +2796,9 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { anyhow::anyhow!("SparseMatrixCompression requires --matrix and --bound\n\n{usage}") })?; let bound = parse_nonnegative_usize_bound(bound, "SparseMatrixCompression", usage)?; + if bound == 0 { + anyhow::bail!("SparseMatrixCompression requires bound >= 1\n\n{usage}"); + } ( ser(SparseMatrixCompression::new(matrix, bound))?, resolved_variant.clone(), @@ -7881,4 +7884,22 @@ mod tests { assert!(err.contains("SparseMatrixCompression requires --matrix and --bound")); assert!(err.contains("Usage: pred create SparseMatrixCompression")); } + + #[test] + fn test_create_sparse_matrix_compression_rejects_zero_bound() { + let mut args = empty_args(); + args.problem = Some("SparseMatrixCompression".to_string()); + args.matrix = Some("1,0;0,1".to_string()); + args.bound = Some(0); + + let out = OutputConfig { + output: None, + quiet: true, + json: false, + auto_json: false, + }; + + let err = create(&args, &out).unwrap_err().to_string(); + assert!(err.contains("bound >= 1")); + } } From 190776b6ae5d14c727a8f4a5a8df71308629f7f4 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Mon, 23 Mar 2026 01:37:48 +0800 Subject: [PATCH 6/6] fix: remove unreachable second pass in storage_vector() After the first pass succeeds without collisions, the biconditional a_{ij}=1 iff b[slot]=i is already guaranteed: row labels are unique and each row only writes to its 1-entry slots. The second pass was dead code (the codecov-uncovered line). Co-Authored-By: Claude Opus 4.6 (1M context) --- src/models/algebraic/sparse_matrix_compression.rs | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/models/algebraic/sparse_matrix_compression.rs b/src/models/algebraic/sparse_matrix_compression.rs index 9fd6313c6..a41dfcc10 100644 --- a/src/models/algebraic/sparse_matrix_compression.rs +++ b/src/models/algebraic/sparse_matrix_compression.rs @@ -113,18 +113,6 @@ impl SparseMatrixCompression { } } - for (row_idx, row) in self.matrix.iter().enumerate() { - let row_label = row_idx + 1; - let shift_offset = shifts[row_idx] - 1; - - for (col_idx, &entry) in row.iter().enumerate() { - let matches_row = storage[shift_offset + col_idx] == row_label; - if entry != matches_row { - return None; - } - } - } - Some(storage) } }