1 /*
2 * Copyright 2017-2018 Tom van Dijk, Johannes Kepler University Linz
3 *
4 * Licensed under the Apache License, Version 2.0 (the "License");
5 * you may not use this file except in compliance with the License.
6 * You may obtain a copy of the License at
7 *
8 * http://www.apache.org/licenses/LICENSE-2.0
9 *
10 * Unless required by applicable law or agreed to in writing, software
11 * distributed under the License is distributed on an "AS IS" BASIS,
12 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13 * See the License for the specific language governing permissions and
14 * limitations under the License.
15 */
16
17 #include <iomanip>
18
19 #include "qpt.hpp"
20
21 #define ODDFIRST 0
22
23 namespace pg {
24
QPTSolver(Oink * oink,Game * game)25 QPTSolver::QPTSolver(Oink *oink, Game *game) : Solver(oink, game)
26 {
27 }
28
~QPTSolver()29 QPTSolver::~QPTSolver()
30 {
31 }
32
33 /**
34 * Returns true if a progress measure "a" is less than "b",
35 * given progress measures of <k> components for player <pl>
36 */
37 static bool
pm_less(int * a,int * b,int k,int pl)38 pm_less(int* a, int* b, int k, int pl)
39 {
40 // remember: _ < 5 < 3 < 1 < 0 < 2 < 4 < 6 (even measures, solving for odd)
41 // remember: _ < 6 < 4 < 2 < 0 < 1 < 3 < 5 (odd measures, solving for even)
42
43 for (int i=0; i<k; i++) {
44 // if equal, then continue with next
45 if (a[i] == b[i]) continue;
46 // cases where a[i] is _ or b[i] is _
47 if (a[i] == -1) return true;
48 if (b[i] == -1) return false;
49 // case distinction based on parity
50 const bool a_is_pl = (a[i]&1) == pl;
51 const bool b_is_pl = (b[i]&1) == pl;
52 if (a_is_pl) {
53 if (b_is_pl) return a[i] < b[i];
54 else return false;
55 } else {
56 if (b_is_pl) return true;
57 else return a[i] > b[i];
58 }
59 }
60 // they are equal, so not less...
61 return false;
62 }
63
64
65 /**
66 * Compute the value of a progress measure.
67 */
68 static unsigned long
pm_val(int * pm,int k,int pl)69 pm_val(int* pm, int k, int pl)
70 {
71 unsigned long res=0;
72 for (int i=0; i<k; i++) {
73 res <<= 1;
74 if (pm[i] != -1 and (pm[i]&1)==pl) res++;
75 }
76 return res;
77 }
78
79
80 /**
81 * Print out a progress measure <pm> (length <k>) to the given stream
82 */
83 static void
pm_stream(std::ostream & out,int * pm,int k)84 pm_stream(std::ostream &out, int *pm, int k)
85 {
86 for (int i=0; i<k; i++) {
87 if (pm[i] != -1) {
88 if (i == 0) out << "\033[33;1m";
89 out << " " << std::setfill('0') << std::setw(2) << pm[i];
90 if (i == 0) out << "\033[m";
91 }
92 else out << " __";
93 }
94 }
95
96
97 /**
98 * Compute updated progress measure <dst> after seeing priority "d",
99 * given progress measure <src> with length <k> recording <pl> measures.
100 * Returns -1 if dst == src, or the updated component index.
101 */
102 static int
up(int * dst,int * src,int d,int k,int pl)103 up(int *dst, int *src, int d, int k, int pl)
104 {
105 // check if this is a "won" witness
106 // a pm is won if the highest component records a value of parity <pl>
107 if (src[0] != -1 and (src[0]&1) == pl) {
108 for (int i=0; i<k; i++) dst[i] = src[i];
109 return -1;
110 }
111
112 // first compute j for Lemma 3.3
113 int j33 = -1;
114 for (int i=k-1; i>=0; i--) {
115 // start from the end to find longest sequence of <pl> parity
116 if (src[i] != -1 and (src[i]&1) == pl) continue;
117 // ok, src[i] is not of <pl> parity, test the assumption on the other half
118 // (all higher are _ or higher than d)
119 j33 = i;
120 for (int j=i-1; j>=0; j--) {
121 if (src[j] != -1 and src[j] < d) {
122 // not good!
123 j33 = -1;
124 break;
125 }
126 }
127 break;
128 }
129
130 // then compute j for Lemma 3.4
131 int j34 = -1;
132 for (int i=0; i<k; i++) {
133 // start from the begin, find first index where the Lemma applies
134 if (src[i] != -1 and src[i] < d) {
135 j34 = i;
136 break;
137 }
138 }
139
140 // determine best index min(j33, j34) or -1
141 int j = j33 == -1 ? j34 : (j34 == -1 ? j33 : (j33 < j34 ? j33 : j34));
142
143 // compute resulting progress measure
144 for (int i=0; i<j; i++) dst[i] = src[i]; // same before j
145 dst[j] = d;
146 for (int i=j+1; i<k; i++) dst[i] = -1; // _ after j
147
148 return j;
149 }
150
151
152 /**
153 * Compute smallest larger progress measure with dst[0] set to _
154 */
155 static bool
bump(int * dst,int * src,int k,int max,int max_opp,int pl)156 bump(int *dst, int *src, int k, int max, int max_opp, int pl)
157 {
158 // reminder: _ 5 3 1 0 2 4 6...
159 // reminder: _ 6 4 2 0 1 3 5...
160
161 for (int i=k-2; i>=0; i--) {
162 if (src[i] == -1) {
163 // if the current is _, then the smallest increase is max_opp
164 dst[i] = max_opp;
165 for (int z=0; z<i; z++) dst[z] = src[z];
166 for (int z=i+1; z<k; z++) dst[z] = -1;
167 return true;
168 } else if ((src[i]&1) != pl) {
169 // if the current is of opponent parity, then subtract 2 OR change parity
170 if (src[i] > (1-pl)) {
171 // if odd != 1 / even != 0 then we can just subtract 2 and we are done
172 dst[i] = src[i]-2;
173 for (int z=0; z<i; z++) dst[z] = src[z];
174 for (int z=i+1; z<k; z++) dst[z] = -1;
175 return true;
176 } else if (i > 0 and src[i-1] >= pl) {
177 // if is 1/0, then can set to 0/1 if the previous is set and we're not highest...
178 dst[i] = pl;
179 for (int z=0; z<i; z++) dst[z] = src[z];
180 for (int z=i+1; z<k; z++) dst[z] = -1;
181 return true;
182 }
183 } else {
184 // if it's of parity <pl>, and the next one is higher, then increase and done
185 // probably the only one that is relevant, since this algorithm is used
186 // when an "even" sequence must be bumped
187 if ((src[i]+2) <= max and i > 0 and src[i-1] >= (src[i]+2)) {
188 dst[i] = src[i]+2;
189 for (int z=0; z<i; z++) dst[z] = src[z];
190 for (int z=i+1; z<k; z++) dst[z] = -1;
191 return true;
192 }
193 }
194 }
195 // did not find a higher progress measure
196 return false;
197 }
198
199
200 /**
201 * Perform antagonistic update.
202 * Return "true" if dst != src, "false" otherwise.
203 */
204 static bool
au(int * dst,int * src,int d,int k,int max,int maxopp,int pl)205 au(int *dst, int *src, int d, int k, int max, int maxopp, int pl)
206 {
207 // first compute normal update
208 int j = up(dst, src, d, k, pl);
209 if (j == -1) return false; // no difference, already smallest...
210
211 // then compute antagonistic update and update the antagonistic measure
212 int tmp[k];
213 if (!bump(tmp, src, k, max, maxopp, pl)) return true; // no bump possible; but dst != src so return true
214 up(tmp, tmp, d, k, pl);
215
216 // use smallest updated measure
217 if (pm_less(tmp, dst, k, pl)) {
218 for (int i=0; i<k; i++) dst[i] = tmp[i];
219 }
220
221 // finally, check if different
222 for (int i=0; i<k; i++) if (dst[i] != src[i]) return true;
223 return false;
224 }
225
226
227 bool
lift(int v,int target)228 QPTSolver::lift(int v, int target)
229 {
230 // check if already Top
231 int * const pm = pm_nodes + k*v; // obtain ptr to current progress measure
232 if (pm[0] != -1 and (pm[0]&1) == pl) return false;
233
234 const int pr = priority(v);
235 int tmp[k], res[k];
236
237 #ifndef NDEBUG
238 int old_strategy = strategy[v];
239
240 if (trace >= 2) {
241 logger << "\033[37;1mupdating vertex " << label_vertex(v) << (owner(v)?" (odd)":" (even)") << "\033[m with current measure";
242 pm_stream(logger, pm, k);
243 logger << std::endl;
244 }
245 #endif
246
247 // First special cases if we are lifting triggered by a given <target>.
248
249 if (1 and target != -1) {
250 if (owner(v) == pl) {
251 // if owned by <pl>, just check if target is better.
252 au(tmp, pm_nodes + k*target, pr, k, max, maxo, pl);
253 if (pm_val(tmp, k, pl) > goal) tmp[0] = max; // lol
254 #ifndef NDEBUG
255 if (trace >= 2) {
256 logger << "to successor " << label_vertex(target) << ":";
257 pm_stream(logger, pm_nodes + k*target, k);
258 logger << " => ";
259 pm_stream(logger, tmp, k);
260 logger << std::endl;
261 }
262 #endif
263 if (pm_less(pm, tmp, k, pl)) {
264 // target is better, update, report, return
265 for (int i=0; i<k; i++) pm[i] = tmp[i];
266 #ifndef NDEBUG
267 if (trace and target != strategy[v]) {
268 if (strategy[v] == -1) {
269 logger << "\033[1;38;5;208m";
270 logger << "set strategy\033[m of \033[36;1m" << label_vertex(v) << "\033[m to \033[36;1m" << label_vertex(target) << "\033[m\n";
271 } else {
272 logger << "\033[1;38;5;208m";
273 logger << "changed strategy\033[m of \033[36;1m" << label_vertex(v) << "\033[m from \033[36;1m" << label_vertex(strategy[v]) << "\033[m to \033[36;1m" << label_vertex(target) << "\033[m\n";
274 }
275 }
276 strategy[v] = target; // does not matter for algorithm, only for output here
277 #endif
278 #ifndef NDEBUG
279 if (trace) {
280 logger << "\033[1;32mnew measure\033[m of \033[36;1m" << label_vertex(v) << "\033[m:";
281 pm_stream(logger, pm, k);
282 logger << " (to " << label_vertex(target) << ")\n";
283 }
284 #endif
285 return true;
286 } else {
287 // target not better, not checking other directions
288 return false;
289 }
290 } else {
291 // if owned by ~<pl>, test if strategy is target
292 if (strategy[v] != -1 and target != strategy[v]) {
293 return false; // no need to do anything... strategy is still same
294 }
295 }
296 }
297
298 // Compute best measure by going over all successors
299
300 bool first = true;
301 int s_cur = strategy[v];
302 if (s_cur != -1) {
303 // first set to current...
304 au(tmp, pm_nodes + k*s_cur, pr, k, max, maxo, pl);
305 if (pm_val(tmp, k, pl) > goal) tmp[0] = max; // goal reached, lift to Top
306 #ifndef NDEBUG
307 if (trace >= 2) {
308 logger << "to successor " << label_vertex(s_cur) << ":";
309 pm_stream(logger, pm_nodes + k*s_cur, k);
310 logger << " => ";
311 pm_stream(logger, tmp, k);
312 logger << std::endl;
313 }
314 #endif
315 for (int i=0; i<k; i++) res[i] = tmp[i];
316 first = false;
317 }
318 for (auto curedge = outs(v); *curedge != -1; curedge++) {
319 int to = *curedge;
320 if (disabled[to]) continue;
321 if (to == s_cur) continue;
322 au(tmp, pm_nodes + k*to, pr, k, max, maxo, pl);
323 if (pm_val(tmp, k, pl) > goal) tmp[0] = max; // goal reached, lift to Top
324 #ifndef NDEBUG
325 if (trace >= 2) {
326 logger << "to successor " << label_vertex(to) << ":";
327 pm_stream(logger, pm_nodes + k*to, k);
328 logger << " => ";
329 pm_stream(logger, tmp, k);
330 logger << std::endl;
331 }
332 #endif
333 if (first) {
334 first = false;
335 for (int i=0; i<k; i++) res[i] = tmp[i];
336 strategy[v] = to;
337 } else if (owner(v) == pl) {
338 // we want the max
339 if (pm_less(res, tmp, k, pl)) {
340 for (int i=0; i<k; i++) res[i] = tmp[i];
341 strategy[v] = to;
342 }
343 } else {
344 // we want the min
345 if (pm_less(tmp, res, k, pl)) {
346 for (int i=0; i<k; i++) res[i] = tmp[i];
347 strategy[v] = to;
348 }
349 }
350 }
351
352 // now "res" contains the best au
353 if (pm_less(pm, res, k, pl)) {
354 // ok, it's an update
355 for (int i=0; i<k; i++) pm[i] = res[i];
356 #ifndef NDEBUG
357 if (trace and old_strategy != strategy[v]) {
358 if (owner(v) == pl) logger << "\033[1;38;5;208m";
359 else logger << "\033[1;31m";
360 if (old_strategy == -1) {
361 logger << "set strategy\033[m of \033[36;1m" << label_vertex(v) << "\033[m to \033[36;1m" << label_vertex(strategy[v]) << "\033[m\n";
362 } else {
363 logger << "changed strategy\033[m of \033[36;1m" << label_vertex(v) << "\033[m from \033[36;1m" << label_vertex(old_strategy) << "\033[m to \033[36;1m" << label_vertex(strategy[v]) << "\033[m\n";
364 }
365 }
366 if (trace) {
367 logger << "\033[1;32mnew measure\033[m of \033[36;1m" << label_vertex(v) << "\033[m:";
368 pm_stream(logger, pm, k);
369 logger << " (to " << label_vertex(strategy[v]) << ")\n";
370 }
371 #endif
372 return true;
373 } else {
374 #ifndef NDEBUG
375 if (trace and old_strategy != strategy[v]) {
376 if (owner(v) == pl) logger << "\033[1;38;5;208m";
377 else logger << "\033[1;31m";
378 if (old_strategy == -1) {
379 logger << "set strategy\033[m of \033[36;1m" << label_vertex(v) << "\033[m to \033[36;1m" << label_vertex(strategy[v]) << "\033[m\n";
380 } else {
381 logger << "changed strategy\033[m of \033[36;1m" << label_vertex(v) << "\033[m from \033[36;1m" << label_vertex(old_strategy) << "\033[m to \033[36;1m" << label_vertex(strategy[v]) << "\033[m\n";
382 }
383 }
384 #endif
385 return false;
386 }
387 }
388
389
390 void
liftloop()391 QPTSolver::liftloop()
392 {
393 /**
394 * Initialize/reset progress measures / strategy
395 */
396 for (int i=0; i<k*nodecount(); i++) pm_nodes[i] = -1; // initialize all to _
397 for (int i=0; i<nodecount(); i++) strategy[i] = -1;
398
399 /**
400 * Run first lifting loop
401 */
402 for (int n=nodecount()-1; n>=0; n--) {
403 if (disabled[n]) continue;
404 lift_attempt++;
405 if (lift(n, -1)) {
406 lift_count++;
407 #if 0
408 for (int from : in[n]) {
409 if (disabled[from]) continue;
410 lift_attempt++;
411 if (lift(from, n)) {
412 lift_count++;
413 todo_push(from);
414 }
415 }
416 #else
417 todo_push(n);
418 #endif
419 }
420 }
421
422 /**
423 * Lift until fixed point
424 */
425 while (!todo.empty()) {
426 int n = todo_pop();
427 for (auto curedge = ins(n); *curedge != -1; curedge++) {
428 int from = *curedge;
429 if (disabled[from]) continue;
430 lift_attempt++;
431 if (lift(from, n)) {
432 lift_count++;
433 todo_push(from);
434 }
435 }
436 }
437
438 /**
439 * Report final state.
440 */
441 if (trace) {
442 for (int v=0; v<nodecount(); v++) {
443 if (disabled[v]) continue;
444 int *pm = pm_nodes + v*k;
445
446 logger << "\033[1m" << label_vertex(v) << (owner(v)?" (odd)":" (even)") << "\033[m:";
447 pm_stream(logger, pm, k);
448
449 if (pm[0] == -1 or (pm[0]&1) != pl) {
450 if (owner(v) != pl) {
451 if (strategy[v] == -1) logger << " no strategy!";
452 else logger << " => " << label_vertex(strategy[v]);
453 }
454 }
455
456 logger << std::endl;
457 }
458 }
459
460 /**
461 * Derive strategies, mark as solved (only for opponent).
462 */
463 for (int v=0; v<nodecount(); v++) {
464 if (disabled[v]) continue;
465 int *pm = pm_nodes + v*k;
466
467 if (pm[0] == -1 or (pm[0]&1) != pl) {
468 if (owner(v) != pl and strategy[v] == -1) LOGIC_ERROR;
469 oink->solve(v, 1-pl, owner(v) != pl ? strategy[v] : -1);
470 }
471 }
472
473 oink->flush();
474 }
475
476
477 static int
ceil_log2(unsigned long long x)478 ceil_log2(unsigned long long x)
479 {
480 static const unsigned long long t[6] = {
481 0xFFFFFFFF00000000ull,
482 0x00000000FFFF0000ull,
483 0x000000000000FF00ull,
484 0x00000000000000F0ull,
485 0x000000000000000Cull,
486 0x0000000000000002ull
487 };
488
489 int y = (((x & (x - 1)) == 0) ? 0 : 1);
490 int j = 32;
491 int i;
492
493 for (i = 0; i < 6; i++) {
494 int k = (((x & t[i]) == 0) ? 0 : j);
495 y += k;
496 x >>= k;
497 j >>= 1;
498 }
499
500 return y;
501 }
502
503
504 void
updateState(unsigned long & _n0,unsigned long & _n1,int & _max0,int & _max1,int & _k0,int & _k1)505 QPTSolver::updateState(unsigned long &_n0, unsigned long &_n1, int &_max0, int &_max1, int &_k0, int &_k1)
506 {
507 // determine number of even/odd vertices and highest even/odd priority
508 unsigned long n0 = 0;
509 unsigned long n1 = 0;
510 int max0 = -1;
511 int max1 = -1;
512
513 for (int i=0; i<nodecount(); i++) {
514 if (disabled[i]) continue;
515 const int pr = priority(i);
516 if ((pr&1) == 0) {
517 if (pr > max0) max0 = pr;
518 n0++;
519 } else {
520 if (pr > max1) max1 = pr;
521 n1++;
522 }
523 }
524
525 _n0 = n0;
526 _n1 = n1;
527 _max0 = max0;
528 _max1 = max1;
529
530 _k0 = 1+ceil_log2(n0+1);
531 _k1 = 1+ceil_log2(n1+1);
532 }
533
534 void
run()535 QPTSolver::run()
536 {
537 unsigned long goal0, goal1;
538 int max0, max1;
539 int k0, k1;
540
541 updateState(goal0, goal1, max0, max1, k0, k1);
542
543 logger << "for odd with even measures: n0=" << goal0 << ", k=" << k0 << std::endl;
544 logger << "for even with odd measures: n1=" << goal1 << ", k=" << k1 << std::endl;
545
546 // for allocation, just use biggest k
547 int big_k = k0 > k1 ? k0 : k1;
548
549 // now create the data structure, for each vertex a PM
550 pm_nodes = new int[big_k * nodecount()];
551 strategy = new int[nodecount()];
552
553 // initialize todo/dirty queues
554 todo.resize(nodecount());
555 dirty.resize(nodecount());
556
557 lift_count = 0;
558 lift_attempt = 0;
559
560 if (bounded) {
561 int i;
562 for (i=1; i<=big_k; i++) {
563 long _l = lift_count, _a = lift_attempt;
564 uint64_t _c = game->count_unsolved();
565 uint64_t c = _c;
566
567 /*if (i <= k0)*/ {
568 pl = 0;
569 k = i;
570 max = max0;
571 maxo = max1 != -1 ? max1 : 0; // used in bump
572 goal = goal0;
573 liftloop();
574
575 c = game->count_unsolved();
576 logger << "after even with k=" << k << ", " << std::setw(9) << lift_count-_l << " lifts, " << std::setw(9) << lift_attempt-_a << " lift attempts, " << c << " unsolved left." << std::endl;
577 if (c == 0) break;
578
579 if (c != _c) updateState(goal0, goal1, max0, max1, k0, k1);
580 _l = lift_count;
581 _a = lift_attempt;
582 }
583 /*if (i <= k1)*/ {
584 pl = 1;
585 k = i;
586 max = max1;
587 maxo = max0 != -1 ? max0 : 1; // used in bump
588 goal = goal1;
589 liftloop();
590
591 c = game->count_unsolved();
592 logger << "after odd with k=" << k << ", " << std::setw(9) << lift_count-_l << " lifts, " << std::setw(9) << lift_attempt-_a << " lift attempts, " << c << " unsolved left." << std::endl;
593 if (c == 0) break;
594
595 if (c != _c) updateState(goal0, goal1, max0, max1, k0, k1);
596 }
597 if (c != _c) i--;
598 }
599
600 logger << "solved with " << lift_count << " lifts, " << lift_attempt << " lift attempts, max k " << i << "." << std::endl;
601 } else if (ODDFIRST) {
602 pl = 1;
603 k = k1;
604 max = max1;
605 maxo = max0 != -1 ? max0 : 1; // used in bump
606 goal = goal1;
607 liftloop();
608
609 uint64_t c = game->count_unsolved();
610 logger << "after odd, " << lift_count << " lifts, " << lift_attempt << " lift attempts, " << c << " unsolved left." << std::endl;
611
612 if (c != 0) {
613 updateState(goal0, goal1, max0, max1, k0, k1);
614
615 pl = 0;
616 k = k0;
617 max = max0;
618 maxo = max1 != -1 ? max1 : 0; // used in bump
619 goal = goal0;
620 liftloop();
621 }
622
623 logger << "solved with " << lift_count << " lifts, " << lift_attempt << " lift attempts." << std::endl;
624 } else {
625 pl = 0;
626 k = k0;
627 max = max0;
628 maxo = max1 != -1 ? max1 : 0; // used in bump
629 goal = goal0;
630 liftloop();
631
632 uint64_t c = game->count_unsolved();
633 logger << "after even, " << lift_count << " lifts, " << lift_attempt << " lift attempts, " << c << " unsolved left." << std::endl;
634
635 if (c != 0) {
636 updateState(goal0, goal1, max0, max1, k0, k1);
637
638 pl = 1;
639 k = k1;
640 max = max1;
641 maxo = max0 != -1 ? max0 : 1; // used in bump
642 goal = goal1;
643 liftloop();
644 }
645
646 logger << "solved with " << lift_count << " lifts, " << lift_attempt << " lift attempts." << std::endl;
647 }
648
649 delete[] pm_nodes;
650 delete[] strategy;
651 }
652
653 }
654