Publications

Adding blocked clauses to a CNF formula can substantially speed up SAT-solving, both in theory and practice. In theory, the addition of blocked clauses can exponentially reduce the length of the shortest refutation for a formula (Kullman, 1999). In practice, it has been recently shown that the runtime of CDCL solvers decreases significantly for certain instance families when blocked clauses are added as a preprocessing step. This fact is in contrast to, but not in contradiction with, prior results showing that Blocked-Clause Elimination (BCE) is sometimes an effective preprocessing. We suggest that the practical role of blocked clauses in SAT-solving might be richer than expected. Concretely, we propose a theoretical study of the complexity of Blocked-Clause Addition (BCA) as a preprocessing step for SAT-solving, and in particular, consider the problem of adding the maximum number of blocked clauses of a given arity k to an input formula F. While BCE is a confluent process, meaning that the order in which blocked clauses are eliminated is irrelevant, this is not the case for BCA: adding a blocked clause to a formula might "unblock" a different clause that was previously blocked. This order sensitivity turns out to be a crucial obstacle for carrying out BCA efficiently as a preprocessing step. Our main result is that computing the maximum number of k-ary blocked clauses that can be added to an input formula F is NP-hard for every k >= 2.

Conferences such as FUN with Algorithms routinely buy goodies (e.g., t-shirts, coffee mugs, etc) for their attendees. Often, said goodies come in different types, varying by color or design, and organizers need to decide how many goodies of each type to buy. We study the problem of buying optimal amounts of each type under a simple model of preferences by the attendees: they are indifferent to the types but want to be able to choose between more than one type of goodies at the time of their arrival. The indifference of attendees suggests that the optimal policy is to buy roughly equal amounts for every goodie type. Despite how intuitive this conjecture sounds, we show that this simple model of assortment optimization is quite rich, and even though we make progress towards proving the conjecture (e.g., we succeed when the number of goodie types is 2 or 3), the general case with K types remains open. We also present asymptotic results and computer simulations, and finally, to motivate further progress, we offer a reward of $100usd for a full proof.

We present and analyze PackIt!, a turn-based game consisting of packing rectangles on an n \times n grid. PackIt! can be easily played on paper, either as a competitive two-player game or in solitaire fashion. On the t-th turn, a rectangle of area t or t+1 must be placed in the grid. In the two-player format of PackIt! whichever player places a rectangle last wins, whereas the goal in the solitaire variant is to perfectly pack the n \times n grid. We analyze conditions for the existence of a perfect packing over n \times n, then present an automated reasoning approach that allows finding perfect games of PackIt! up to n=50 which includes a novel SAT-encoding technique of independent interest, and conclude by proving an NP-hardness result.

Almost identical mathematical problems can result in wildly different solutions. In this piece of counterfactual history, Bernardo Subercaseaux and Marijn Heule discuss two graph theoretic problems that Leonhard Euler did not have the opportunity to meet. While the proof for the first problem can be elegantly summarized into a paragraph, thanks to Euler’s results, the shortest proof known for the second problem uses over 30 terabytes of data. Therefore, we argue that despite his mathematical genius, Euler would not have been able to solve the latter problem. The almost alien prolificity of the Swiss mathema- tician makes him a perfect fictitious intermediary for discussing the divide between the world of human mathematics and the world of computational mathematics.

We present a comprehensive demonstration of how automated reasoning can assist mathematical research, both in the discovery of conjectures and in their verification. Our focus is a discrete geometry problem: What is \{}mu _{5}(n)\{μ5(n), the minimum number of convex pentagons induced by n points in the plane? In the first stage toward tackling this problem, automated reasoning tools guide discovery and conjectures: we use SAT-based tools to find abstract configurations of points that would induce few pentagons. Afterward, we use Operations Research tools to find and visualize realizations of these configurations in the plane, if they exist. Mathematical thought and intuition are still vital parts of the process for turning the obtained visualizations into general constructions. A surprisingly simple upper bound follows from our constructions: \{}mu _{5}(n) }le }left( {}begin{array}{c}}lfloor n/2 }rfloor }} 5}end{array}}}right) + }left( {}begin{array}{c}}lceil n/2 }rceil }} 5}end{array}}}right) \{μ5(n)≤⌊n/2⌋5+⌈n/2⌉5, and we conjecture it is optimal. In the second stage, we turn our focus to verifying this conjecture. Using MaxSAT, we confirm that \{}mu _5(n)\{μ5(n)matches the conjectured values for \\n }le 16\\n≤16, thereby improving both the existing lower and upper bounds for \\n }in [12, 16]\\n∈[12,16]. Our MaxSAT results rely on two mathematical theorems with pen-and-paper proofs, highlighting once again the rich interplay between automated and traditional mathematics.

