I was wondering if we can redefine it as a constraint problem with exact solutions in z3 or something