Fix #294: [Model] UndirectedFlowLowerBounds

[GiggleLiu]

Summary

• add the execution plan for UndirectedFlowLowerBounds
• scope the work to the model, CLI/example-db wiring, and paper entry
• keep related rule work out of this PR

Fixes #294

[codecov]

Codecov Report

❌ Patch coverage is 97.29730% with 8 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.61%. Comparing base (07c0da1) to head (57c6458).
⚠️ Report is 2 commits behind head on main.

Files with missing lines	Patch %	Lines
src/models/graph/undirected_flow_lower_bounds.rs	96.41%	8 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #741      +/-   ##
==========================================
- Coverage   97.61%   97.61%   -0.01%     
==========================================
  Files         433      435       +2     
  Lines       53474    53770     +296     
==========================================
+ Hits        52197    52485     +288     
- Misses       1277     1285       +8     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[GiggleLiu]

Implementation Summary

Changes

• Added UndirectedFlowLowerBounds as a new graph satisfaction model with registry metadata, canonical example-db data, and focused unit tests.
• Wired the model into graph/module/prelude exports plus Typst paper documentation and bibliography.
• Added CLI support for pred create UndirectedFlowLowerBounds with --capacities, --lower-bounds, --source, --sink, and --requirement, plus focused CLI tests.

Deviations from Plan

• The model intentionally exposes one binary orientation variable per edge instead of raw per-direction flow variables. evaluate() orients the undirected graph from that config and then solves the remaining lower-bounded directed feasibility problem internally via a circulation/max-flow reduction. This matches the issue's required 2^num_edges complexity and avoids a pseudo-polynomial witness encoding.
• The current repo no longer uses standalone builder functions in src/example_db/model_builders.rs; the canonical example is registered through canonical_model_example_specs() in the model file and chained from src/models/graph/mod.rs.

Open Questions

• None.

[GiggleLiu]

Agentic Review Report

Structural Check

Structural Review: model UndirectedFlowLowerBounds

Structural Completeness

#	Check	Status
1	Model file exists	PASS
2	inventory::submit! present	PASS
3	Serialize / Deserialize derive on struct	PASS
4	Problem trait impl	PASS
5	SatisfactionProblem impl	PASS
6	#[cfg(test)] + #[path = ...] test link	PASS
7	Dedicated model test file exists	PASS
8	Test file has at least 3 test functions	PASS
9	Registered in src/models/graph/mod.rs	PASS
10	Re-exported in src/models/mod.rs	PASS
11	declare_variants! entry exists	PASS
12	CLI resolve_alias entry exists	PASS
13	CLI create support exists	PASS
14	Canonical model example registered	PASS — via canonical_model_example_specs() chained from src/models/graph/mod.rs, which is the repo’s current example-db pattern
15	Paper display-name entry exists	PASS
16	Paper problem-def block exists	PASS
17	No blacklisted autogenerated files committed	PASS

Build Status

• make test: PASS
• make clippy: PASS

Semantic Review

• evaluate() correctness: ISSUE — the implementation accepts source == sink, but the circulation reduction then adds the required t -> s edge as a self-loop. That self-loop contributes zero net balance, so the requirement can be silently dropped and the model returns false positives. Reproduced with pred create UndirectedFlowLowerBounds --graph 0-1 --capacities 1 --lower-bounds 0 --source 0 --sink 0 --requirement 1 followed by pred solve, which returns a satisfying solution. Relevant code: src/models/graph/undirected_flow_lower_bounds.rs:78-87, src/models/graph/undirected_flow_lower_bounds.rs:186-212.
• dims() correctness: OK — one binary orientation variable per edge matches the documented implementation strategy and declared 2^num_edges complexity.
• Size getter consistency: OK — num_vertices() / num_edges() match the registered complexity variables.
• Weight handling: OK — not applicable.

Issue Compliance

#	Check	Status
1	Problem name matches issue	OK
2	Mathematical definition matches	OK for ordinary s != t instances; ISSUE for accepted s == t instances, which are handled incorrectly as noted above
3	Problem type (sat) matches	OK
4	Type parameters match	OK
5	Configuration space matches	OK — implementation intentionally uses one orientation bit per edge and solves the residual lower-bounded flow internally
6	Feasibility check matches	ISSUE — indistinct terminals are not rejected, and the resulting evaluator can accept instances whose required flow should not be satisfiable
7	Objective function matches	OK
8	Complexity matches	OK

Summary

• 17/17 structural checks passed
• 6/8 issue-compliance checks passed cleanly
• Issues found:
  • UndirectedFlowLowerBounds should reject source == sink; currently those instances can evaluate to true because the demand edge becomes a self-loop and contributes no balance.

---

Quality Check

Quality Review

Design Principles

• DRY: ISSUE — the shared parse_capacities() helper was generalized for this PR, but in the process it dropped the domain-size validation that UndirectedTwoCommodityIntegralFlow still relies on in its constructor. That created a regression in an existing CLI path. Relevant code: problemreductions-cli/src/commands/create.rs:4205-4226, src/models/graph/undirected_two_commodity_integral_flow.rs:90-97.
• KISS: OK — the core orientation-plus-circulation approach is straightforward and much simpler than encoding pseudo-polynomial witness magnitudes into the explicit search space.
• HC/LC: OK — model logic, CLI wiring, tests, and paper docs stay in separate modules.

HCI (CLI changed)

