Comments (2)
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:
-
check that a provided solution x* is satisfies the formula F
-
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:
-
check that the provided solution x* is satisfiable for the formula F
-
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.
Related Issues (20)
- Improve Documentation
- Internal error when using wrong formula file
- Degree becomes negative after multiplication and addition. HOT 2
- Feature request: progress measure HOT 1
- Feature request: preprocessing
- Bug: variables with coefficient 0 after saturation not ignored
- Printing sorted constraints HOT 1
- Improve / Fix Hints
- __int128 support HOT 3
- Allow negative IDs for relative reference. HOT 1
- Add include statement.
- Performance improvements for occurrence list. HOT 1
- Return code 127 when running low or out of memory. HOT 1
- Partial formula loading and solution logging. HOT 1
- Non standard code.
- Color code rules in trace.
- Inconsistent behaviour of deletion HOT 1
- Add examples for different rules in documentation.
- Test fuzzing via parser generator.
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from veripb.