Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
10works
0followers
12topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

10 published item(s)

preprint2022arXiv

Physarum Inspired Dynamics to Solve Semi-Definite Programs

Physarum Polycephalum is a slime mold that can solve shortest path problems. A mathematical model based on Physarum's behavior, known as the Physarum Directed Dynamics, can solve positive linear programs. In this paper, we present a family of Physarum-based dynamics extending the previous work and introduce a new algorithm to solve positive Semi-Definite Programs (SDP). The Physarum dynamics are governed by orthogonal projections (w.r.t. time-dependent scalar products) on the affine subspace defined by the linear constraints. We present a natural generalization of the scalar products used in the LP case to the matrix space for SDPs, which boils down to the linear case when all matrices in the SDP are diagonal, thus, representing an LP. We investigate the behavior of the induced dynamics theoretically and experimentally, highlight challenges arising from the non-commutative nature of matrix products, and prove soundness and convergence under mild conditions. Moreover, we consider a more abstract view on the dynamics that suggests a slight variation to guarantee unconditional soundness and convergence-to-optimality. By simulating these dynamics using suitable discretizations, one obtains numerical algorithms for solving positive SDPs, which have applications in discrete optimization, e.g., for computing the Goemans-Williamson approximation for MaxCut or the Lovasz theta number for determining the clique/chromatic number in perfect graphs.

preprint2022arXiv

Physarum-Inspired Multi-Commodity Flow Dynamics

In wet-lab experiments, the slime mold Physarum polycephalum has demonstrated its ability to solve shortest path problems and to design efficient networks. For the shortest path problem, a mathematical model for the evolution of the slime is available and it has been shown in computer experiments and through mathematical analysis that the dynamics solves the shortest path problem. In this paper, we introduce a dynamics for the network design problem. We formulate network design as the problem of constructing a network that efficiently supports a multi-commodity flow problem. We investigate the dynamics in computer simulations and analytically. The simulations show that the dynamics is able to construct efficient and elegant networks. In the theoretical part we show that the dynamics minimizes an objective combining the cost of the network and the cost of routing the demands through the network. We also give alternative characterization of the optimum solution.

preprint2021arXiv

Improving EFX Guarantees through Rainbow Cycle Number

We study the problem of fairly allocating a set of indivisible goods among $n$ agents with additive valuations. Envy-freeness up to any good (EFX) is arguably the most compelling fairness notion in this context. However, the existence of EFX allocations has not been settled and is one of the most important problems in fair division. Towards resolving this problem, many impressive results show the existence of its relaxations, e.g., the existence of $0.618$-EFX allocations, and the existence of EFX at most $n-1$ unallocated goods. The latter result was recently improved for three agents, in which the two unallocated goods are allocated through an involved procedure. Reducing the number of unallocated goods for arbitrary number of agents is a systematic way to settle the big question. In this paper, we develop a new approach, and show that for every $\varepsilon \in (0,1/2]$, there always exists a $(1-\varepsilon)$-EFX allocation with sublinear number of unallocated goods and high Nash welfare. For this, we reduce the EFX problem to a novel problem in extremal graph theory. We introduce the notion of rainbow cycle number $R(\cdot)$. For all $d \in \mathbb{N}$, $R(d)$ is the largest $k$ such that there exists a $k$-partite digraph $G =(\cup_{i \in [k]} V_i, E)$, in which 1) each part has at most $d$ vertices, i.e., $\lvert V_i \rvert \leq d$ for all $i \in [k]$, 2) for any two parts $V_i$ and $V_j$, each vertex in $V_i$ has an incoming edge from some vertex in $V_j$ and vice-versa, and 3) there exists no cycle in $G$ that contains at most one vertex from each part. We show that any upper bound on $R(d)$ directly translates to a sublinear bound on the number of unallocated goods. We establish a polynomial upper bound on $R(d)$, yielding our main result. Furthermore, our approach is constructive, which also gives a polynomial-time algorithm for finding such an allocation.

preprint2020arXiv

A Little Charity Guarantees Almost Envy-Freeness

Fair division of indivisible goods is a very well-studied problem. The goal of this problem is to distribute $m$ goods to $n$ agents in a &#34;fair&#34; manner, where every agent has a valuation for each subset of goods. We assume general valuations. Envy-freeness is the most extensively studied notion of fairness. However, envy-free allocations do not always exist when goods are indivisible. The notion of fairness we consider here is &#34;envy-freeness up to any good&#34; (EFX) where no agent envies another agent after the removal of any single good from the other agent&#39;s bundle. It is not known if such an allocation always exists even when $n=3$. We show there is always a partition of the set of goods into $n+1$ subsets $(X_1,\ldots,X_n,P)$ where for $i \in [n]$, $X_i$ is the bundle allocated to agent $i$ and the set $P$ is unallocated (or donated to charity) such that we have$\colon$ 1) envy-freeness up to any good, 2) no agent values $P$ higher than her own bundle, and 3) fewer than $n$ goods go to charity, i.e., $|P| < n$ (typically $m \gg n$). Our proof is constructive. When agents have additive valuations and $\lvert P \rvert$ is large (i.e., when $|P|$ is close to $n$), our allocation also has a good maximin share (MMS) guarantee. Moreover, a minor variant of our algorithm also shows the existence of an allocation which is $4/7$ groupwise maximin share (GMMS): this is a notion of fairness stronger than MMS. This improves upon the current best bound of $1/2$ known for an approximate GMMS allocation.

preprint2020arXiv

Convergence of the Non-Uniform Directed Physarum Model

