I love constraint programming. It allows you to code very close to the original spec. There are differences between systems though. Z3 might have a good raw performance, but using it feels like programming in "two worlds". In contrast, Picat or Prolog integrate seamlessly with constraints. I did a talk about constraint programming with Scryer Prolog here (Spanish audio): https://www.youtube.com/watch?v=c_yP_kr7DxI