(I'm no expert but..) I recently got into Prolog, and Alloy sounds very similar. So I was asking "How is it different?" Strangely, in the FAQ, no mention of Prolog. I found just this:
>How does the Alloy Analyzer differ from theorem provers?
>The Alloy Analyzer's analysis is fully automatic, and when an assertion is found to be false, the Alloy Analyzer generates a counterexample. It's a "refuter" rather than a "prover".
(i.e. where Prolog would just write "no" if nothing found.) In the Alloy* paper also, no mention of Prolog. To find a counterexample, couldn't you set Prolog to find one?
Prolog is a general programming language with built-in backchaining semantics. It in general does not know how to solve constraints. Indeed if your clauses have loops Prolog will just run in circles until it is out of stack space. The following common rules for equivalence are good examples of valid logic statements that do not work with Prolog's naive execution strategy:
% Symmetry
f(A, B) :- f(B, A).
% Transitivity
f(A, C) :- f(A, B), f(B, C).
Indeed in general finding the symmetric/transitive closure of relations is a very hard problem. Constraint/SAT solvers use heuristics to solve problems like the above and can accept much more declarative specifications than Prolog.
You could try in Prolog. But the other difference is that prolog is. General purpose language (though used in a more specific set of situations). Alloy is not.
Also the search mechanisms are not the same. Prolog uses a backtracking, depth-first search behind the scenes. Alloy does not.
EDIT: I was out earlier and didn't want to make a claim I couldn't verify/backup. Alloy uses a SAT solver behind the scenes to find solutions.
Alloy is a specification language. To verify the specification, the alloy analyser (a model checker) has to artificially create some number of instances and simulate it.
Prolog is an executable language. You, the user, give it a database, and it searches for solutions that satisfies constraints. It doesn't create the basic facts on its own.
There exists a compiler from imperative alloy to prolog to make this transition.
Hmm well, not all Prolog uses fit the 'give it a database' model..(In fact I can't think of any Prolog programs I've seen that do fit it) e.g. I was tried the the finite domain solver in Gnu Prolog[0] recently, I wanted arrangements of about 15 shapes that obeyed certain constraints, the program was 6 very short lines! I didn't tell it anything except the constraints.
But yeah, alloy and alloy* sound fascinating, I must investigate further, thank you.
You are right. Constraint solving in general is a specific area that does not require a knowledge base; instead it is a search for a solution from the specified domain that fits all the specified constraints. Here there is considerable overlap between prolog, alloy and z3.
However, most general prolog programming has the same requirements placed on other executable languages, to transform, store and communicate data. Alloy is not the tool for this aspect.
Prolog is Turing-complete, you can have non-terminating programs in it (and thus there are problems that can be expressed in Prolog that you can never get an answer to), does the same hold true for Alloy? If not I think that it would make more sense to compare Datalog (which I think forces all of its programs to provably terminate) with Alloy rather than Prolog with Alloy.
I've seen constraint solvers used in a couple of contexts.
The first was at a food delivery company where we used one to calculate optimal delivery routes - we'd give it a list of delivery vans available, and a list of deliveries with the distances between those deliveries, along with constraints such as the size of the delivery to be made and capacity of the vans, and the desired delivery times. With that information it would then determine which van deliveries should be in, and what order they should be made in.
The second was a large conference, where it was used to work out the talk schedule given a list of talks, a list of available venues, and any requirements for each talk such as a venue of a certain size, or the need for a projector. It took a while to work things out, but eventually it would either find slots for everyone, or determine that it was impossible to schedule everything within the given constraints. (For the curious it can be found here: https://github.com/emfcamp/slotmachine)
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:
Alloy (and the philosophy it is based on) is explained in Daniel Jackson's book <<Software Abstractions>>, which is a very nice book to read on techniques of specification and verification (at the specification level).
I got that. What exactly is exciting about such verification, especially despite the theoretical complexity, effort, and lack of common use?
I really don't want to insult anyone with these questions. I'm genuinely curious why people spend time on such things and presuppose there are good reasons. I just don't know them yet.
If you have a problem where you need to find a solution that satisfies a set of constraints, or maximises it in some ways. Then you could use constraint solvers to do it.
Those are normally combinatorics related problems/solutions.
A sudoku is a good example of such a problem. You need to find a combination of numbers that satisfy the sudoku constraints.
In general, it is a search optimization. You have a finite set of possible solutions. In sudoku, that would be every combination of integers 1 to 9 given the set of empty squares in the grid.
You could loop over each possible combination, and try them one by one until you find one that satisfies the sudoku constraints (the rules of sudoku in this case). But, this is pretty slow, and generating the set of all combination on its own can be tricky.
A constraint solver helps you to do that, and possibly do it in a way that is smart about which combination it tries first, to arrive at a solution faster.
Generally, it requires some kind of language where you teach it the problem, and define the constraints, in a way that it can solve it for you.
Alloy and Alloy* are used as specification languages, not constraint solvers. There are different speclangs with different specialties, and Alloy is particularly good at domain modeling. Here's an example of an early draft of a spec I've been working on; I'm mostly doing this from memory so there might be some errors.
We have organizations that are being billed. Each bill consists of one or more items, each of which has a vendor that supplied that has to be paid.
sig Org {}
sig Bill {
, client: Org // exactly one
, item: some Item // one or more
}
sig Item {
, vendor: Org
}
If I then generate models, I'll immediately see some weird things. First, multiple bills can share the same item. Second, a bill can have an item that is the same as the client. Whether we want to do the former or not depends on what we're modeling: standardized items or _specific_ instances of an item. Let's assume the former, in which case we're fine with it. The latter is something we never want, but can also guarantee never happens. We'll add a fact showing that.
fact "orgs can't bill themselves" {
all b: Bill |
no i: b.item |
i.vendor = b.client
}
Part two: some items have bills of their own. If you have a line for "labwork", the vendor doing the labwork has their own corresponding items they have to pay to do the labwork. But not all items do.
sig Item {
, vendor: Org
, bill: lone Bill //lone means "optional"
}
But now the models go crazy! They raise all sorts of weird cases:
* We're very clearly mixing "items as an abstract thing" with "bills as a concrete instance" (as they map to the paying org). We need to fix the difference in conceptual levels here.
* What if the vendor of an item is different from the client of the bill? This is probably an inconsistency we should avoid in practice.
* Can two items share the same bill? Maybe! We can't rule this out.
* Should an item be part of its own bill? Almost certainly not.
* We can have an organization O be billed by a vendor V for an item I with a corresponding bill that has O as a vendor! O is getting billed for something they themselves are making money off. This happens all the time in reality and we definitely have to permit it in our model.
After figuring these out we might want to make it even more complex, like having different types of items or disjoint vendor possibilities or make the system dynamic or whatever. But the key thing here is we can explore all of the consequences of the data model without having to run into the issues in production first.
Hillel Wayne has a great series of blog posts on using Alloy to solve software design problems: https://www.hillelwayne.com/tags/alloy/