Use of Z3 smt solver with Python api to solve the Survo puzzle