I've been exploring SMT solvers and the SMT-LIB standard, which provides a declarative language for defining problems in terms of logical formulas and constraints. My understanding is that SMT solvers essentially "solve constraints" specified in this language.
This seems very similar to constraint programming, where constraints are defined and a system finds solutions that satisfy them, without explicitly coding the solving process. However, I’ve noticed that people don’t usually refer to SMT-LIB as part of the constraint programming paradigm. Atleast from the articles and papers I read.
Does the SMT-LIB language fit within the constraint programming paradigm, or is it categorized differently? Are there key distinctions between SMT-LIB and traditional constraint programming languages?
In general, SMTLib is not really intended to be a programming-language. That is, end-users are not expected to directly program using SMTLib. It doesn't have usual programming-language like constructs to be suitable for end-user programming.
It is, however, intended to be lingua-franca for other tools to use that require SAT/SMT based solver capabilities. That is, a common language that all different SMT-solvers understand.
In this sense, I'd say SMTLib is not a constraint-programming language. It simply provides a format for expressing constraints in a way that is supported by a variety of solvers. (z3, yices, MathSAT, CVC5 etc.) Actual constraint-programming languages (or other programs/libraries) can take advantage of the common SMTLib language so they can utilize SMT-solvers to resolve constraints in their own domains.
Of course, this is opinion based. But my take would be SMT-Lib is an intermediate-representation that provides a bridge from arbitrary programming languages to SMT-solvers; as opposed to a constraint-programming language itself. (But it is also true that people use it to that effect with great efficacy.)