Multiple objectives about veripb HOT 2 OPEN

Hi,

this is a very interesting question, so far we did not consider multi
objective optimization (except if the objectives have a strict
priority in which case they can be combined into a single objective by
scaling coefficients appropriately). I would be interested in
supporting multi objective optimization but this is a bit outside of
my current expertise and I am not entirely sure if it would fit the
current framework.

Essentially, we only support proofs of unsatisfiability (for all x the
formula F is not satisfied). The reason why we can do optimization is
that it can be split into two steps:

1. check that a provided solution x* is satisfies the formula F

2. check that there is no solution with a better objective value,
   i.e., f(x) < f(x*) and F is unsatisfiable.

So we can potentially verify statements of the form

exists y for all x ...

and hence the same approach should work for verifying a single pareto
optimal solution:

1. check that the provided solution x* is satisfiable for the formula F

2. check that there is no pareto better solution, i.e., the formula

    F and (
        (f_1(y) < f_1(x*) and  f_2(y) = f_2(x*) and ... ) 
        or (f_1(y) = f_1(x*) and  f_2(y) < f_2(x*) and ... ) 
        or ...
    ) 
   
    is unsatisfiable.
   

and it might be nice to add some syntactic sugar to the current proof
format to have this in one proof file.

Checking that we found the entire pareto front seems more difficult
and I do not see on top of my head how / if this can be expressed as a
single unsatisfiable problem. The difficulty is that the quantifiers
for this task are swapped and we would need to verify something of the
form

for all x exists y s.t. x is in the found pareto front or y is
pareto better than x

Maybe something could be done here by splitting it into two separate
problems as you might be suggesting: one for the variable space to
show pareto optimal solutions and one for the objective space that
would require rules specific to this problem and ensuring that all
possible pareto fronts are discovered / ruled out. Regarding sharing
constraints between different sub-proofs to avoid re-deriving
information one would need to be careful to not break anything.

Checking that we have the full pre image for a given part of the
pareto front should be possible already with the current set of rules
as this can be done by verifying unsatiability of the problem

exists x s.t. x is not in the set of found solutions and x is in
one of the given pareto fronts and x satisfies the formula F

(or enumerating solutions of the problem x is in one of the pareto
fronts and x satisfies the formula F)

I hope this gives you some idea of what type of statements we can
potentially verify.

I am not aware of any proof logging for multi objective optimization
or general quantified boolean formulas, which would also be relevant
for this application. There are theoretic proof systems for quantified
boolean formulas in CNF, such as Q-Resolution.

Best Regards,
Stephan

from veripb.

I feel this formula is wrong:

F and (
     (f_1(y) < f_1(x*) and  f_2(y) = f_2(x*) and ... ) 
     or (f_1(y) = f_1(x*) and  f_2(y) < f_2(x*) and ... ) 
     or ...
 ) 

And it should look like:

F and (
     (f_1(y) < f_1(x*) and  f_2(y) =< f_2(x*) and ... ) 
     or (f_1(y) =< f_1(x*) and  f_2(y) < f_2(x*) and ... ) 
     or ...
 ) 

As i don't see if there is a Pareto optimal solution why is must be only dominant in one component.

F and (
     (f_1(y) <= f_1(x*) and  f_2(y) <= f_2(x*) and ... 
     and (f_1(y) + f_2(y) + ... < f_1(x*) +f_2(x*)  ... ) 
   
 ) 

which doesn't seem that horrible in a pseudo boolean framework. The < can be easily replaced by an =< if the gap to next biggest/smallest possible sum of all objectives is know. In case of Integer weights ... +1 =< would work but with some thought a stronger bound could be formulated. (Example if all all objectives can only assume even values, +2 would work)

Do you think it would be possible to express that?

As for verifying properties about the entire pareto front, reasoning in the objective space is unavoidable in the absence of quantors and would also likely lead to better performance.

from veripb.