Unnesting function dramatically improves propagation

[JoD]

In attachment the eindwerktoekenning specification. Changing line 39 from

!s: HasPreference(s,AssignedTo(s)).

to

!s t: AssignedTo(s)=t => HasPreference(s,t).

reduces the number of unknown atoms from 1 million to 2300. Approximation doesn't like nested functions?

[JoD]

changing

!s1 s2: StudentProposal(AssignedTo(s1)) & AssignedTo(s2)=AssignedTo(s1) => s1=s2.

to

!s1 s2 t: StudentProposal(t) & t=AssignedTo(s1) & t=AssignedTo(s2) => s1=s2.

further reduces the search space to 500 atoms.

[Broes De Cat]

First part of the issue: we typically do existential unnesting (always safe). Problem: might introduce context switches and hence new Tseitins. Solutions: track context and/or do both unnestings and keep the smallest one (simpler code?)

Second part: unnesting does not recognize identical terms and does multiple unnestings or introduce multiple cp variables.