The directed Physarum dynamics is known to solve positive linear programs: minimize $c^T x$ subject to $Ax = b$ and $x \ge 0$ for a positive cost vector $c$. The directed Physarum dynamics evolves a positive vector $x$ according to the dynamics $\dot{x} = q(x) - x$. Here $q(x)$ is the solution to $Af = b$ that minimizes the &#34;energy&#34; $\sum_i c_i f_i^2/x_i$. In this paper, we study the non-uniform directed dynamics $\dot{x} = D(q(x) - x)$, where $D$ is a positive diagonal matrix. The non-uniform dynamics is more complex than the uniform dynamics (with $D$ being the identity matrix), as it allows each component of $x$ to react with different speed to the differences between $q(x)$ and $x$. Our contribution is to show that the non-uniform directed dynamics solves positive linear programs.

preprint2020arXiv

Convergence of the Non-Uniform Physarum Dynamics

Let $c \in \mathbb{Z}^m_{> 0}$, $A \in \mathbb{Z}^{n\times m}$, and $b \in \mathbb{Z}^n$. We show under fairly general conditions that the non-uniform Physarum dynamics \[ \dot{x}_e = a_e(x,t) \left(|q_e| - x_e\right) \] converges to the optimum solution $x^*$ of the weighted basis pursuit problem minimize $c^T x$ subject to $A f = b$ and $|f| \le x$. Here, $f$ and $x$ are $m$-vectors of real variables, $q$ minimizes the energy $\sum_e (c_e/x_e) q_e^2$ subject to the constraints $A q = b$ and $\mathrm{supp}(q) \subseteq \mathrm{supp}(x)$, and $a_e(x,t) > 0$ is the reactivity of edge $e$ to the difference $|q_e| - x_e$ at time $t$ and in state $x$. Previously convergence was only shown for the uniform case $a_e(x,t) = 1$ for all $e$, $x$, and $t$. We also show convergence for the dynamics \[ \dot{x}_e = x_e \cdot \left( g_e \left(\frac{|q_e|}{x_e}\right) - 1\right),\] where $g_e$ is an increasing differentiable function with $g_e(1) = 1$. Previously convergence was only shown for the special case of the shortest path problem on a graph consisting of two nodes connected by parallel edges.

preprint2020arXiv

EFX Exists for Three Agents

We study the problem of distributing a set of indivisible items among agents with additive valuations in a $\mathit{fair}$ manner. The fairness notion under consideration is Envy-freeness up to any item (EFX). Despite significant efforts by many researchers for several years, the existence of EFX allocations has not been settled beyond the simple case of two agents. In this paper, we show constructively that an EFX allocation always exists for three agents. Furthermore, we falsify the conjecture by Caragiannis et al. by showing an instance with three agents for which there is a partial EFX allocation (some items are not allocated) with higher Nash welfare than that of any complete EFX allocation.

preprint2020arXiv

The Maximum-Level Vertex in an Arrangement of Lines

Let $L$ be a set of $n$ lines in the plane, not necessarily in general position. We present an efficient algorithm for finding all the vertices of the arrangement $A(L)$ of maximum level, where the level of a vertex $v$ is the number of lines of $L$ that pass strictly below $v$. The problem, posed in Exercise~8.13 in de Berg etal [BCKO08], appears to be much harder than it seems, as this vertex might not be on the upper envelope of the lines. We first assume that all the lines of $L$ are distinct, and distinguish between two cases, depending on whether or not the upper envelope of $L$ contains a bounded edge. In the former case, we show that the number of lines of $L$ that pass above any maximum level vertex $v_0$ is only $O(\log n)$. In the latter case, we establish a similar property that holds after we remove some of the lines that are incident to the single vertex of the upper envelope. We present algorithms that run, in both cases, in optimal $O(n\log n)$ time. We then consider the case where the lines of $L$ are not necessarily distinct. This setup is more challenging, and the best we have is an algorithm that computes all the maximum-level vertices in time $O(n^{4/3}\log^{3}n)$. Finally, we consider a related combinatorial question for degenerate arrangements, where many lines may intersect in a single point, but all the lines are distinct: We bound the complexity of the weighted $k$-level in such an arrangement, where the weight of a vertex is the number of lines that pass through the vertex. We show that the bound in this case is $O(n^{4/3})$, which matches the corresponding bound for non-degenerate arrangements, and we use this bound in the analysis of one of our algorithms.

preprint2013arXiv

A Framework for the Verification of Certifying Computations

Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually involves intricate mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm - yet it is all the user has to trust. The verification of checkers is feasible with current tools and leads to computations that can be completely trusted. We describe a framework to seamlessly verify certifying computations. We use the automatic verifier VCC for establishing the correctness of the checker and the interactive theorem prover Isabelle/HOL for high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of typical examples of the industrial-level and widespread algorithmic library LEDA.

preprint2012arXiv

Remarks on Category-Based Routing in Social Networks

It is well known that individuals can route messages on short paths through social networks, given only simple information about the target and using only local knowledge about the topology. Sociologists conjecture that people find routes greedily by passing the message to an acquaintance that has more in common with the target than themselves, e.g. if a dentist in Saarbrücken wants to send a message to a specific lawyer in Munich, he may forward it to someone who is a lawyer and/or lives in Munich. Modelling this setting, Eppstein et al. introduced the notion of category-based routing. The goal is to assign a set of categories to each node of a graph such that greedy routing is possible. By proving bounds on the number of categories a node has to be in we can argue about the plausibility of the underlying sociological model. In this paper we substantially improve the upper bounds introduced by Eppstein et al. and prove new lower bounds.