Multiple objectives

[freemin7]

I would like to start a discussion around multi-objective pseudo boolean optimization. The result of a pseudo boolean optimization is (a subset of) a pareto front. Due to the nature of PBO this pareto front will contain finitely many points. I envision three modes of verification.

• check that all solutions given are a subset of the pareto front
• check that the image of the solutions under the objectives is the entire pareto front
• check that the solutions given are the entire preimage of the pareto front under the objectives

A subset of the pareto front might be generated by a positive linear combination of objectives, repeated optimization of one free objective or by a solver interacting with the user to explore the pareto front under his guidance or by trying to find the closest point to a given infeasible one. Even if the pareto front is not fully explored it can be useful to still be able to verify that those guided solves are on the pareto front.

A complete pareto front might be generated by a core driven search, a multi objective linear/binary search or a local exploration along the pareto front by relaxing one objective to increase others. The difference between point 2 and 3 is that multiple assignments might have the same objective values and the 2nd doesn't care that is got all assignments that that map to certain point on the pareto front.

This would require changes in format as objectives would need to be able to identified and preferably named. In addition it would require additional reasoning about the completeness of the pareto front, such as:

• that certain parts of the objective space are dominated by an existing solution,
• that nothing can dominate a solution optimizing only objective A in objective A
• maybe also something like "there are no intermediate solution" between pareto front members due to the discreteness of the search space.

Let me give an example that demonstrates this reasoning:

o1 -2 x1 -2 x2 -1 x3
o2 -3 x1 -2 ~x2

Lets find upper bound for o2
min -3 x1 -2 ~x2
We find assignment x1 ~x2 ~x3
This mean for all points of the pareto front: o2 <= -5, however this assignment (giving o1=-2) is not necessarily on the pareto front, so we need to check:
min -2 x2 -1 x3, -3 x1 -2 ~x2 = -5
We find assignment x1 ~x2 x3 with (-3,-5)
(-3,-5) can't be dominated since -5 is the minimum for o2 and o1 can't be any better subject to o2 = -5
Lets find upper bound for o1
min o1 -2 x1 -2 x2 -1 x3
we find assignment x1 x2 x3 
This mean for all points of the pareto front: o1 <= -5, however this assignment (giving o1=-3) is not necessarily on the pareto front, so we need to check:
min -3 x1 -2 ~x2, -2 x2 -1 x3  = -5
We find assignment x1 x2 x3 with (-5,-3)
(-5,-3) can't be dominated since -5 is the minimum for o1 and o2 can't be any better subject to o1 = -5
Since (-5,-3) is pareto optimal there can't be any (x,y) with x<-5 or (-5=x and y<=-3) or (x>=-5 and y>-3) or (x>-5 and y>=-3) that's also part of the pareto set and differs in objective
Since (-3,-5) is pareto optimal there can't be any (x,y) with y<-5 or (-5=y and x<=-3) or (y>=-5 and x>-3) or (y>-5 and x>=-3) that's also part of the pareto set and differs in objective
This only leaves a solution with (-4,-4) as possible candidate for the pareto set.
sat -2 x2 -1 x3 = -4, -3 x1 -2 ~x2 = 4
Such a solution however does not exist.
(-3,-5) with assignment x1 ~x2 x3
(-5,-3) with assignment  x1 x2 x3 
cover the entire pareto-set however we didn't check that they are all the assignments that could result in those objective values

I think this reasoning can be expressed entirely with the help of PB problems which can also be elaborated in the same proof format however the proof checker would need to be aware that sometimes we are not making statements about the variable space of a particular instance but reasoning about solution space in which the pareto front lies instead. Are limited form of this reasoning already exist to justify the search in PBO.

I am aware that one could use the existing format and just make a folder of named proofs about particular PBO/PB problems that occurred during solving and refer those in a proof at objective space level. However it might be bothersome to re-derive information or always check that all depended proofs were included.

I didn't find any reference to multi-objective optimization in that repository, so i started an issue. Would you be open to consider proof logging for multi-objective pseudo boolean optimization?

[StephanGocht]

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

[freemin7]

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.