SMTI (stable marriage problem with incomplete list and ties) solved in z3py. Dev guide Dependencies z3 for python pytest Launching tests: pytest solver_test.py Credits https://github.com/DennisYurichev/SAT_SMT_by_example