Learning formulas in Linear Temporal Logic ( $${\textbf {LTL}}_f $$ ) from finite traces is a fundamental research problem which has found applications in artificial intelligence, software engineering, programming languages, formal methods, control of cyber-physical systems, and robotics. We implement a new CPU tool called Bolt improving over the state of the art by learning formulas more than 100x faster over 70% of the benchmarks, with smaller or equal formulas in 98% of the cases. Our key insight is to leverage a problem called Boolean Set Cover as a subroutine to combine existing formulas using Boolean connectives. Thanks to the Boolean Set Cover component, our approach offers a novel trade-off between efficiency and formula size.

Efficiently computing accurate representations of high-dimensional data is essential for data analysis and unsupervised learning. Dendrograms, also known as ultrametrics, are widely used representations that preserve hierarchical relationships within the data. However, popular methods for computing them, such as *linkage* algorithms, suffer from quadratic time and space complexity, making them impractical for large datasets. The "best ultrametric embedding" (a.k.a. "best ultrametric fit") problem, which aims to find the ultrametric that best preserves the distances between points in the original data, is known to require at least quadratic time for an exact solution. Recent work has focused on improving scalability by approximating optimal solutions in subquadratic time, resulting in a (sqrt(2) + epsilon)-approximation (Cohen-Addad, de Joannis de Verclos and Lagarde, 2021). In this paper, we present the first subquadratic algorithm that achieves arbitrarily precise approximations of the optimal ultrametric embedding. Specifically, we provide an algorithm that, for any c >1, outputs a c-approximation of the best ultrametric in time O(n^(1 + 1/c)). In particular, for any fixed epsilon > 0, the algorithm computes a (1+ epsilon)-approximation in time O(n^(2 - epsilon + o(epsilon ^2))). Experimental results show that our algorithm improves upon previous methods in terms of approximation quality while maintaining comparable running times.

International audience

International audience

International audience

International audience

We describe DreyFVS, a heuristic for Directed Feedback Vertex Set submitted to the 2022 edition of Parameterized Algorithms and Computational Experiments Challenge. The Directed Feedback Vertex Set problem asks to remove a minimal number of vertices from a digraph such that the resulting digraph is acyclic. Our algorithm first performs a guess on a reduced instance by leveraging the Sinkhorn-Knopp algorithm, to then improve this solution by pipelining two local search methods.

In this work, we revisit the problem of testing membership in regular languages, first studied by Alon et al. [Alon et al., 2001]. We develop a one-sided error property tester for regular languages under weighted edit distance that makes 𝒪(ε^{-1} log(1/ε)) non-adaptive queries, assuming that the language is described by an automaton of constant size. Moreover, we show a matching lower bound, essentially closing the problem for the edit distance. As an application, we improve the space bound of the current best streaming property testing algorithm for visibly pushdown languages from 𝒪(ε^{-4} log⁶ n) to 𝒪(ε^{-3} log⁵ n log log n), where n is the size of the input. Finally, we provide a Ω(max(ε^{-1}, log n)) lower bound on the memory necessary to test visibly pushdown languages in the streaming model, significantly narrowing the gap between the known bounds.

This document describes our exact Cluster Editing solver, PaSTEC, which got the third place in the 2021 PACE Challenge.

International audience