A MiniZinc  version of the graceful labeling model in  was sent to me . This looks actually quite nice, so therefore I reproduce it here:
MiniZinc comes with an IDE so that makes it easy to edit and run the model:
This is solved with the Gecode  Constraint Programming solver.
Generating all solutions is just a question of changing a setting:
Indeed we get all solutions:
- von Koch and Z3, http://yetanothermathprogrammingconsultant.blogspot.com/2017/09/von-koch-and-z3.html
- Mikael Zayenz Lagerkvist, private communication