fix(opt): Only perform optimization when building a model

[bclement-ocp]

The optimization module is supposed to help us build an optimized model, so it doesn't make much sense to start optimizing before we start actually looking for a model.

Previously, we were kind of forced into it because it would be incorrect to perform case splits before optimizing. Now that optimization is integrated directly into the SAT solver, it is fully independent from case splits, and this restriction does not apply any longer.

This fixes issues where we would try to optimize eagerly in a small solution space and would end up enumerating the solution space before performing examining some decisions that would prune it for us, which is exactly what happened in #1222.

Separate optimization (do_optimize) from case splitting (do_case_split) at the Theory level, and perform optimization in compute_concrete_model, i.e. at the time we switch to model generation (note: this limits the impact of optimization on unsat problems).

Also change the order of decisions to consider optimized splits last for consistency, although that should not have much impact in practice.

[bclement-ocp]

Updated quickly after marking as ready for review because I realized that do_optimize only performs side effects and does not need to return a new theory environment, sorry!

[Halbaroth]

Previously, we were kind of forced into it because it would be incorrect to perform case splits before optimizing. Now that optimization is integrated directly into the SAT solver, it is fully independent from case splits, and this restriction does not apply any longer.

Can you explain in more details please? I am not sure to understand what you mean by incorrect? I thought it was for performance issue. If your problem is SAT and you perform split before optimizing, you will produce a suboptimal model and then you will optimize it, which is slower than optimizing first and splitting to complete the model.

[bclement-ocp]

Can you explain in more details please? I am not sure to understand what you mean by incorrect?

Consider the following problem:

(set-logic ALL)
(declare-const x Int)
(declare-const y Int)
(assert (<= y x))
(assert (<= 0 x 10))
(maximize y)
(check-sat)

We would send the assertions y <= x, 0 <= x and x <= 10 to the theory. In the original case split version for optimization, from the point of view of the theory, if we first select x = 0 as a case split we will find the model where x = 0 and y = 0, which is not optimal for the constraints we have given the theory.

We would fix it later by looking for a model with y > 0 in satml_frontend, but again, from the point of view of the theory, we find a model that is not optimal given the constraints we were provided.

Currently we perform optimization based on the regular environment (not the case split environment), so we are always optimizing independently of case splits.

If your problem is SAT and you perform split before optimizing, you will produce a suboptimal model and then you will optimize it, which is slower than optimizing first and splitting to complete the model.

I don't think this assertion is correct in general, because it is might be easier to optimize an existing model than to find an optimized model directly (see e.g. the two-steps process of a simplex algorithm). This is exactly what happens with #1222 : we try to optimize first, but each time we try to select an optimized value, it turns out there is no model with that value.

(In the case that the problem is UNSAT in which case optimizing first is likely to take longer to prove unsatisfiability).

What made this kind of work in the original implementation is that if we optimize to a value but then the SAT solver makes a decision that is in contradiction with this optimized value, we would silently cancel the optimization and re-optimize (as part of the infamous try_it).

Optimization and splitting are now independent (because we optimize in the main environment but split in the case split environment), so we are both splitting first (we make splitting decisions earlier during the program execution) and optimizing first (because once we optimize we will cancel any split that were incompatible with the optimized value, without backtracking the SAT).

The interaction between --enable-sat-cs and optimization is less clear, and I think both schemes are somewhat broken currently anyways, so i have reverted that part of the change. It is still probably better to split first and optimize after, so that we at least have a model to optimize (but mostly we should stop splitting on values and partition the space instead).