arXiv subjects

Kenan Wood

Publications and source records attributed to Kenan Wood.

6 recordsLinked to original sources

arXiv2025

Satisfiability Modulo Theories for Verifying MILP Certificates

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 formally verify the correctness of our schema at the logical level using Why3's automated deductive logic framework. Furthermore, we implement a checker for VIPR certificates by expressing our formally verified 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.

cs.LO↗

arXiv2024

Bilevel Programming for Pebbling Numbers of Lemke Graph Products

Given a configuration of indistinguishable pebbles on the vertices of a graph, 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 least integer such that any configuration with that many pebbles and any target vertex, some sequence of pebbling moves can place a pebble on the target. Graham's conjecture asserts that the pebbling number of the cartesian product of two graphs is at most the product of the two graphs' pebbling numbers. Products of so-called Lemke graphs are widely thought to be the most likely counterexamples to Graham's conjecture, provided one exists. In this paper, we introduce a novel framework for computing pebbling numbers using bilevel optimization. We use this approach to algorithmically show that the pebbling numbers of all products of 8-vertex Lemke graphs are consistent with Graham's conjecture, with the added assumption that pebbles can only be placed on a set of at most four vertices.

math.CO↗

arXiv2024

Optimal Multilevel Slashing for Blockchains

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.

cs.DC↗

arXiv2024

Distributed Agreement in the Arrovian Framework

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.

cs.DC↗

arXiv2024

Local Configurations in Union-Closed Families

The Frankl or Union-Closed Sets conjecture states that for any finite union-closed family of sets $\mathcal{F}$ containing some nonempty set, there is some element $i$ in the ground set $U(\mathcal F) := \bigcup_{S \in \mathcal{F}} S$ of $\mathcal{F}$ such that $i$ is in at least half of the sets in $\mathcal{F}$. In this work, we find new values and bounds for the least integer $FC(k, n)$ such that any union-closed family containing $FC(k, n)$ distinct $k$-sets of an $n$-set $X$ satisfies Frankl's conjecture with an element of $X$. Additionally, we answer an older question of Vaughan regarding symmetry in union-closed families and we give a proof of a recent question posed by Ellis, Ivan and Leader. Finally, we introduce novel local configuration criteria through a generalization of Poonen's Theorem to prove the conjecture for many, previously unknown classes of families.

math.CO↗

arXiv2024

Expiring Assets in Automated Market Makers

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.

q-fin.TR↗