Picat the language is pretty cute but the really impressive part of Picat to me is their CP solver.

It's one of the best in recent years, despite using just eager compilation to SAT rather than lazy clause generation or another fancy hybrid technique.

It went against the grain by using encodings with smaller size that have poor propagation properties (like encoding numbers into binary with adder circuits) but then threw all sorts of compiler tech at the problem to optimize the circuits as much as possible.

It paid off it sure seems like.