• Error messages: ISSUE — invalid UndirectedFlowLowerBounds inputs currently panic in the model constructor instead of returning actionable CLI errors. Reproduced with:
  • pred create UndirectedFlowLowerBounds ... --capacities 1,1,1,1 --lower-bounds 2,2,1,1 ... → panic: lower bound at edge 0 must be at most its capacity
  • pred create UndirectedFlowLowerBounds ... --requirement 0 ... → panic: requirement must be at least 1
    Relevant code: problemreductions-cli/src/commands/create.rs:1332-1358, problemreductions-cli/src/commands/create.rs:4230-4251, src/models/graph/undirected_flow_lower_bounds.rs:87-93.
• Discoverability: OK — pred list, pred show, help text, and create examples all expose the new model clearly.
• Consistency: ISSUE — neighboring CLI paths already have explicit “return an error, not panic” coverage for invalid input, but this new path relies on constructor asserts instead. The same refactor also regressed an existing CLI command (UndirectedTwoCommodityIntegralFlow).
• Least surprise: ISSUE — pred create ... --source 0 --sink 0 --requirement 1 succeeds, and the resulting instance solves to true, which is surprising for an s-t flow problem.
• Feedback: OK — happy-path create, solve, and evaluate output is clear.

Test Quality

• Naive test detection: ISSUE
  • The new model tests cover happy-path evaluation, serialization, and one infeasible instance, but they miss the indistinct-terminal edge case that currently produces a false positive. Relevant file: src/unit_tests/models/graph/undirected_flow_lower_bounds.rs.
  • The new CLI tests cover serialization and missing --lower-bounds, but they do not cover the two panic paths introduced here (lower_bounds > capacities, --requirement 0) or the UndirectedTwoCommodityIntegralFlow regression from the parse_capacities() refactor. Relevant file: problemreductions-cli/src/commands/create.rs:5911-5989.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

• UndirectedFlowLowerBounds accepts source == sink, and the model then returns false positives because the required-flow edge in the circulation reduction collapses into a self-loop. Relevant code: src/models/graph/undirected_flow_lower_bounds.rs:78-87, src/models/graph/undirected_flow_lower_bounds.rs:186-212.
• pred create UndirectedFlowLowerBounds panics on invalid lower bounds and on --requirement 0 instead of reporting a normal CLI error. Relevant code: problemreductions-cli/src/commands/create.rs:1332-1358, problemreductions-cli/src/commands/create.rs:4230-4251, src/models/graph/undirected_flow_lower_bounds.rs:87-93.
• The parse_capacities() refactor regresses pred create UndirectedTwoCommodityIntegralFlow: a max-size capacity now panics in the constructor instead of being rejected in CLI validation. Reproduced with --capacities 18446744073709551615,1,2. Relevant code: problemreductions-cli/src/commands/create.rs:4205-4226, src/models/graph/undirected_two_commodity_integral_flow.rs:90-97.

Minor (Nice to Have)

None.

Summary

• The happy path is solid: the model is registered correctly, documented, and works end-to-end from pred create --example through pred solve / pred evaluate.
• The main risks are input-validation gaps: one real model-correctness bug (source == sink) and two CLI panic paths (one new, one regression to an existing feature).

---

Agentic Feature Tests

Feature Test Report: problem-reductions CLI

Feature tested: UndirectedFlowLowerBounds
Use case: discover the new model from the CLI, inspect it, create the canonical example, solve it, and evaluate the documented witness configuration
Verdict: fail

Summary

Check	Result	Notes
pred list	PASS	UndirectedFlowLowerBounds appears in the catalog with O(2^num_edges)
pred show UndirectedFlowLowerBounds	PASS	Schema, description, and complexity display correctly
pred create --example UndirectedFlowLowerBounds	PASS	Example JSON writes successfully
pred solve <example>	PASS	Brute-force solver returns the documented all-zero orientation
pred evaluate <example> --config 0,0,0,0,0,0,0	PASS	Returns true

Findings

• Confirmed: invalid lower bounds crash the CLI instead of returning an ordinary validation error.
  • Reproduction: pred create UndirectedFlowLowerBounds --graph 0-1,0-2,1-3,2-3 --capacities 1,1,1,1 --lower-bounds 2,2,1,1 --source 0 --sink 3 --requirement 2
  • Actual result: process panics with lower bound at edge 0 must be at most its capacity
  • Classification: confirmed
  • Severity: important
• Confirmed: --requirement 0 crashes the CLI instead of returning an ordinary validation error.
  • Reproduction: pred create UndirectedFlowLowerBounds --graph 0-1,0-2,1-3,2-3 --capacities 2,2,1,1 --lower-bounds 2,2,1,1 --source 0 --sink 3 --requirement 0
  • Actual result: process panics with requirement must be at least 1
  • Classification: confirmed
  • Severity: important
• Confirmed: indistinct terminals produce a false-positive satisfiable instance.
  • Reproduction: pred create UndirectedFlowLowerBounds --graph 0-1 --capacities 1 --lower-bounds 0 --source 0 --sink 0 --requirement 1, then pred solve ... --solver brute-force
  • Actual result: solver returns {"evaluation":"true","solution":[0],...}
  • Classification: confirmed
  • Severity: important

Suggestions

• Reject source == sink in both the model constructor and CLI validation, matching the semantics used by other path/flow-style problems.
• Validate requirement >= 1 and lower_bounds[i] <= capacities[i] in pred create UndirectedFlowLowerBounds before calling the constructor, and add non-panicking CLI tests for those cases.
• Restore the removed capacity-domain guard for UndirectedTwoCommodityIntegralFlow, either in parse_capacities() or in a model-specific validation layer, and add a regression test.

---

Generated by review-pipeline