Disclaimer: I'm not an expert so anything down here may be wrong. The "most basic" form of solver in this world is a SAT solver: it takes a logic formula of co

Disclaimer: I'm not an expert so anything down here may be wrong. The "most basic" form of solver in this world is a SAT solver: it takes a logic formula of conjunctions and disjunctions (ANDs and/or ORs), defined over binary variables, and either finds an assignment to the variables that satisfies it or states that there is no such assignment (the formula cannot be satisfied). From this simple case, you can expand in several directions: a) Accept first order logic formulas (adds "forall" ∀, "exists" ∃, and "implication" → to the formulas). b) Accept formulas with variables of other types/(theories), such as integers, floats, sets. These are known as satisfiability modulo theories (SMT) solvers. c) Accept relational algebra operators (projection, selection, join, etc.) d) ... anything you can think of that makes solving your particular problem more efficient. All of these extensions can be "translated" to a SAT problem/formula. The issue is that the translated formula often grows exponentially (i.e.: add one variable to an SMT formula, and you get "times n" variables in the SAT translation). The advantage of these "specialized" forms of solvers is twofold: 1) They receive better semantical information about the problem, and hence can use more compact representations and optimization tricks that the non-specialized solvers cannot use. 2) They make it easier for users to specify their problems (this could be solved by an automated translator though). Now that we have a way to reason about what different constraint solvers are and how they relate to each other, we can translate "Alloy* : A Higher-Order Relational Constraint Solver" to "a constraint solver that exploits relational operators and higher-order constraints". "First order" is ∃, ∀, etc. above, "Higher order" is ∀∃, ∃∀, etc. treated as a semantically distinct case that allows for better optimizations. Of course, these specializations are (usually) not done just because they are fun to do. They are developed as ongoing efforts to use constraint solving techniques to solve actual problems. In this case they highlight Alloy* as a solver for: - Optimization problems (meeting scheduling, planning, etc.) - Model checking / program verification. - Program generation.