Have to add to obvious ones: prolog. Almost every prolog comes now with a sat solver.

With prolog it's usually easiest to formulate a problem. Efficient solutions are a bit of a black art though: https://www.metalevel.at/prolog/horror