Preprocessing variables

[EmirDe]

Based on our discussion.

About encoding problems. Say we do circuit decomposition. Depending how exactly MiniZinc generates FlatZinc, it likely produces auxiliary variables that have the meaning x = 1 <-> [y >= 5], essentially the SAT view of atomic constraints. But our solver natively handles atomic constraints. In this case, instead of having the variable x, we could simply have it removed entirely, and operate over atomic constraints. Probably this happens with other models/decompositions, too. For other solvers, this is fine because they anyway have a SAT view. But for us, potentially we can get speed-ups and/or better learning.

Maarten: We should definitely do that...It should be a preprocessing step in our flatzinc reader

We can also preprocess variables using our views, e.g., x = y + 2. We talked about this for a long time but never got to it.

• Preprocess variables that our predicates can capture, e.g., x = 1 <-> [y >= 5]
• Preprocess functionally dependent variables, e.g., x = y + 2

Need to have an option to enable/disable this, so it is easier to assess impact, and also it might be relevant for proof logging.

[ImkoMarijnissen]

I think the problem with treating atomic constraints as literals is that we need to support notify_backtrack.

From what I remember, this is somewhat difficult since the notification engine uses stateful integers, meaning that upon backtracking, there is no information about what atomic constraints are undone. Perhaps we could add a special kind of stateful integers, which informs the notification system that the index has been moved from $a$ to $b$ upon backtracking.

Another option is to use the PredicateIdAssignments, which contains a trail of predicates. The problem is that we would need to be able to differentiate between the two predicate types when untracking (i.e., atomic constraints which are tracked by the engine and those which are not but for which the status was requested at some point) and ensure that the decision level is correct when notifying (this decision level can be incorrect since predicates can be tracked at any point, even if it is already true/false).

Either way, it would be interesting to look into!