3 ms·
I got the solution with a straightforward set of assertions in Z3. It was a lot of typing, and I wonder if there's a more succinct way to do this than the foll
by SloopJon 4y ago
I got the solution with a straightforward set of assertions in Z3. It was a lot of typing, and I wonder if there's a more succinct way to do this than the following:
(declare-const blitzen Int)
(declare-const comet Int)
...
(assert
(and
; lower bound for readability (1 is front)
(> blitzen 0)
(> comet 0)
...
; upper bound for readability (9 is rear)
(< blitzen 10)
(< comet 10)
...
; clues from the puzzle
(> vixen rudolph)
...
(< dasher vixen)))