Technical Background

The underspecification solver in utool is based on the freeness algorithm for dominance graphs defined in Bodirsky et al. 2004. This algorithm goes through a dominance graph and successively chooses a fragment which it can put at the root of a solution. It does this in a clever way, so that it only tries to put things at the root that can actually end up at the root.

Because the original Bodirsky et al. algorithm will sometimes try to solve the same subgraph multiple times, the implementation in utool uses a chart-like data structure for caching intermediate results. It will memoise the solved forms for each subgraph it has already seen, and do nothing when it tries to solve the same subgraph a second time. Interestingly, filling this data structure is extremely cheap. utool spends the vast majority of its runtime on enumerating the actual solved forms from the chart.

Internally, utool solves dominance graphs. We have shown in various papers how different underspecification formalisms can be encoded as dominance graphs: normal dominance constraints, Hole Semantics, Minimal Recursion Semantics. These encodings are implemented in utool in the form of "codecs". It is straightforward to add new codecs to utool, if a formalism is intertranslatable with dominance graphs.

The translation of MRS and Hole Semantics into dominance graphs is only correct on "nets" and "hypernormally connected constraints", respectively. (Nets and hypernormally connected constraints are essentially the same class.) In practice, this means that we need an efficient way of checking whether a constraint is a net (although interestingly, most constraints in practice seem to be nets). Beginning with utool 1.2, you can test whether a description is hypernormally connected by running "utool classify" and checking whether the bit for 16 is set in the exit code.

A more detailed technical description can be found in our recent paper on this topic.