 aleksandarmilicevic.github.io Go back Open original

# Alloy*: A Higher-Order Relational Constraint Solver

The formulation of Turan's theorem states that a `k+1`-free graph with `n` nodes can maximally have `(k-1)n2/(2k)` edges. A graph is `k+1`-free if it contains no clique with `k+1` nodes (a clique is a subset of nodes in which every two nodes are connected by an edge); this is equivalent to saying that its maximum clique has exactly `k` nodes. A formalization of Turan's theorem in Alloy is given in the figure on the right.

The formalization of the `maxClique` property is higher-order, because it quantifies over all possible sets of `Node`s to assert that there does not exist another set of nodes which is a `clique` and has more nodes than the max-clique. Higher-order specifications are expressible in Alloy, but the official Alloy Analyzer is not powerful enough to analyze them. In Alloy*, in contrast, this check can be automatically performed to confirm that no counterexample can be found within the specified scope.

There are two ways to now formalize Turan's theorem (the `Turan_dom_constr` and `Turan_classical` commands). In both cases, the idea is to asserts that for all possible `edge` relations (from `Node` to `Node`) that are symmetric and irreflexive, if the max-clique in that graph has `k` nodes (`k=#mClq`), the number of selected edges (`e=(#edges).div`) must be at most `(k-1)n2/(2k)` (the number of tuples in `edges` is divided by `2` because the graph in setup of the theorem in undirected). The differences, although syntactic, have significant impact on performance:

classical
the classical way to constrain the domain of a universal quantifier (e.g., all edges that are symmetric and irreflexive) is to use an implication in the quantifier body; similarly, to constraint the domain of an existential quantifier (e.g., some set of nodes that is max-clique), a conjunction in the body is used.
with domain
constraints
for an efficient CEGIS implementation, we prefer domain constraints to be given explicitly (as opposed to merged and inlined in the quantifier body) using the newly introduced `when` clause (not available in standard Alloy).
 command\scope 5 6 7 8 9 10 `Turan_classical` 4s 10s 43s to to to `Turan_dom_constr` 0.3s 3s 6s 10s 44s 170s comparison of analysis times for various scopes
```some sig Node {} // between every two nodes there is an edge
pred clique[edges: Node -> Node, clq: set Node] { all disj n1, n2: clq | n1 -> n2 in edges
} // no other clique with more nodes
pred maxClique[edges: Node -> Node, clq: set Node] { clique[edges, clq] no cq2: set Node | cq2!=clq && clique[edges,cq2] && #cq2>#clq
} // symmetric and irreflexive
pred edgeProps[edges: Node -> Node] { (~edges in edges) and (no edges & iden)
} // max number of edges in a (k+1)-free graph with n
// nodes is (k-1)n^2/(2k)
check Turan_dom_constr { all edges: Node -> Node when edgeProps[edges] | some mClq: set Node when maxClique[edges, mClq] | let n = #Node, k = #mClq, e = (#edges).div | e <= k.minus.mul[n].mul[n].div.div[k]
}for 7 but 0..294 Int -- checks in ~6s // same as above, but with inlined domain constraints
check Turan_classical { all edges: Node -> Node | edgeProps[edges] implies { some mClq: set Node { maxClique[edges, mClq] let n = #Node, k = #mClq, e = (#edges).div | e <= k.minus.mul[n].mul[n].div.div[k] } }
} for 7 but 0..294 Int -- checks in ~43s
```