Support unused variables in the objective function when the optimization problem is trivial
During the PB15, an issue was discovered when variables not used in the CNF appear in the objective function and that the optimal solution is found directly.
Here is a simple test case:
[code]
- #variable= 3 #constraint= 1 min: +1 x1 +1 x2 +1 x3 ; +1 x3 +1 x2 = 1; [/code]
The solver will find a first model x2 -x3 for instance which satisfes the constraint.
The solver adds a constraint x1 + x2 +x3 < 1 which makes the formula UNSAT.
As such, the previous model, without mention of x1 is returned.
We need to detect that case, and to complete the model by falsifying the literals found in the objective function.
Detecting that situation is easy. Fixing properly the model requires a bit of work.