Erd\Hos and Guy (1973) initiated a line of research studying \mu_k(n), the minimum number of convex k-gons one can obtain by placing n points in the plane without any three of them being collinear. Asymptotically, the limits c_k := \lim_n\to ∞ \mu_k(n)/\binomnk exist for all k, and are strictly positive due to the Erdős-Szekeres theorem. This article focuses on the case k=5, where c_5 was known to be between 0.0608516 and 0.0625 (Goaoc et al. 2018, Subercaseaux et al. 2023). The lower bound was obtained through the Flag Algebra method of Razborov (2007), using semi-definite programming. In this article we prove a more modest lower bound of \frac5\sqrt5-114 ≈0.04508 without any computation; we exploit \emph“planar-point equations” that count, in different ways, the number of convex pentagons (or other geometric objects) in a point placement. To derive our lower bound we combine such equations by viewing them from a statistical perspective, which we believe can be fruitful for other related problems.

Radio 2-colorings of graphs are a generalization of vertex colorings motivated by the problem of assigning frequency channels in radio networks. In a radio 2-coloring of a graph, vertices are assigned integer colors so that the color of two vertices u and v differ by at least 2 if u and v are neighbors, and by at least 1 if u and v have a common neighbor. Our work improves the best-known bounds for optimal radio 2-colorings of small hypercube graphs, a combinatorial problem that has received significant attention in the past. We do so by using automated reasoning techniques such as symmetry breaking and Cube and Conquer, obtaining that for n = 7 and n = 8, the coding-theory upper bounds of Whittlesey et al. (1995) are not tight. Moreover, we prove the answer for n=7 to be either 12 or 13, thus making a substantial step towards answering an open problem by Knuth (2015). Finally, we include several combinatorial observations that might be useful for further progress, while also arguing that fully determining the answer for n=7 will require new techniques.

A packing k-coloring is a natural variation on the standard notion of graph k-coloring, where vertices are assigned numbers from {1, \ldots, k}, and any two vertices assigned a common color c ∈{1, \ldots, k} need to be at a distance greater than c (as opposed to 1, in standard graph colorings). Despite a sequence of incremental work, determining the packing chromatic number of the infinite square grid has remained an open problem since its introduction in 2002. We culminate the search by proving this number to be 15. We achieve this result by improving the best-known method for this problem by roughly two orders of magnitude. The most important technique to boost performance is a novel, surprisingly effective propositional encoding for packing colorings. Additionally, we developed an alternative symmetry-breaking method. Since both new techniques are more complex than existing techniques for this problem, a verified approach is required to trust them. We include both techniques in a proof of unsatisfiability, reducing the trusted core to the correctness of the direct encoding.

We study \mu_5(n), the minimum number of convex pentagons induced by n points in the plane in general position. Despite a significant body of research in understanding \mu_4(n), the variant concerning convex quadrilaterals, not much is known about \mu_5(n). We present two explicit constructions, inspired by point placements obtained through a combination of Stochastic Local Search and a program for realizability of point sets, that provide \mu_5(n) ≤⌊n/2⌋ \choose 5 + ⌈n/2⌉ \choose 5. Furthermore, we conjecture this bound to be optimal, and provide partial evidence by leveraging a MaxSAT encoding that allows us to verify our conjecture for n ≤16.

