Publication

A comment on performance guarantees of a greedy algorithm for minimizing a supermodular set function on comatroid

Related publications (29)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

2024

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

Non-planarity of Markoff graphs mod p

Matthew De Courcy-Ireland

We prove the non-planarity of a family of 3-regular graphs constructed from the solutions to the Markoff equation x2 + y2 + z2 = xyz modulo prime numbers greater than 7. The proof uses Euler characteristic and an enumeration of the short cycles in these gr ...

European Mathematical Soc-Ems2024

Analytical Computation of the Sensitivity Coefficients in Hybrid AC/DC Networks

Mario Paolone, Willem Lambrichts

In this paper, we present a model for the analytical computation of the power flow sensitivity coefficients (SCs) for hybrid AC/DC networks. The SCs are defined as the partial derivates of the nodal voltages with respect to the active and reactive power in ...

2024

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

A Gapless Post-quantum Hash Proof System in the Hamming Metric

Serge Vaudenay, Bénédikt Minh Dang Tran

A hash proof system (HPS) is a form of implicit proof of membership to a language. Out of the very few existing post-quantum HPS, most are based on languages of ciphertexts of code-based or lattice-based cryptosystems and inherently suffer from a gap cause ...

2023

Computer-assisted proof of kernel inequalities

Maryna Viazovska, Abhinav Kumar

This data set provides a computer-assisted proof for the kernel inequalities needed to prove universal optimality in the paper "Universal optimality of the E_8 and Leech lattices and interpolation formulas" (by Cohn, Kumar, Miller, Radchenko, and Viazovska ...

EPFL Infoscience2023

Wide-scale identification of novel/eliminated genes responsible for evolutionary transformations

Daria Korotkova

BackgroundIt is generally accepted that most evolutionary transformations at the phenotype level are associated either with rearrangements of genomic regulatory elements, which control the activity of gene networks, or with changes in the amino acid conten ...

2023

Public-Key Encryption with Quantum Keys

Khashayar Barooti

In the framework of Impagliazzo's five worlds, a distinction is often made between two worlds, one where public-key encryption exists (Cryptomania), and one in which only one-way functions exist (MiniCrypt). However, the boundaries between these worlds can ...

Springer International Publishing Ag2023

Approximation Algorithms for Allocation and Network Design

Etienne Michel François Bamas

In this thesis, we give new approximation algorithms for some NP-hard problems arising in resource allocation and network design. As a resource allocation problem, we study the Santa Claus problem (also known as the MaxMin Fair Allocation problem) in which ...

EPFL2023

Duality and bicrystals on infinite binary matrices

Thomas Gerber

The set of finite binary matrices of a given size is known to carry a finite type AA bicrystal structure. We first review this classical construction, explain how it yields a short proof of the equality between Kostka polynomials and one-dimensional sums t ...

2023

Results on Sparse Integer Programming and Geometric Independent Sets

Jana Tabea Cslovjecsek

An integer linear program is a problem of the form max{c^T x : Ax=b, x >= 0, x integer}, where A is in Z^(n x m), b in Z^m, and c in Z^n. Solving an integer linear program is NP-hard in general, but there are several assumptions for which it becomes fixed ...

EPFL2023

Byzantine-Resilient Learning Beyond Gradients: Distributing Evolutionary Search

Rachid Guerraoui, Andrei Kucharavy, Matteo Monti

Modern machine learning (ML) models are capable of impressive performances. However, their prowess is not due only to the improvements in their architecture and training algorithms but also to a drastic increase in computational power used to train them.|S ...

Assoc Computing Machinery2023

Toward Mobile Distributed Ledgers

Boi Faltings, Sujit Prakash Gujar, Dimitrios Chatzopoulos, Anurag Jain

Advances in mobile computing have paved the way for new types of distributed applications that can be executed solely by mobile devices on Device-to-Device (D2D) ecosystems (e.g., crowdsensing). Sophisticated applications, like cryptocurrencies, need distr ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2022

Gradient flow dynamics of shallow ReLU networks for square loss and orthogonal inputs

Nicolas Henri Bernard Flammarion, Loucas Pillaud-Vivien, Etienne Patrice Boursier

The training of neural networks by gradient descent methods is a cornerstone of the deep learning revolution. Yet, despite some recent progress, a complete theory explaining its success is still missing. This article presents, for orthogonal input vectors, ...

NeurIPS2022

BLOOM: Bimodal Lattice One-out-of-Many Proofs and Applications

Ngoc Khanh Karol Nguyen

We give a construction of an efficient one-out-of-many proof system, in which a prover shows that he knows the pre-image for one element in a set, based on the hardness of lattice problems. The construction employs the recent zero-knowledge framework of Ly ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Streaming and Matching Problems with Submodular Functions

Paritosh Garg

Submodular functions are a widely studied topic in theoretical computer science. They have found several applications both theoretical and practical in the fields of economics, combinatorial optimization and machine learning. More recently, there have also ...

EPFL2022

A dependence of the cost of fast controls for the heat equation on the support of initial datum

Hoài-Minh Nguyên

The controllability cost for the heat equation as the control time

T

goes to 0 is well-known of the order

e^{C/T}

for some positive constant

C

, depending on the controlled domain and for all initial datum. In this paper, we prove that the constant $C ...

2021

Computation of Al-Salam Carlitz and Askey-Wilson moments using Motzkin paths

Gaspard Ohlmann

In this paper we study the moments of polynomials from the Askey scheme, and we focus on Askey-Wilson polynomials. More precisely, we give a combinatorial proof for the case where d = 0. Their values have already been computed by Kim and Stanton in 2015, h ...

ELECTRONIC JOURNAL OF COMBINATORICS2021

Proof Of Concept Of A Graphene-Based Resonant Accelerometer

Luis Guillermo Villanueva Torrijo, Daniel Moreno Garcia

Acceleration measurements are fundamental in applications such as consumer electronics, navigation, automotive safety and Internet of things (IoT). In comparison with capacitive or piezoresistive MEMS accelerometers, resonant graphene accelerometers have t ...

IEEE2021