-
Proven Runtime Guarantees for How the MOEA/D Computes the Pareto Front From the Subproblem Solutions
Authors:
Benjamin Doerr,
Martin S. Krejca,
Noé Weeks
Abstract:
The decomposition-based multi-objective evolutionary algorithm (MOEA/D) does not directly optimize a given multi-objective function $f$, but instead optimizes $N + 1$ single-objective subproblems of $f$ in a co-evolutionary manner. It maintains an archive of all non-dominated solutions found and outputs it as approximation to the Pareto front. Once the MOEA/D found all optima of the subproblems (t…
▽ More
The decomposition-based multi-objective evolutionary algorithm (MOEA/D) does not directly optimize a given multi-objective function $f$, but instead optimizes $N + 1$ single-objective subproblems of $f$ in a co-evolutionary manner. It maintains an archive of all non-dominated solutions found and outputs it as approximation to the Pareto front. Once the MOEA/D found all optima of the subproblems (the $g$-optima), it may still miss Pareto optima of $f$. The algorithm is then tasked to find the remaining Pareto optima directly by mutating the $g$-optima.
In this work, we analyze for the first time how the MOEA/D with only standard mutation operators computes the whole Pareto front of the OneMinMax benchmark when the $g$-optima are a strict subset of the Pareto front. For standard bit mutation, we prove an expected runtime of $O(n N \log n + n^{n/(2N)} N \log n)$ function evaluations. Especially for the second, more interesting phase when the algorithm start with all $g$-optima, we prove an $Ω(n^{(1/2)(n/N + 1)} \sqrt{N} 2^{-n/N})$ expected runtime. This runtime is super-polynomial if $N = o(n)$, since this leaves large gaps between the $g$-optima, which require costly mutations to cover.
For power-law mutation with exponent $β\in (1, 2)$, we prove an expected runtime of $O\left(n N \log n + n^β \log n\right)$ function evaluations. The $O\left(n^β \log n\right)$ term stems from the second phase of starting with all $g$-optima, and it is independent of the number of subproblems $N$. This leads to a huge speedup compared to the lower bound for standard bit mutation. In general, our overall bound for power-law suggests that the MOEA/D performs best for $N = O(n^{β- 1})$, resulting in an $O(n^β\log n)$ bound. In contrast to standard bit mutation, smaller values of $N$ are better for power-law mutation, as it is capable of easily creating missing solutions.
△ Less
Submitted 3 May, 2024; v1 submitted 2 May, 2024;
originally announced May 2024.
-
Sound Automation of Magic Wands (extended version)
Authors:
Thibault Dardinier,
Gaurav Parthasarathy,
Noé Weeks,
Alexanders J. Summers,
Peter Müller
Abstract:
The magic wand $\mathbin{-\!\!*}$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula $A \mathbin{-\!\!*} B$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magi…
▽ More
The magic wand $\mathbin{-\!\!*}$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula $A \mathbin{-\!\!*} B$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magic wand (also called packaging a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or, as we show in this paper, are unsound. We present a formal framework that precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics. We prove in Isabelle/HOL that our formal framework is sound and complete, and use it to develop a novel package algorithm that offers competitive automation and is sound. Moreover, we present a novel, restricted definition of wands and prove in Isabelle/HOL that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands. We have implemented our techniques for the Viper language, and demonstrate that they are effective in practice.
△ Less
Submitted 2 August, 2022; v1 submitted 23 May, 2022;
originally announced May 2022.
-
Visual Companion for Booklovers
Authors:
Zona Kostic,
Jared Jessup,
Jeffrey Baglioni,
Nathan Weeks,
Johann Philipp Dreessen,
Ning Chen,
Tianyu Liu
Abstract:
An innumerable number of individual choices go into discovering a new book. There are unmistakably two groups of booklovers: those who like to search online, follow other people's latest readings, or simply react to a system's recommendations; and those who love to wander between library stacks, lose themselves behind bookstore shelves, or simply hide behind piles of (un)organized books. Depending…
▽ More
An innumerable number of individual choices go into discovering a new book. There are unmistakably two groups of booklovers: those who like to search online, follow other people's latest readings, or simply react to a system's recommendations; and those who love to wander between library stacks, lose themselves behind bookstore shelves, or simply hide behind piles of (un)organized books. Depending on which group a person may fall into, there are two distinct and corresponding mediums that inform his or her choices: digital, that provides efficient retrieval of information online, and physical, a more tactile pursuit that leads to unexpected discoveries and promotes serendipity. How could we possibly bridge the gap between these seemingly disparate mediums into an integrated system that can amplify the benefits they both offer? In this paper, we present the BookVIS application, which uses book-related data and generates personalized visualizations to follow users in their quest for a new book. In this new redesigned version, the app brings associative visual connections to support intuitive exploration of easily retrieved digital information and its relationship with the physical book in hand. BookVIS keeps track of the user's reading preferences and generates a dataSelfie as an individual snapshot of a personal taste that grows over time. Usability testing has also been conducted and has demonstrated the app's ability to identify distinguishable patterns in readers' tastes that could be further used to communicate personal preferences in new "shelf-browsing" iterations. By efficiently supplementing the user's cognitive information needs while still supporting the spontaneity and enjoyment of the book browsing experience, BookVIS bridges the gap between real and online realms, and maximizes the engagement of personalized mobile visual clues.
△ Less
Submitted 31 October, 2020;
originally announced November 2020.