Formal XAI (explainable AI) is a growing area that focuses on computing explanations with mathematical guarantees for the decisions made by ML models. Inside formal XAI, one of the most studied cases is that of explaining the choices taken by decision trees, as they are traditionally deemed as one of the most interpretable classes of models. Recent work has focused on studying the computation of sufficient reasons, a kind of explanation in which given a decision tree T and an instance x, one explains the decision T(x) by providing a subset y of the features of x such that for any other instance z compatible with y, it holds that T(z) = T(x), intuitively meaning that the features in y are already enough to fully justify the classification of x by T. It has been argued, however, that sufficient reasons constitute a restrictive notion of explanation. For such a reason, the community has started to study their probabilistic counterpart, in which one requires that the probability of T(z) = T(x) must be at least some value δ∈(0, 1], where z is a random instance that is compatible with y. Our paper settles the computational complexity of δ-sufficient-reasons over decision trees, showing that both (1) finding δ-sufficient-reasons that are minimal in size, and (2) finding δ-sufficient-reasons that are minimal inclusion-wise, do not admit polynomial-time algorithms (unless P = NP). This is in stark contrast with the deterministic case (δ= 1) where inclusion-wise minimal sufficient-reasons are easy to compute. By doing this, we answer two open problems originally raised by Izza et al., and extend the hardness of explanations for Boolean circuits presented by Wäldchen et al. to the more restricted case of decision trees. On the positive side, we identify structural restrictions of decision trees that make the problem tractable, and show how SAT solvers might be able to tackle these problems in practical settings.

The growing body of work in learning-augmented online algorithms studies how online algorithms can be improved when given access to ML predictions about the future. Motivated by ML models that give a confidence parameter for their predictions, we study online algorithms with predictions that are ε-accurate: namely, each prediction is correct with probability (at least) ε, but can be arbitrarily inaccurate with the remaining probability. We show that even with predictions that are accurate with a small probability and arbitrarily inaccurate otherwise, we can dramatically outperform worst-case bounds for a range of classical online problems including caching, online set cover, and online facility location. Our main results are an O(\log(1/\varepsilon))-competitive algorithm for caching, and a simple O(1/\varepsilon)-competitive algorithm for a large family of covering problems, including set cover and facility location, with ε-accurate predictions.

Wordle is a single-player word-guessing game where the goal is to discover a secret word w that has been chosen from a dictionary D. In order to discover w, the player can make at most 𝓁 guesses, which must also be words from D, all words in D having the same length k. After each guess, the player is notified of the positions in which their guess matches the secret word, as well as letters in the guess that appear in the secret word in a different position. We study the game of Wordle from a complexity perspective, proving NP-hardness of its natural formalization: to decide given a dictionary D and an integer 𝓁 if the player can guarantee to discover the secret word within 𝓁 guesses. Moreover, we prove that hardness holds even over instances where words have length k = 5, and that even in this case it is NP-hard to approximate the minimum number of guesses required to guarantee discovering the secret word. We also present results regarding its parameterized complexity and offer some related open problems.

A packing k-coloring of a graph G = (V, E) is a mapping from V to 1, ..., k such that any pair of vertices u, v that receive the same color c must be at distance greater than c in G. Arguably the most fundamental problem regarding packing colorings is to determine the packing chromatic number of the infinite square grid. A sequence of previous works has proved this number to be between 13 and 15. Our work improves the lower bound to 14. Moreover, we present a new encoding that is asymptotically more compact than the previously used ones.

The game of Hangman is a classical asymmetric two player game in which one player, the setter, chooses a secret word from a language, that the other player, the guesser, tries to discover through single letter matching queries, answered by all occurrences of this letter if any. In the Evil Hangman variant, the setter can change the secret word during the game, as long as the new choice is consistent with the information already given to the guesser. We show that a greedy strategy for Evil Hangman can perform arbitrarily far from optimal, and most importantly, that playing optimally as an Evil Hangman setter is computationally difficult. The latter result holds even assuming perfect knowledge of the language, for several classes of languages, ranging from Finite to Turing Computable. The proofs are based on reductions to Dominating Set on 3-regular graphs and to the Membership problem, combinatorial problems already known to be computationally hard.

Several queries and scores have been proposed to explain individual predictions made by ML models. Examples include queries based on “anchors", which are parts of an instance that are sufficient to justify its classification, and ”feature perturbation" scores such as SHAP. Given the need for flexible, reliable, and easy-to-apply interpretability methods for ML models, we foresee the need for developing declarative languages to naturally specify different explainability queries. We do this in a principled way by rooting such a language in a logic called FOIL, that allows for expressing many simple but important explainability queries, and might serve as a core for more expressive interpretability languages. We study the computational complexity of FOIL queries over classes of ML models often deemed to be easily interpretable: decision trees and more general decision diagrams. Since the number of possible inputs for an ML model is exponential in its dimension, tractability of the FOIL evaluation problem is delicate, but can be achieved by either restricting the structure of the models, or the fragment of FOIL being evaluated. We also present a prototype implementation of FOIL wrapped in a high-level declarative language, and perform experiments showing that such a language can be used in practice.

