You might find Chris Mungall's py-typedlogic interesting:
Re:What Is miniKanren?
by adamgordonbell on Thursday January 02, 2025 @11:07AM
(#42575630)
Thanks! And thanks for miniKanren and reasoned schemer!
If you're interested in SMT solvers, the Z3 bindings for Python are very easy to use.
Hillel Wayne is working on a Logic for Programmers book [0] that might be what you're looking for.
The chapters on both constraint solvers and logic programming are pretty short overviews, we're talking less than 15 pages. I wouldn't recommend it if that's what you're specifically interested in.
For SAT/SMT in Python, I've heard this book is pretty good: https://theory.stanford.edu/~nikolaj/programmingz3.html. Google OR-tools has a Python frontend and they have interactive tutorials (https://developers.google.com/optimization/examples). I don't know about logic programming in Python. Note that while there's some overlap between logic programming and constraint solving ([1] [2]), the communities are pretty independent from each other. Different histories, tools, techniques, etc.
I played with some Scala mini Karen implementations before, but the ones I tried were all half-baked or non-working.