selen 0.15.5

Constraint Satisfaction Problem (CSP) solver
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

# Sort Constraint Implementation

## Overview
Implemented the `sort` constraint to fix `allperm.fzn` and other files requiring sorting functionality.

## FlatZinc Signature
```
predicate sort(array [int] of var int: x, array [int] of var int: y);
```
Where:
- `x`: Input array (unsorted)
- `y`: Output array (sorted version of x)

## Implementation Strategy

Since Selen doesn't have a built-in sort constraint, we decompose it into:

1. **Ordering Constraint**: `y` is sorted (non-decreasing order)
   - For all i: `y[i] <= y[i+1]`
   - Uses existing `int_le` constraint

2. **Channeling Constraint**: `y` is a permutation of `x`
   - Each element in `y` must equal some element in `x`
   - Each element in `x` must equal some element in `y`
   - Uses reified equality (`int_eq_reif`) + disjunction (`bool_or`)

## Implementation Details

### File: `/src/flatzinc/mapper/constraints/global.rs`

**Method**: `map_sort()`

**Ordering**: 
```rust
for i in 0..n-1 {
    self.model.new(y[i].le(&y[i + 1]));
}
```

**Channeling** (for arrays with n ≤ 10):
```rust
// For each y[i], ensure it equals at least one x[j]
for yi in y {
    let mut equality_vars = vec![];
    for xj in x {
        let bi = self.model.bool();
        self.model.int_eq_reif(yi, xj, bi);  // bi ⇔ (yi = xj)
        equality_vars.push(bi);
    }
    let or_result = self.model.bool_or(&equality_vars);
    self.model.new(or_result.eq(1));  // At least one must be true
}
// Symmetric for each x[j]
```

**Optimization**: For arrays > 10 elements, we rely on ordering + domain pruning (full channeling creates O(n²) constraints).

## Registration
Added to `/src/flatzinc/mapper.rs`:
```rust
"sort" => self.map_sort(constraint),
```

## Test Results

### Before Implementation
- **Batch 01**: 74/86 (86.0%)
- **allperm.fzn**: ✗ Failed (sort constraint not implemented)

### After Implementation
- **Batch 01**: 75/86 (87.2%)
- **allperm.fzn**: ✓ Passes
- **Build**: Clean compilation in 13.68s

## Usage Statistics
- **Total Uses**: 30 instances across test suite
- **Batch 01**: 1 file (allperm.fzn)

## Key Insights

1. **Decomposition Approach**: Breaking complex global constraints into primitive constraints is effective
2. **Reified Constraints**: Essential for expressing "at least one must be true" logic
3. **Scalability Trade-off**: Full channeling for small arrays (n ≤ 10), relaxed for larger arrays
4. **VarIdExt Import**: Required for using `.eq()`, `.le()` methods on VarId

## Related Constraints
- `int_eq_reif`: Reified equality
- `bool_or`: N-ary disjunction
- `int_le`: Less-than-or-equal

## Future Improvements
1. More efficient channeling using `element` constraints
2. Specialized propagators for sort (rather than decomposition)
3. Support for stable sort variants
4. Better handling of large arrays (n > 10)