Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
ericpony.github.io
Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
1–10 of 16 posts
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#2Very good to see all this in one short page!
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#3It's worth noting these notes are 11 years old. The first give-away was the comment that in Python 3/2 is an integer, which is indeed true in Python 2 but not in Py3.
For modern users of Z3, you'd want to do `pip install z3-solver` rather than use `Z3Py` mentioned at the very bottom of this doc.
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#4Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#5https://www.hakank.org/z3/
Thank you for the link.
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#6That’s a very clean API.
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#7Solvers are something that still kind of feel like magic to me. I have done a fair amount of Isabelle, and the "sledgehammer" tool in there (which uses solvers to see if an existing proof can be made to work to solve your subgoal) is something that impresses me every single time I use it.
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#8I have created a Python library called "z4-solver" that adds some nice utility functions on top of z3: https://github.com/Tyilo/z4
I always use that instead of the z3-solver directly.
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#9I have created a Python library called "z4-solver" that adds some nice utility functions on top of z3: https://github.com/Tyilo/z4 I always use that instead of the z3-solver directly.
Have you tried to compare Z3 with cvc5? https://cvc5.github.io/docs/cvc5-1.1.2/api/python/pythonic/p...
It offers basically the same API and could be faster in many cases
Re: Z3 API in Python: From Sudoku to N-Queens in Under 20 Lines (2015)
#10I have created a Python library called "z4-solver" that adds some nice utility functions on top of z3: https://github.com/Tyilo/z4 I always use that instead of the z3-solver directly.
Have you tried to compare Z3 with cvc5? https://cvc5.github.io/docs/cvc5-1.1.2/api/python/pythonic/p... It offers basically the same API and could be faster in many cases
I was about to comment the same. Z3 always takes all the credit but cvc5 is just as great!