If you want a language for expressing constraint satisfaction problems that's higher-level than SAT, I think MiniZinc is pretty interesting. https://www.minizinc.org/