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