reified and half-reified predicates

Question

It has been recently brought to my attention that some recent version of FlatZinc supports half-reified predicates:

Half-reified predicates essentially represent constraints that are implied by a Boolean variable rather than being equivalent to one.

source: docs

Q:

• do all global predicates have a _reif version now?
• do all global predicates have a _imp version too?

Looking at the content of share/minizinc/ I can see that inside std only nosets.mzn uses _imp predicates, so my impression is that it is not yet mandatory to support _imp predicates. Q: Is this correct?

Looking at the docs, I found this:

Solver libraries should therefore provide reified versions of constraints whenever possible. The library contains files fzn__reif.mzn for this purpose.

source: docs

If I interpret it correctly, it is not necessary to support _reif predicates because they are already redefined in share/minizinc (although it can be beneficial for performance). Q: Is this correct?

Answer 1

Most often predicates (calls), R(...), are used as an actual constraint: constraint R(...). The question when processing the expression R(...) is now if it can be given directly to the solver or if it has a redefinition that needs to be evaluated.

If the predicate is used in a more complex expression B \/ R(...), then we cannot just give the solver the call R(...) because we don't want to enforce R(...). Instead we want to know if the relationship described by R(...) holds. This is what we call a reification.

For this reason, there must be a R_reif(..., r) predicate that forces r <-> R(...). Essentially this give the truth value of R(...). Again, when the compiler is given the expression R_reif(...,r), then it will see if it can be given directly to the solver or if there is a redefinition available. If both of these are unavailable, then the compiler will try to generate a redefinition from the redefinition of R(...). If this also fails, then the compiler will stop the compilation.

If we look back at our example, B \/ R(...), then one might note that using r <-> R(...) is more than what is necessary. If R(...) is false, then we still need B to be true and if B is false we still want to force R(...); however, we know that nothing will force R(...) to become false. We say R(...) is in a positive context. In this case that means that having r -> R(...) is enough. This is referred to as a half-reification.

In MiniZinc it is possible to introduce a R_imp(..., r) predicate to provide a separate half-reified predicate. This can again be something that is directly passed into the solver or a redefinition. If the compiler has to reify a expression R(...) and sees that it is in a positive context, then it will try first to see if it can find R_imp(..., r) and otherwise fall-back to R_reif(..., r). Note that if a redefinition is generated, then the context of the call propagates inward and half reifications can still occur in the redefinition.

To summarise and answer your questions directly:

• All global predicates can be reified. A redefinition of the _reif can be defined explicitly or can be generated through the generation from their redefinition.
• None of the globals are half-reified. This is not necessary since half-reifications can still be triggered when generating redefinitions of reifications and there are currently no known cases where an explicit half-reified definition performs better.
• There are no currently half-reified predicates that have required solver support. Note however that any _reif predicate that can be implemented as _imp by the solver (including FlatZinc builtins).
• It is not required to support any global _reif predicates; however, there are several required _reif predicates in the FlatZinc builtins that do need support. If these predicates are not redefined or implemented by the solver, then the solver cannot support the generated FlatZinc.