non_dominated_sort.bend
unified-nsga-iii@0.2.0.0 · 283 lines · 0 definitions
1# NonDominatedSort — C# Unsga3.Core.NonDominatedSort.
2# Fast non-dominated sorting by peeling (Deb et al.).
3# `sort` uses Deb constraint-domination: feasible beats infeasible;
4# both infeasible and unequal CV → smaller CV; equal CV is mutual
5# non-domination (objectives are not compared). Both feasible → Pareto.
6# `dominates` stays the Pareto predicate (law dominates_irreflexive).
7# Zero constraints (cv 0) keeps today's Pareto fronts.
8#
9# Layout (Bend guide: Arrays cannot ride a fork tree; List.get is a
10# cons walk): one sequential pass materializes `Row{index, objectives, cv}`
11# so the peel never `List.get`s a fat Individual. Per-candidate split
12# still mid-splits `a b = f(lo) f(hi)` (same front/leftover order as
13# the tail-first walk). Inner is_dominated stays a sequential OR so a
14# first hit skips the rest. Same ranks and index order when every cv is 0.
15
16import Base
17import unified-nsga-iii@0.2.0.0/individual.bend as Ind
18import unified-nsga-iii@0.2.0.0/util.bend as Util
19
20# One sort-row: population index plus the objective vector. Built once
21# per `sort`; leftover peels reuse the same rows (no re-index).
22type Row is Data:
23 Row{
24 i: Nat
25 f: List<&2, F32>
26 cv: F32
27 }
28
29def row_idx(r: Row) -> Nat:
30 match r:
31 case Row{i, f, cv}:
32 i
33
34def row_f(r: Row) -> List<&2, F32>:
35 match r:
36 case Row{i, f, cv}:
37 f
38
39def row_cv(r: Row) -> F32:
40 match r:
41 case Row{i, f, cv}:
42 cv
43
44def rows_of.go(pop: List<&2, Ind.Individual>, +i: Nat) -> List<&2, Row>:
45 match pop:
46 case Nil{}:
47 Nil{}
48 case +h <> t:
49 Row{i, Ind.objectives(h), Ind.constraint_violation(h)} <> rows_of.go(t, 1n+i)
50
51def rows_of(+pop: List<&2, Ind.Individual>) -> List<&2, Row>:
52 rows_of.go(pop, 0n)
53
54def row_idxs(rs: List<&2, Row>) -> List<&2, Nat>:
55 match rs:
56 case Nil{}:
57 Nil{}
58 case +r <> t:
59 row_idx(r) <> row_idxs(t)
60
61def verdict.a(bb: Bool) -> Nat:
62 match bb:
63 case True{}:
64 0n
65 case False{}:
66 1n
67
68def verdict.b(bb: Bool) -> Nat:
69 match bb:
70 case True{}:
71 2n
72 case False{}:
73 0n
74
75# Minimization: 0n = mutual non-domination, 1n = a dominates b, 2n = b dominates a.
76def verdict(ab: Bool, bb: Bool) -> Nat:
77 match ab:
78 case True{}:
79 verdict.a(bb)
80 case False{}:
81 verdict.b(bb)
82
83def compare_pareto.go(a: List<&2, F32>, b: List<&2, F32>, ab: Bool, bb: Bool) -> Nat:
84 # Unequal lengths: mutual non-domination (0), even if the shared prefix
85 # is strictly better. C# ComparePareto throws. ZDT/DTLZ use one length.
86 # Locked by src/nds_unequal.bend.
87 match a b:
88 case Nil{} Nil{}:
89 verdict(ab, bb)
90 case +x <> xs +y <> ys:
91 compare_pareto.go(xs, ys, Bool.or(ab, F32.is_lt(x, y)), Bool.or(bb, F32.is_lt(y, x)))
92 case Nil{} y <> ys:
93 0n
94 case x <> xs Nil{}:
95 0n
96
97def compare_pareto(a: List<&2, F32>, b: List<&2, F32>) -> Nat:
98 compare_pareto.go(a, b, False{}, False{})
99
100# Equal CV among infeasible points: 0. Deb does not Pareto-compare.
101# C# CompareConstraintDominated on published main falls through to
102# Pareto; this tree does not (Deb / constraint-domination target).
103def compare_cd.infeas(+cva: F32, +cvb: F32, a_lt: Bool, b_lt: Bool) -> Nat:
104 match a_lt:
105 case True{}:
106 1n
107 case False{}:
108 match b_lt:
109 case True{}:
110 2n
111 case False{}:
112 0n
113
114# 0 mutual, 1 a dominates b, 2 b dominates a.
115# Feasible (cv ≤ 0) beats infeasible. Both feasible → Pareto,
116# including unequal objective lengths (mutual non-domination).
117def compare_cd.feas(
118 +fa: List<&2, F32>,
119 +fb: List<&2, F32>,
120 +cva: F32,
121 +cvb: F32,
122 a_feas: Bool,
123 b_feas: Bool
124) -> Nat:
125 match a_feas b_feas:
126 case True{} True{}:
127 compare_pareto(fa, fb)
128 case True{} False{}:
129 1n
130 case False{} True{}:
131 2n
132 case False{} False{}:
133 compare_cd.infeas(cva, cvb, F32.is_lt(cva, cvb), F32.is_lt(cvb, cva))
134
135def compare_cd(+fa: List<&2, F32>, +fb: List<&2, F32>, +cva: F32, +cvb: F32) -> Nat:
136 compare_cd.feas(fa, fb, cva, cvb, F32.is_le(cva, 0.0), F32.is_le(cvb, 0.0))
137
138def compare_constraint(+a: Ind.Individual, +b: Ind.Individual) -> Nat:
139 compare_cd(Ind.objectives(a), Ind.objectives(b), Ind.constraint_violation(a), Ind.constraint_violation(b))
140
141def dominates.is1(p: Nat) -> Bool:
142 match p:
143 case 0n:
144 True{}
145 case 1n+q:
146 False{}
147
148def dominates.fin(c: Nat) -> Bool:
149 match c:
150 case 0n:
151 False{}
152 case 1n+p:
153 dominates.is1(p)
154
155# Pareto only. Irreflexivity is closed in PROOF.bend on this predicate.
156# `sort` uses compare_cd, not this function.
157def dominates(a: Ind.Individual, b: Ind.Individual) -> Bool:
158 dominates.fin(compare_pareto(Ind.objectives(a), Ind.objectives(b)))
159
160def dominates_ff(+fa: List<&2, F32>, +fb: List<&2, F32>) -> Bool:
161 dominates.fin(compare_pareto(fa, fb))
162
163def dominates_cd(+fa: List<&2, F32>, +cva: F32, +fb: List<&2, F32>, +cvb: F32) -> Bool:
164 dominates.fin(compare_cd(fa, fb, cva, cvb))
165
166# Sequential OR so a first hit can skip the rest. Candidate-level
167# parallelism lives in split_walk (coarse mid-split). Walks `all`
168# rows directly — no List.get into the population.
169def is_dominated(+all: List<&2, Row>, +i: Nat, +fi: List<&2, F32>, +cvi: F32) -> Bool:
170 match all:
171 case Nil{}:
172 False{}
173 case +r <> rs:
174 match r:
175 case Row{+j, +fj, +cvj}:
176 Bool.or(
177 Bool.and(Bool.not(Nat.is_eq(i, j)), dominates_cd(fj, cvj, fi, cvi)),
178 is_dominated(rs, i, fi, cvi)
179 )
180
181def row_dom(+all: List<&2, Row>, +r: Row) -> Bool:
182 match r:
183 case Row{+i, +f, +cv}:
184 is_dominated(all, i, f, cv)
185
186# Split remaining into (front indices, leftover rows). Same front
187# membership and leftover order as the old index-list peel.
188# |front| + |leftover| = |remaining| by construction.
189type Split is Data:
190 Split{
191 ff: List<&2, Nat>
192 ot: List<&2, Row>
193 }
194
195def split_put(+r: Row, s: Split, dominated: Bool) -> Split:
196 match s:
197 case Split{ff, ot}:
198 match dominated:
199 case True{}:
200 Split{ff, r <> ot}
201 case False{}:
202 Split{row_idx(r) <> ff, ot}
203
204def split_cat(a: Split, b: Split) -> Split:
205 match a b:
206 case Split{ff1, ot1} Split{ff2, ot2}:
207 Split{List.append(&2, Nat, ff1, ff2), List.append(&2, Row, ot1, ot2)}
208
209# Per-candidate split is independent given `all`. Mid-split then
210# concatenate fronts / leftovers so order matches the tail-first walk.
211def split_walk.go(+all: List<&2, Row>, +fuel: Nat, cand: List<&2, Row>) -> Split:
212 match fuel cand:
213 case 0n Nil{}:
214 Split{Nil{}, Nil{}}
215 case 0n +r <> rest:
216 split_put(r, split_walk.go(all, 0n, rest), row_dom(all, r))
217 case 1n+p Nil{}:
218 Split{Nil{}, Nil{}}
219 case 1n+p +r <> Nil{}:
220 split_put(r, Split{Nil{}, Nil{}}, row_dom(all, r))
221 case 1n+p h <> t:
222 +xs = {h <> t : List<&2, Row>}
223 +mid = Nat.div(Util.list_len(Row, xs), 2n)
224 lo hi = split_walk.go(all, p, List.take(&2, Row, xs, mid)) split_walk.go(all, p, List.drop(&2, Row, xs, mid))
225 split_cat(lo, hi)
226
227def split_walk(+all: List<&2, Row>, +cand: List<&2, Row>) -> Split:
228 split_walk.go(all, Util.list_len(Row, cand), cand)
229
230# Empty first front (unreachable on a finite Pareto set) keeps the head
231# so peel stays a partition.
232def split_ne(+r: Row, +rest: List<&2, Row>, s: Split) -> Split:
233 match s:
234 case Split{ff, ot}:
235 match ff:
236 case Nil{}:
237 Split{row_idx(r) <> Nil{}, rest}
238 case h <> t:
239 Split{h <> t, ot}
240
241def split_front(remaining: List<&2, Row>) -> Split:
242 match remaining:
243 case Nil{}:
244 Split{Nil{}, Nil{}}
245 case +r <> +rest:
246 split_ne(r, rest, split_walk(r <> rest, r <> rest))
247
248def split_fst(s: Split) -> List<&2, Nat>:
249 match s:
250 case Split{ff, ot}:
251 ff
252
253def split_snd(s: Split) -> List<&2, Row>:
254 match s:
255 case Split{ff, ot}:
256 ot
257
258def peel(fuel: Nat, remaining: List<&2, Row>) -> List<&2, List<&2, Nat>>:
259 match fuel remaining:
260 case 0n Nil{}:
261 Nil{}
262 case 1n+f Nil{}:
263 Nil{}
264 case 0n +r <> +rest:
265 row_idxs({r <> rest : List<&2, Row>}) <> Nil{}
266 case 1n+f +r <> +rest:
267 +s = split_front({r <> rest : List<&2, Row>})
268 split_fst(s) <> peel(f, split_snd(s))
269
270def sort(population: List<&2, Ind.Individual>) -> List<&2, List<&2, Nat>>:
271 match population:
272 case Nil{}:
273 Nil{}
274 case +h <> +t:
275 +rs = rows_of.go({h <> t : List<&2, Ind.Individual>}, 0n)
276 peel(Util.list_len(Row, rs), rs)
277
278def front_index_count(fronts: List<&2, List<&2, Nat>>) -> Nat:
279 match fronts:
280 case Nil{}:
281 0n
282 case h <> t:
283 Nat.add(Util.list_len(Nat, h), front_index_count(t))