In spite of several claims stating that some models are more interpretable than others – e.g., "linear models are more interpretable than deep neural networks" – we still lack a principled notion of interpretability to formally compare among different classes of models. We make a step towards such a notion by studying whether folklore interpretability claims have a correlate in terms of computational complexity theory. We focus on local post-hoc explainability queries that, intuitively, attempt to answer why individual inputs are classified in a certain way by a given model. In a nutshell, we say that a class \mathcalC_1 of models is more interpretable than another class \mathcalC_2, if the computational complexity of answering post-hoc queries for models in \mathcalC_2 is higher than for those in \mathcalC_1. We prove that this notion provides a good theoretical counterpart to current beliefs on the interpretability of models; in particular, we show that under our definition and assuming standard complexity-theoretical assumptions (such as P\neqNP), both linear and tree-based models are strictly more interpretable than neural networks. Our complexity analysis, however, does not provide a clear-cut difference between linear and tree-based models, as we obtain different results depending on the particular post-hoc explanations considered. Finally, by applying a finer complexity analysis based on parameterized complexity, we are able to prove a theoretical result suggesting that shallow neural networks are more interpretable than deeper ones.

Despite the growing interest in interpretability for machine learning models, there seems to be a gap between the world of researchers and that of practitioners and data scientists. Declarative languages, tailored for interactive interpretability and bias detection of models, could be a step towards shortening such a gap. Based on requirements often posed over interpretability tasks, it is desirable for such languages to be interactive, model agnostic, faithful to the models, and have clear and well-understood semantics and complexity. A reasonable way to meet several of these requirements is by having a language strongly rooted in logic. As a first step towards the design of such language, we study how interpretability and bias detection queries can be expressed in first-order logic (FO) –arguably, one of the most prominent logics in different areas of computer science– over a suitable encoding of machine learning models. We then study the computational complexity of evaluating FO formulae over linear-based, tree-based and deep models. Evaluation is shown to be easier for decision trees and perceptrons than it is for deep neural networks, which seems validated by folklore assumptions of the field. Finally, we discuss possible extensions to the underlying logical structure and how they enhance expressiveness, as well as possible directions towards tractability.

We study the expressive power of the LARA language – a recently proposed unified model for expressing relational and linear algebra operations – both in terms of traditional database query languages and some analytic tasks often performed in machine learning pipelines. We start by showing LARA to be expressive complete with respect to first-order logic with aggregation. Since LARA is parameterized by a set of user-defined functions which allow to transform values in tables, the exact expressive power of the language depends on how these functions are defined. We distinguish two main cases depending on the level of genericity queries are enforced to satisfy. Under strong genericity assumptions the language cannot express matrix convolution, a very important operation in current machine learning operations. This language is also local, and thus cannot express operations such as matrix inverse that exhibit a recursive behavior. For expressing convolution, one can relax the genericity requirement by adding an underlying linear order on the domain. This, however, destroys locality and turns the expressive power of the language much more difficult to understand. In particular, although under complexity assumptions the resulting language can still not express matrix inverse, a proof of this fact without such assumptions seems challenging to obtain.

Tensors are one of the most widely used data structures in modern Machine Learning applications. Although they provide a flexible way of storing and accessing data, they often expose too many low-level details that may result in error prone code that is difficult to maintain and extend. Abstracting low-level functionalities into high-level operators in the form of a query language is a task in which the Data Management community has extensive experience. It is thus important to understand how such an experience can be applied in the design of useful languages for tensor manipulation. In this short paper we study a matrix and a tensor query language that have been recently proposed in the database literature. We show, by using examples, how these proposals are in line with the practical interest in rethinking tensor abstractions. On the technical side, we compare the two languages in terms of operators that naturally arise in Machine Learning pipelines, such as convolution, matrix-inverse, and Einstein summation. We hope our results to provide a theoretical kick-off for the discussion on the design of core declarative query languages for tensors.

The wavelet tree is a data structure to succinctly represent sequences of elements over a fixed but potentially large alphabet. It is a very versatile data structure which exhibits interesting properties even when its compression capabilities are not considered, efficiently supporting several queries. Although the wavelet tree was proposed more than a decade ago, it has not yet been widely used by the competitive programming community. This paper tries to fill the gap by showing how this data structure can be used in classical competitive programming problems, discussing some implementation details, and presenting a performance analysis focused in a competitive programming setting.