## Choice

Choice construct is now available in Souffle to support the notion of non-determinism. With choice, it is now much easier to express worklist algorithm in Souffle by specifying functional dependencies on the relations.

A functional dependency `x -> y` on relation `R(x:number, y:number)` means that each `x` in `R` will uniquely define a value of `y`. For example, during the computation, if a set of tuples `{(1,1), (1,2), (1,3)}` are about to be inserted into `R`, Souffle only chooses arbitrary one of them (hence the “non-determinism”), since inserting more than one would break the functional dependency.

Functional dependency can be enforced on relation using the keyword `choice-domain` during relation declaration in Souffle with the following syntax:

``````<relation-declaration>      ::= ".decl" <relation-name> "(" <attributes> ")" <choice-domain>
<choice-domain>             ::= "" | "choice-domain" <constraint> { "," <constraint>}
<constraint>                ::= <variable> | "(" <variable> { "," <variable> } ")"
``````

Note here, for the sake of brevity, our syntax omits the co-domain (i.e. the right hand side of the arrow). Therefore, a choice-domain `D` for a relation with attribute set `X` implicitly defines a functional dependency of `D -> X \ D`.

## Examples

### Spanning Tree

``````.decl edge(u:symbol, v:symbol)
.decl st(u:symbol, v:symbol) choice-domain v
.decl startNode(x:symbol)

st("root", x) :- startNode(x).
st(u, v) :- st(_, v), edge(u, v).
``````

The above program calculates a spanning tree on a connected component of an undirected graph. The first rule simply chooses a start node. The second rule states that, an edge `(u, v)` is in the spanning tree: if `v` is reachable in the spanning tree and there is an edge between `u` and `v`. The `choice-domain v` on `st` ensures that the value of `v` is unique, i.e., each node can be visited only once in the spanning tree.

### Eligible advisors

``````.decl student (s:symbol, majr:symbol, year:number)
.decl professor (s:symbol, majr:symbol)
.decl advisor (s:symbol, year:number, p:symbol) choice-domain (s, year)

advisor(s, y, p) :- student(s, y, m), professor(p, m).
``````

The above program allocates an advisor for each student. The `choice-domain (s, year)` on `advisor` makes sure that the combination of `(student, year)` is unique, i.e., student from each year is assigned to a professor only once.

### Total order.

``````.decl d(x:symbol)
.decl list(prev:symbol, next:symbol) choice-domain prev, next

list(p, n) :- d(n), list(_, p).
``````

Given an unordered set of elements, the above program assigns them into a list, effectively computes a total order over the set. The rule states that, `p` is before `e` if `p` is already assigned into the total order list. With the help of the two choice-domains `prev` and `next`: `prev` makes sure that for each element, there can only be one unique element after it; similarly, `next` makes sure for each element, there can be only one unique element before it. Those constraints defines the property of a total order set.