|
| 1 | +# Unbounded Float Variables - Implementation Required |
| 2 | + |
| 3 | +**Date**: October 4, 2025 |
| 4 | +**Priority**: HIGH |
| 5 | +**Context**: Zelen (FlatZinc parser) integration |
| 6 | +**Issue**: Selen's `model.float(min, max)` does not properly handle unbounded float variables |
| 7 | + |
| 8 | +--- |
| 9 | + |
| 10 | +## Problem Statement |
| 11 | + |
| 12 | +When Zelen parses FlatZinc files with unbounded float variables like: |
| 13 | + |
| 14 | +```flatzinc |
| 15 | +var float: R; |
| 16 | +var float: P; |
| 17 | +var 0.0..10.0: I; |
| 18 | +``` |
| 19 | + |
| 20 | +Zelen currently calls: |
| 21 | +```rust |
| 22 | +self.model.float(f64::NEG_INFINITY, f64::INFINITY) // For unbounded |
| 23 | +self.model.float(0.0, 10.0) // For bounded |
| 24 | +``` |
| 25 | + |
| 26 | +**Current Behavior**: Zelen must use finite bounds as a workaround: |
| 27 | +```rust |
| 28 | +self.model.float(-1e9, 1e9) // Temporary hack |
| 29 | +``` |
| 30 | + |
| 31 | +**Result**: Solver finds technically valid but meaningless solutions with extreme values: |
| 32 | +``` |
| 33 | +R = -909836065.5737699 # Expected: ~65.78 |
| 34 | +P = -90909090.90909092 # Expected: ~1000.00 |
| 35 | +I = 9.999999999999998 # Expected: ~4.0 |
| 36 | +``` |
| 37 | + |
| 38 | +**Expected Behavior** (from Coin-BC solver): |
| 39 | +``` |
| 40 | +Borrowing 1000.00 at 4.0% interest, and repaying 260.00 |
| 41 | +per quarter for 1 year leaves 65.78 owing |
| 42 | +``` |
| 43 | + |
| 44 | +--- |
| 45 | + |
| 46 | +## Root Cause |
| 47 | + |
| 48 | +This is a **solver responsibility**, not a parser responsibility: |
| 49 | + |
| 50 | +1. **Separation of Concerns**: Zelen should only parse FlatZinc and map to Selen API |
| 51 | +2. **Solver Knowledge**: Selen knows its internal float representation and precision limits |
| 52 | +3. **Architecture**: Selen already handles integer domain discretization internally |
| 53 | + |
| 54 | +The `Model::float(min, max)` method needs to: |
| 55 | +- Accept infinite bounds gracefully |
| 56 | +- Infer reasonable finite bounds internally when needed |
| 57 | +- Use problem context to determine appropriate ranges |
| 58 | + |
| 59 | +--- |
| 60 | + |
| 61 | +## Recommended Solution |
| 62 | + |
| 63 | +### Option 1: Automatic Bound Inference (RECOMMENDED) |
| 64 | + |
| 65 | +Implement intelligent bound inference inside `Model::float()`: |
| 66 | + |
| 67 | +```rust |
| 68 | +impl Model { |
| 69 | + pub fn float(&mut self, min: f64, max: f64) -> VarId { |
| 70 | + let (actual_min, actual_max) = if min.is_infinite() || max.is_infinite() { |
| 71 | + // Infer bounds from problem context |
| 72 | + self.infer_float_bounds() |
| 73 | + } else { |
| 74 | + (min, max) |
| 75 | + }; |
| 76 | + |
| 77 | + // Create float variable with actual bounds |
| 78 | + self.create_float_variable(actual_min, actual_max) |
| 79 | + } |
| 80 | + |
| 81 | + fn infer_float_bounds(&self) -> (f64, f64) { |
| 82 | + let mut min_bound = 0.0; |
| 83 | + let mut max_bound = 0.0; |
| 84 | + let mut found_any = false; |
| 85 | + |
| 86 | + // Scan all existing float variables for bounded ranges |
| 87 | + for var_id in &self.float_variables { |
| 88 | + if let Some((min, max)) = self.get_float_bounds(var_id) { |
| 89 | + if min.is_finite() && max.is_finite() { |
| 90 | + min_bound = min_bound.min(min); |
| 91 | + max_bound = max_bound.max(max); |
| 92 | + found_any = true; |
| 93 | + } |
| 94 | + } |
| 95 | + } |
| 96 | + |
| 97 | + if found_any { |
| 98 | + // Expand by 1000x to give solver reasonable search space |
| 99 | + let range = (max_bound - min_bound).abs().max(1.0); |
| 100 | + let expansion = range * 1000.0; |
| 101 | + let inferred_min = (min_bound - expansion).max(-1e12); |
| 102 | + let inferred_max = (max_bound + expansion).min(1e12); |
| 103 | + (inferred_min, inferred_max) |
| 104 | + } else { |
| 105 | + // No context available, use conservative defaults |
| 106 | + // This is reasonable for most practical problems |
| 107 | + (-10000.0, 10000.0) |
| 108 | + } |
| 109 | + } |
| 110 | +} |
| 111 | +``` |
| 112 | + |
| 113 | +**Advantages**: |
| 114 | +- ✅ Proper separation of concerns |
| 115 | +- ✅ Solver maintains control over its internal representation |
| 116 | +- ✅ Works automatically for all users (not just Zelen) |
| 117 | +- ✅ Can be improved/tuned without changing parser |
| 118 | + |
| 119 | +### Option 2: Lazy Bound Inference (ALTERNATIVE) |
| 120 | + |
| 121 | +Defer bound inference until first constraint is posted: |
| 122 | + |
| 123 | +```rust |
| 124 | +impl Model { |
| 125 | + pub fn float(&mut self, min: f64, max: f64) -> VarId { |
| 126 | + // Store unbounded flag |
| 127 | + let var_id = self.create_float_variable_internal(min, max, min.is_infinite() || max.is_infinite()); |
| 128 | + |
| 129 | + if min.is_infinite() || max.is_infinite() { |
| 130 | + self.unbounded_float_vars.push(var_id); |
| 131 | + } |
| 132 | + |
| 133 | + var_id |
| 134 | + } |
| 135 | + |
| 136 | + fn finalize_unbounded_floats(&mut self) { |
| 137 | + // Called before solving |
| 138 | + let inferred_bounds = self.infer_float_bounds(); |
| 139 | + |
| 140 | + for var_id in &self.unbounded_float_vars { |
| 141 | + self.update_float_bounds(var_id, inferred_bounds.0, inferred_bounds.1); |
| 142 | + } |
| 143 | + |
| 144 | + self.unbounded_float_vars.clear(); |
| 145 | + } |
| 146 | +} |
| 147 | +``` |
| 148 | + |
| 149 | +**Advantages**: |
| 150 | +- ✅ Can analyze complete model before setting bounds |
| 151 | +- ✅ More accurate inference with full problem context |
| 152 | + |
| 153 | +**Disadvantages**: |
| 154 | +- ⚠️ More complex implementation |
| 155 | +- ⚠️ Requires tracking unbounded variables |
| 156 | + |
| 157 | +--- |
| 158 | + |
| 159 | +## Implementation Details |
| 160 | + |
| 161 | +### Current File Locations |
| 162 | + |
| 163 | +**Selen codebase structure**: |
| 164 | +``` |
| 165 | +src/ |
| 166 | + model/ |
| 167 | + mod.rs # Model struct and variable creation methods |
| 168 | + constraints.rs # Constraint posting methods (float_lin_eq, etc.) |
| 169 | + variables/ |
| 170 | + mod.rs # VarId and variable types |
| 171 | + domain.rs # Domain representations |
| 172 | + constraints/ |
| 173 | + propagators/ # Constraint propagators |
| 174 | +``` |
| 175 | + |
| 176 | +### Where to Make Changes |
| 177 | + |
| 178 | +**File**: `src/model/mod.rs` (or wherever `Model::float()` is defined) |
| 179 | + |
| 180 | +**Current implementation** (approximate): |
| 181 | +```rust |
| 182 | +pub fn float(&mut self, min: f64, max: f64) -> VarId { |
| 183 | + // Discretize float interval into grid |
| 184 | + let var_id = self.variables.new_float_var(min, max); |
| 185 | + var_id |
| 186 | +} |
| 187 | +``` |
| 188 | + |
| 189 | +**Updated implementation**: |
| 190 | +```rust |
| 191 | +pub fn float(&mut self, min: f64, max: f64) -> VarId { |
| 192 | + // Handle infinite bounds |
| 193 | + let (actual_min, actual_max) = if min.is_infinite() || max.is_infinite() { |
| 194 | + self.infer_float_bounds_for_unbounded() |
| 195 | + } else { |
| 196 | + (min, max) |
| 197 | + }; |
| 198 | + |
| 199 | + // Discretize float interval into grid |
| 200 | + let var_id = self.variables.new_float_var(actual_min, actual_max); |
| 201 | + var_id |
| 202 | +} |
| 203 | + |
| 204 | +fn infer_float_bounds_for_unbounded(&self) -> (f64, f64) { |
| 205 | + // Implementation from Option 1 above |
| 206 | + // ... |
| 207 | +} |
| 208 | +``` |
| 209 | + |
| 210 | +--- |
| 211 | + |
| 212 | +## Testing Requirements |
| 213 | + |
| 214 | +### Test Case 1: Unbounded Float Variables |
| 215 | +```rust |
| 216 | +#[test] |
| 217 | +fn test_unbounded_float_variables() { |
| 218 | + let mut model = Model::new(); |
| 219 | + |
| 220 | + // Should not panic or use infinite bounds |
| 221 | + let x = model.float(f64::NEG_INFINITY, f64::INFINITY); |
| 222 | + let y = model.float(-10.0, 10.0); |
| 223 | + |
| 224 | + // Should infer reasonable bounds from y |
| 225 | + model.float_lin_eq(&[1.0, 1.0], &[x, y], 0.0); |
| 226 | + |
| 227 | + let result = model.solve(); |
| 228 | + assert!(result.is_ok()); |
| 229 | +} |
| 230 | +``` |
| 231 | + |
| 232 | +### Test Case 2: Loan Problem (Real-World) |
| 233 | +```rust |
| 234 | +#[test] |
| 235 | +fn test_loan_problem_unbounded() { |
| 236 | + let mut model = Model::new(); |
| 237 | + |
| 238 | + // Unbounded float variables (principal, balance) |
| 239 | + let p = model.float(f64::NEG_INFINITY, f64::INFINITY); |
| 240 | + let r = model.float(f64::NEG_INFINITY, f64::INFINITY); |
| 241 | + |
| 242 | + // Bounded interest rate |
| 243 | + let i = model.float(0.0, 10.0); |
| 244 | + |
| 245 | + // Constraints (simplified) |
| 246 | + model.float_lin_eq(&[1.0, -0.01], &[p, i], 1000.0); |
| 247 | + |
| 248 | + let solution = model.solve().unwrap(); |
| 249 | + |
| 250 | + // Should find reasonable values, not extreme ones |
| 251 | + let p_val = solution.get_float_value(p); |
| 252 | + assert!(p_val > 0.0 && p_val < 100000.0, "Principal should be reasonable"); |
| 253 | +} |
| 254 | +``` |
| 255 | + |
| 256 | +### Test Case 3: Mixed Bounded/Unbounded |
| 257 | +```rust |
| 258 | +#[test] |
| 259 | +fn test_mixed_bounded_unbounded() { |
| 260 | + let mut model = Model::new(); |
| 261 | + |
| 262 | + let bounded = model.float(0.0, 100.0); |
| 263 | + let unbounded1 = model.float(f64::NEG_INFINITY, f64::INFINITY); |
| 264 | + let unbounded2 = model.float(f64::NEG_INFINITY, f64::INFINITY); |
| 265 | + |
| 266 | + // Unbounded variables should infer from bounded |
| 267 | + model.float_lin_eq(&[1.0, 1.0, 1.0], &[bounded, unbounded1, unbounded2], 0.0); |
| 268 | + |
| 269 | + let result = model.solve(); |
| 270 | + assert!(result.is_ok()); |
| 271 | +} |
| 272 | +``` |
| 273 | + |
| 274 | +--- |
| 275 | + |
| 276 | +## Performance Considerations |
| 277 | + |
| 278 | +1. **Bound Inference Cost**: Should be O(n) where n = number of existing float variables |
| 279 | +2. **Memory**: No additional memory overhead (just computing bounds) |
| 280 | +3. **Precision**: Ensure expanded bounds don't cause discretization issues |
| 281 | +4. **Caching**: Consider caching inferred bounds if multiple unbounded variables created |
| 282 | + |
| 283 | +--- |
| 284 | + |
| 285 | +## Alternative: Document Limitation |
| 286 | + |
| 287 | +If implementing bound inference is too complex for now, document the limitation: |
| 288 | + |
| 289 | +```rust |
| 290 | +impl Model { |
| 291 | + /// Create a float variable with the given bounds. |
| 292 | + /// |
| 293 | + /// # Important: Bounded Floats Required |
| 294 | + /// |
| 295 | + /// Selen requires finite bounds for float variables. If you have an |
| 296 | + /// "unbounded" float in your problem, you must provide reasonable finite |
| 297 | + /// bounds based on problem context. |
| 298 | + /// |
| 299 | + /// **Common defaults:** |
| 300 | + /// - Financial problems: `-1e6` to `1e6` |
| 301 | + /// - Scientific computing: `-1e9` to `1e9` |
| 302 | + /// - General purpose: `-10000.0` to `10000.0` |
| 303 | + /// |
| 304 | + /// # Panics |
| 305 | + /// |
| 306 | + /// Panics if `min` or `max` is infinite or NaN. |
| 307 | + pub fn float(&mut self, min: f64, max: f64) -> VarId { |
| 308 | + assert!(min.is_finite(), "Float variable minimum bound must be finite"); |
| 309 | + assert!(max.is_finite(), "Float variable maximum bound must be finite"); |
| 310 | + assert!(min < max, "Float variable minimum must be less than maximum"); |
| 311 | + |
| 312 | + self.create_float_variable(min, max) |
| 313 | + } |
| 314 | +} |
| 315 | +``` |
| 316 | + |
| 317 | +Then Zelen can handle the inference (less ideal, but functional). |
| 318 | + |
| 319 | +--- |
| 320 | + |
| 321 | +## Priority and Timeline |
| 322 | + |
| 323 | +**Priority**: HIGH - Blocks proper FlatZinc float support in Zelen |
| 324 | + |
| 325 | +**Estimated Effort**: |
| 326 | +- Option 1 (Inference): 2-4 hours |
| 327 | +- Option 2 (Lazy): 4-6 hours |
| 328 | +- Documentation only: 30 minutes |
| 329 | + |
| 330 | +**Recommendation**: Start with Option 1 (simple inference), can enhance later if needed. |
| 331 | + |
| 332 | +--- |
| 333 | + |
| 334 | +## Current Workaround in Zelen |
| 335 | + |
| 336 | +**File**: `/home/ross/devpublic/zelen/src/mapper.rs` (line ~97) |
| 337 | + |
| 338 | +```rust |
| 339 | +Type::Float => { |
| 340 | + // TODO: Selen should handle unbounded floats internally |
| 341 | + // For now, use conservative finite bounds as a workaround |
| 342 | + // This is a solver responsibility, not a parser responsibility |
| 343 | + self.model.float(-1e9, 1e9) // ❌ TEMPORARY HACK |
| 344 | +} |
| 345 | +``` |
| 346 | + |
| 347 | +Once Selen properly handles unbounded floats, change to: |
| 348 | +```rust |
| 349 | +Type::Float => self.model.float(f64::NEG_INFINITY, f64::INFINITY) // ✅ CORRECT |
| 350 | +``` |
| 351 | + |
| 352 | +--- |
| 353 | + |
| 354 | +## Questions to Answer |
| 355 | + |
| 356 | +Before implementing, consider: |
| 357 | + |
| 358 | +1. **What is Selen's float discretization strategy?** |
| 359 | + - Fixed-precision grid? |
| 360 | + - Adaptive precision? |
| 361 | + - Interval arithmetic? |
| 362 | + |
| 363 | +2. **What are reasonable default bounds for Selen's internal representation?** |
| 364 | + - Does discretization work well with ±1e12 range? |
| 365 | + - What's the practical precision limit? |
| 366 | + |
| 367 | +3. **Should inference be per-variable or global?** |
| 368 | + - Global: All unbounded floats get same inferred bounds |
| 369 | + - Per-variable: Each could have different inference based on local constraints |
| 370 | + |
| 371 | +4. **Should this be configurable?** |
| 372 | + - Allow user to override default unbounded behavior? |
| 373 | + - `ModelConfig { unbounded_float_bounds: (-1e6, 1e6) }`? |
| 374 | + |
| 375 | +--- |
| 376 | + |
| 377 | +## Success Criteria |
| 378 | + |
| 379 | +✅ `model.float(f64::NEG_INFINITY, f64::INFINITY)` does not panic |
| 380 | +✅ Unbounded float variables get reasonable finite bounds automatically |
| 381 | +✅ Loan problem (from Zelen) produces sensible results |
| 382 | +✅ Performance impact < 1% on existing benchmarks |
| 383 | +✅ Documentation clearly explains unbounded float handling |
| 384 | + |
| 385 | +--- |
| 386 | + |
| 387 | +## Contact |
| 388 | + |
| 389 | +When implementing this in Selen, please update this document with: |
| 390 | +- ✅ Implementation approach chosen (Option 1, 2, or other) |
| 391 | +- ✅ File locations modified |
| 392 | +- ✅ Test cases added |
| 393 | +- ✅ Any API changes or breaking changes |
| 394 | + |
| 395 | +Then return to Zelen project and remove the workaround. |
0 commit comments