-
Distributed Agreement in the Arrovian Framework
Authors:
Kenan Wood,
Hammurabi Mendes,
Jonad Pulaj
Abstract:
Preference aggregation is a fundamental problem in voting theory, in which public input rankings of a set of alternatives (called preferences) must be aggregated into a single preference that satisfies certain soundness properties. The celebrated Arrow Impossibility Theorem is equivalent to a distributed task in a synchronous fault-free system that satisfies properties such as respecting unanimous…
▽ More
Preference aggregation is a fundamental problem in voting theory, in which public input rankings of a set of alternatives (called preferences) must be aggregated into a single preference that satisfies certain soundness properties. The celebrated Arrow Impossibility Theorem is equivalent to a distributed task in a synchronous fault-free system that satisfies properties such as respecting unanimous preferences, maintaining independence of irrelevant alternatives (IIA), and non-dictatorship, along with consensus since only one preference can be decided.
In this work, we study a weaker distributed task in which crash faults are introduced, IIA is not required, and the consensus property is relaxed to either $k$-set agreement or $ε$-approximate agreement using any metric on the set of preferences. In particular, we prove several novel impossibility results for both of these tasks in both synchronous and asynchronous distributed systems. We additionally show that the impossibility for our $ε$-approximate agreement task using the Kendall tau or Spearman footrule metrics holds under extremely weak assumptions.
△ Less
Submitted 29 October, 2024; v1 submitted 6 September, 2024;
originally announced September 2024.
-
Optimal Multilevel Slashing for Blockchains
Authors:
Kenan Wood,
Hammurabi Mendes,
Jonad Pulaj
Abstract:
We present the notion of multilevel slashing, where proof-of-stake blockchain validators can obtain gradual levels of assurance that a certain block is bound to be finalized in a global consensus procedure, unless an increasing and optimally large number of Byzantine processes have their staked assets slashed -- that is, deducted -- due to provably incorrect behavior. Our construction is a highly…
▽ More
We present the notion of multilevel slashing, where proof-of-stake blockchain validators can obtain gradual levels of assurance that a certain block is bound to be finalized in a global consensus procedure, unless an increasing and optimally large number of Byzantine processes have their staked assets slashed -- that is, deducted -- due to provably incorrect behavior. Our construction is a highly parameterized generalization of combinatorial intersection systems based on finite projective spaces, with asymptotic high availability and optimal slashing properties. Even under weak conditions, we show that our construction has asymptotically optimal slashing properties with respect to message complexity and validator load; this result also illustrates a fundamental trade off between message complexity, load, and slashing. In addition, we show that any intersection system whose ground elements are disjoint subsets of nodes (e.g. "committees" in committee-based consensus protocols) has asymptotic high availability under similarly weak conditions. Finally, our multilevel construction gives the flexibility to blockchain validators to decide how many "levels" of finalization assurance they wish to obtain. This functionality can be seen either as (i) a form of an early, slashing-based block finalization; or (ii) a service to support reorg tolerance.
△ Less
Submitted 29 October, 2024; v1 submitted 13 May, 2024;
originally announced May 2024.
-
Expiring Assets in Automated Market Makers
Authors:
Kenan Wood,
Maurice Herlihy,
Hammurabi Mendes,
Jonad Pulaj
Abstract:
An automated market maker (AMM) is a state machine that manages pools of assets, allowing parties to buy and sell those assets according to a fixed mathematical formula. AMMs are typically implemented as smart contracts on blockchains, and its prices are kept in line with the overall market price by arbitrage: if the AMM undervalues an asset with respect to the market, an "arbitrageur" can make a…
▽ More
An automated market maker (AMM) is a state machine that manages pools of assets, allowing parties to buy and sell those assets according to a fixed mathematical formula. AMMs are typically implemented as smart contracts on blockchains, and its prices are kept in line with the overall market price by arbitrage: if the AMM undervalues an asset with respect to the market, an "arbitrageur" can make a risk-free profit by buying just enough of that asset to bring the AMM's price back in line with the market.
AMMs, however, are not designed for assets that expire: that is, assets that cannot be produced or resold after a specified date. As assets approach expiration, arbitrage may not be able to reconcile supply and demand, and the liquidity providers that funded the AMM may have excessive exposure to risk due to rapid price variations.
This paper formally describes the design of a decentralized exchange (DEX) for assets that expire, combining aspects of AMMs and limit-order books. We ensure liveness and market clearance, providing mechanisms for liquidity providers to control their exposure to risk and adjust prices dynamically in response to situations where arbitrage may fail.
△ Less
Submitted 8 January, 2024;
originally announced January 2024.
-
Automating Weight Function Generation in Graph Pebbling
Authors:
Dominic Flocco,
Jonad Pulaj,
Carl Yerger
Abstract:
Graph pebbling is a combinatorial game played on an undirected graph with an initial configuration of pebbles. A pebbling move consists of removing two pebbles from one vertex and placing one pebble on an adjacent vertex. The pebbling number of a graph is the smallest number of pebbles necessary such that, given any initial configuration of pebbles, at least one pebble can be moved to a specified…
▽ More
Graph pebbling is a combinatorial game played on an undirected graph with an initial configuration of pebbles. A pebbling move consists of removing two pebbles from one vertex and placing one pebble on an adjacent vertex. The pebbling number of a graph is the smallest number of pebbles necessary such that, given any initial configuration of pebbles, at least one pebble can be moved to a specified root vertex. Recent lines of inquiry apply computational techniques to pebbling bound generation and improvement.
Along these lines, we present a computational framework that produces a set of tree strategy weight functions that are capable of proving pebbling number upper bounds on a connected graph. Our mixed-integer linear programming approach automates the generation of large sets of such functions and provides verifiable certificates of pebbling number upper bounds. The framework is capable of producing verifiable pebbling bounds on any connected graph, regardless of its structure or pebbling properties. We apply the model to the 4th weak Bruhat to prove $π(B_4) \leq 66$ and to the Lemke square graph to produce a set of certificates that verify $π(L x L) \leq 96$.
△ Less
Submitted 19 December, 2023;
originally announced December 2023.
-
Satisfiability Modulo Theories for Verifying MILP Certificates
Authors:
Kenan Wood,
Runtian Zhou,
Haoze Wu,
Hammurabi Mendes,
Jonad Pulaj
Abstract:
Correctness of results from mixed-integer linear programming (MILP) solvers is critical, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR 1.0 is the first recently proposed general certificate format for answers produced by MILP solvers. We design a schema to encode VIPR's inference rules as a g…
▽ More
Correctness of results from mixed-integer linear programming (MILP) solvers is critical, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR 1.0 is the first recently proposed general certificate format for answers produced by MILP solvers. We design a schema to encode VIPR's inference rules as a ground formula that completely characterizes the validity of the algorithmic check, removing any ambiguities and imprecisions present in the specification. We implement a checker for VIPR certificates by expressing our ground formula with the Satisfiability Modulo Theory Library (SMT-LIB) and check its validity. Our approach is solver-agnostic, and we test its viability using benchmark instances found in the literature.
△ Less
Submitted 26 September, 2024; v1 submitted 16 December, 2023;
originally announced December 2023.
-
On the Linear Ordering Problem and the Rankability of Data
Authors:
Thomas R. Cameron,
Sebastian Charmot,
Jonad Pulaj
Abstract:
In 2019, Anderson et al. proposed the concept of rankability, which refers to a dataset's inherent ability to be meaningfully ranked. In this article, we give an expository review of the linear ordering problem (LOP) and then use it to analyze the rankability of data. Specifically, the degree of linearity is used to quantify what percentage of the data aligns with an optimal ranking. In a sports c…
▽ More
In 2019, Anderson et al. proposed the concept of rankability, which refers to a dataset's inherent ability to be meaningfully ranked. In this article, we give an expository review of the linear ordering problem (LOP) and then use it to analyze the rankability of data. Specifically, the degree of linearity is used to quantify what percentage of the data aligns with an optimal ranking. In a sports context, this is analogous to the number of games that a ranking can correctly predict in hindsight. In fact, under the appropriate objective function, we show that the optimal rankings computed via the LOP maximize the hindsight accuracy of a ranking. Moreover, we develop a binary program to compute the maximal Kendall tau ranking distance between two optimal rankings, which can be used to measure the diversity among optimal rankings without having to enumerate all optima. Finally, we provide several examples from the world of sports and college rankings to illustrate these concepts and demonstrate our results.
△ Less
Submitted 12 April, 2021;
originally announced April 2021.
-
Diameter Polytopes of Feasible Binary Programs
Authors:
Thomas R. Cameron,
Sebastian Charmot,
Jonad Pulaj
Abstract:
Feasible binary programs often have multiple optimal solutions, which is of interest in applications as they allow the user to choose between alternative optima without deteriorating the objective function. In this article, we present the optimal diameter of a feasible binary program as a metric for measuring the diversity among all optimal solutions. In addition, we present the diameter binary pr…
▽ More
Feasible binary programs often have multiple optimal solutions, which is of interest in applications as they allow the user to choose between alternative optima without deteriorating the objective function. In this article, we present the optimal diameter of a feasible binary program as a metric for measuring the diversity among all optimal solutions. In addition, we present the diameter binary program whose optima contains two optimal solutions of the given feasible binary program that are as diverse as possible with respect to the optimal diameter. Our primary interest is in the study of the diameter polytope, i.e., the polytope underlying the diameter binary program. Under suitable conditions, we show that much of the structure of the diameter polytope is inherited from the polytope underlying the given binary program. Finally, we apply our results on the diameter binary program and diameter polytope to cases where the given binary program corresponds to the linear ordering problem and the symmetric traveling salesman problem.
△ Less
Submitted 16 August, 2020;
originally announced August 2020.
-
Characterizing 3-sets in Union-Closed Families
Authors:
Jonad Pulaj
Abstract:
A family of sets is union-closed (UC) if the union of any two sets in the family is also in the family. Frankl's UC sets conjecture states that for any nonempty UC family $\mathcal{F} \subseteq 2^{[n]}$ such that $\mathcal{F} \neq \left\{\emptyset\right\}$, there exists an element $i \in [n]$ that is contained in at least half the sets of $\mathcal{F}$. The 3-sets conjecture of Morris states that…
▽ More
A family of sets is union-closed (UC) if the union of any two sets in the family is also in the family. Frankl's UC sets conjecture states that for any nonempty UC family $\mathcal{F} \subseteq 2^{[n]}$ such that $\mathcal{F} \neq \left\{\emptyset\right\}$, there exists an element $i \in [n]$ that is contained in at least half the sets of $\mathcal{F}$. The 3-sets conjecture of Morris states that the smallest number of distinct 3-sets (whose union is an $n$-set) that ensure Frankl's conjecture is satisfied for any UC family that contains them is $ \lfloor{n/2\rfloor} + 1$ for all $n \geq 4$. For an UC family $\mathcal{A} \subseteq 2^{[n]}$, Poonen's Theorem characterizes the existence of weights on $[n]$ which ensure all UC families that contain $\mathcal{A}$ satisfy Frankl's conjecture, however the determination of such weights for specific $\mathcal{A}$ is nontrivial even for small $n$. We classify families of 3-sets on $n \leq 9$ using a polyhedral interpretation of Poonen's Theorem and exact rational integer programming. This yields a proof of the 3-sets conjecture.
△ Less
Submitted 6 March, 2019;
originally announced March 2019.
-
Using Skip Graphs for Increased NUMA Locality
Authors:
Samuel Thomas,
Ana Hayne,
Jonad Pulaj,
Hammurabi Mendes
Abstract:
We present a data partitioning technique performed over skip graphs that promotes significant quantitative and qualitative improvements on NUMA locality in concurrent data structures, as well as reduced contention. We build on previous techniques of thread-local indexing and laziness, and, at a high level, our design consists of a partitioned skip graph, well-integrated with thread-local sequentia…
▽ More
We present a data partitioning technique performed over skip graphs that promotes significant quantitative and qualitative improvements on NUMA locality in concurrent data structures, as well as reduced contention. We build on previous techniques of thread-local indexing and laziness, and, at a high level, our design consists of a partitioned skip graph, well-integrated with thread-local sequential maps, operating without contention. As a proof-of-concept, we implemented map and relaxed priority queue ADTs using our technique. Maps were conceived using lazy and non-lazy approaches to insertions and removals, and our implementations are shown to be competitive with state-of-the-art maps. We observe a 6x higher CAS locality, a 68.6% reduction on the number of remote CAS operations, and a increase from 88.3% to 99% CAS success rate when using a lazy skip graph as compared to a control skip list (subject to the same codebase, optimizations, and implementation practices). Qualitatively speaking, remote memory accesses are not only reduced in number, but the larger the NUMA distance between threads, the larger the reduction is. We consider two alternative implementations of relaxed priority queues that further take advantage of our data partitioning over skip graphs: (a) using ``spraying'', a well-known random-walk technique usually performed over skip lists, but now performed over skip graphs; and (b) a custom protocol that traverses the skip graph deterministically, marking elements along this traversal. We provide formal arguments indicating that the first approach is more \emph{relaxed}, that is, that the span of removed keys is larger, while the second approach has smaller contention. Experimental results indicate that the approach based on spraying performs better on skip graphs, yet both seem to scale appropriately.
△ Less
Submitted 18 February, 2020; v1 submitted 18 February, 2019;
originally announced February 2019.
-
A hybrid primal heuristic for Robust Multiperiod Network Design
Authors:
Fabio D'Andreagiovanni,
Jonatan Krolikowski,
Jonad Pulaj
Abstract:
We investigate the Robust Multiperiod Network Design Problem, a generalization of the classical Capacitated Network Design Problem that additionally considers multiple design periods and provides solutions protected against traffic uncertainty. Given the intrinsic difficulty of the problem, which proves challenging even for state-of-the art commercial solvers, we propose a hybrid primal heuristic…
▽ More
We investigate the Robust Multiperiod Network Design Problem, a generalization of the classical Capacitated Network Design Problem that additionally considers multiple design periods and provides solutions protected against traffic uncertainty. Given the intrinsic difficulty of the problem, which proves challenging even for state-of-the art commercial solvers, we propose a hybrid primal heuristic based on the combination of ant colony optimization and an exact large neighborhood search. Computational experiments on a set of realistic instances from the SNDlib show that our heuristic can find solutions of extremely good quality with low optimality gap.
△ Less
Submitted 22 April, 2017;
originally announced April 2017.
-
An (MI)LP-based Primal Heuristic for 3-Architecture Connected Facility Location in Urban Access Network Design
Authors:
Fabio D'Andreagiovanni,
Fabian Mett,
Jonad Pulaj
Abstract:
We investigate the 3-architecture Connected Facility Location Problem arising in the design of urban telecommunication access networks. We propose an original optimization model for the problem that includes additional variables and constraints to take into account wireless signal coverage. Since the problem can prove challenging even for modern state-of-the art optimization solvers, we propose to…
▽ More
We investigate the 3-architecture Connected Facility Location Problem arising in the design of urban telecommunication access networks. We propose an original optimization model for the problem that includes additional variables and constraints to take into account wireless signal coverage. Since the problem can prove challenging even for modern state-of-the art optimization solvers, we propose to solve it by an original primal heuristic which combines a probabilistic fixing procedure, guided by peculiar Linear Programming relaxations, with an exact MIP heuristic, based on a very large neighborhood search. Computational experiments on a set of realistic instances show that our heuristic can find solutions associated with much lower optimality gaps than a state-of-the-art solver.
△ Less
Submitted 27 April, 2017; v1 submitted 31 December, 2015;
originally announced December 2015.
-
A Fast Hybrid Primal Heuristic for Multiband Robust Capacitated Network Design with Multiple Time Periods
Authors:
Fabio D'Andreagiovanni,
Jonatan Krolikowski,
Jonad Pulaj
Abstract:
We investigate the Robust Multiperiod Network Design Problem, a generalization of the Capacitated Network Design Problem (CNDP) that, besides establishing flow routing and network capacity installation as in a canonical CNDP, also considers a planning horizon made up of multiple time periods and protection against fluctuations in traffic volumes. As a remedy against traffic volume uncertainty, we…
▽ More
We investigate the Robust Multiperiod Network Design Problem, a generalization of the Capacitated Network Design Problem (CNDP) that, besides establishing flow routing and network capacity installation as in a canonical CNDP, also considers a planning horizon made up of multiple time periods and protection against fluctuations in traffic volumes. As a remedy against traffic volume uncertainty, we propose a Robust Optimization model based on Multiband Robustness (Büsing and D'Andreagiovanni, 2012), a refinement of classical Gamma-Robustness by Bertsimas and Sim that uses a system of multiple deviation bands. Since the resulting optimization problem may prove very challenging even for instances of moderate size solved by a state-of-the-art optimization solver, we propose a hybrid primal heuristic that combines a randomized fixing strategy inspired by ant colony optimization, which exploits information coming from linear relaxations of the problem, and an exact large neighbourhood search. Computational experiments on a set of realistic instances from the SNDlib show that our original heuristic can run fast and produce solutions of extremely high quality associated with low optimality gaps.
△ Less
Submitted 27 April, 2017; v1 submitted 21 October, 2014;
originally announced October 2014.
