Alloy*: A Higher-Order Relational Constraint Solver

(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?

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).

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.

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)

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.