Bernardo Subercaseaux | Publications

My most up-to-date list of papers is usually on Google Scholar, but this page is my tidier, annotated list, with BibTeX, abstracts, and links whenever they are available.

Some datapoints

Erdős number: 3 (for example, Paul Erdős → Noga Alon → Daniel Lokshtanov → me).
Collaborators from: Austria, Chile, China, France, Germany, India, Japan, the Netherlands, Norway, Portugal, Russia, Slovakia, Spain, and the USA.
Most common conference: NeurIPS (five papers). Actively trying to change this 🙃.
Most fun conference: FUN with Algorithms.
Distinctions: Best paper at CICM 2025 and LPAR 2023; distinguished paper at PODS 2025; runner-up for best paper at CICM 2024; best-paper nomination at TACAS 2023; spotlights at NeurIPS 2021 and AFCI@NeurIPS 2020; and first place in the IEEE LA-CCI Latin American master's thesis contest in AI.

Citations by year

615 total citations · h-index 12

Google Scholar · Aug 2026 (2026 YTD)

Papers

2026

Computing NP-hard Repetitiveness Measures via MAX-SAT

Hideo Bannai, Keisuke Goto, Masakazu Ishihata, Shunsuke Kanda, Dominik Köppl, Takaaki Nishimoto, and Bernardo Subercaseaux

ACM Trans. Algorithms 2026

HTML

Repetitiveness measures reveal profound characteristics of datasets, and give rise to compressed data structures and algorithms working in compressed space. Alas, the computation of some of these measures is NP-hard, and straight-forward computation is infeasible for datasets of even small sizes. Three such measures are the smallest size of a string attractor, the smallest size of a bidirectional macro scheme, and the smallest size of a straight-line program. While a vast variety of implementations for heuristically computing approximations exist, exact computation of these measures has received little to no attention. In this paper, we present MAX-SAT formulations that provide the first non-trivial implementations for exact computation of smallest string attractors, smallest bidirectional macro schemes, and smallest straight-line programs. Computational experiments show that our implementations work for texts of length up to a few hundred for straight-line programs and bidirectional macro schemes, and texts even over a million for string attractors.
@article{bannai2026repetitiveness, author = {Bannai, Hideo and Goto, Keisuke and Ishihata, Masakazu and Kanda, Shunsuke and K{\"{o}}ppl, Dominik and Nishimoto, Takaaki and Subercaseaux, Bernardo}, title = {Computing NP-hard Repetitiveness Measures via {MAX-SAT}}, journal = {{ACM} Trans. Algorithms}, volume = {22}, number = {2}, pages = {15:1--15:25}, year = {2026}, url = {https://doi.org/10.1145/3777895}, doi = {10.1145/3777895} }
A Demigod’s Number for the Rubik’s Cube

Arturo Merino, and Bernardo Subercaseaux

In FUN 2026

arXiv HTML PDF

It is well-known by now that any state of the $3\times 3 \times 3$ Rubik's Cube can be solved in at most 20 moves, a result often referred to as "God's Number". However, this result took Rokicki et al. around 35 CPU years to prove and is therefore very challenging to reproduce. We provide a novel approach to obtain a worse bound of 36 moves with high confidence, but that offers two main advantages: (i) it is easy to understand, reproduce, and verify, and (ii) our main idea generalizes to bounding the diameter of other vertex-transitive graphs by at most twice its true value, hence the name "demigod number". Our approach is based on the fact that, for vertex-transitive graphs, the average distance between vertices is at most half the diameter, and by sampling uniformly random states and using a modern solver to obtain upper bounds on their distance, a standard concentration bound allows us to confidently state that the average distance is around $18.32 \pm 0.1$, from where the diameter is at most $36$.
@inproceedings{merino2025demigodsNumber, author = {Merino, Arturo and Subercaseaux, Bernardo}, editor = {Iacono, John}, title = {A Demigod's Number for the Rubik's Cube}, booktitle = {13th International Conference on Fun with Algorithms, {FUN} 2026, Porquerolles, France, May 18-22, 2026}, series = {LIPIcs}, volume = {366}, pages = {31:1--31:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2026}, url = {https://doi.org/10.4230/LIPIcs.FUN.2026.31}, doi = {10.4230/LIPICS.FUN.2026.31} }
Solving Small Rubik’s Cubes as Slowly as Possible

Jenny Quan, Noah Kim, Bernardo Subercaseaux, and John Mackey

In FUN 2026

HTML

We study, for different Rubik's puzzles, whether from any starting state one can solve the puzzle as slowly as possible, visiting every reachable state exactly once before reaching the solved configuration. This question corresponds to the existence of Hamiltonian paths (ending in the solved state) in the Cayley graphs associated with these puzzles. A major conjecture attributed to Lovász is that every Cayley graph has a Hamiltonian path. An even stronger version of the conjecture, considered by Dupuis and Wagon (2015) and Gregor et al. (2024), is that every Cayley graph of degree at least 3 is either bipartite and has Hamiltonian paths between any pair of vertices on opposite parts, or is non-bipartite and has Hamiltonian paths between any pair of vertices. Our study of slowly solving Rubik's puzzles amounts to studying this Strong Lovász Conjecture in their respective Cayley graphs. We first verify the Strong Lovász Conjecture computationally for small Rubik's puzzles like the $1 \times 2 \times 3$ or $1 \times 3 \times 3$ cuboids, which have under 200 states. This approach, however, becomes infeasible for the $2 \times 2 \times 2$, which has over 3.6 million states. Our main result is then showing that the Strong Lovász Conjecture holds for the $2 \times 2 \times 2$ cube, using a careful graph-theoretic construction based on the subgroup induced by the R and U turns.
@inproceedings{quan2026slowRubiks, author = {Quan, Jenny and Kim, Noah and Subercaseaux, Bernardo and Mackey, John}, editor = {Iacono, John}, title = {Solving Small Rubik's Cubes as Slowly as Possible}, booktitle = {13th International Conference on Fun with Algorithms, {FUN} 2026, Porquerolles, France, May 18-22, 2026}, series = {LIPIcs}, volume = {366}, pages = {38:1--38:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2026}, url = {https://doi.org/10.4230/LIPIcs.FUN.2026.38}, doi = {10.4230/LIPICS.FUN.2026.38} }
Price of Locality in Permutation Mastermind: Are TikTok Influencers Chaotic Enough?

Bernardo Subercaseaux

In FUN 2026

arXiv HTML PDF

In the permutation Mastermind game, the goal is to uncover a secret permutation $σ^\star \colon [n] \to [n]$ by making a series of guesses $π_1, \ldots, π_T$ which must also be permutations of $[n]$, and receiving as feedback after guess $π_t$ the number of positions $i$ for which $σ^\star(i) = π_t(i)$. While the existing literature on permutation Mastermind suggests strategies in which $π_t$ and $π_{t+1}$ might be widely different permutations, a resurgence in popularity of this game as a TikTok trend shows that humans (or at least TikTok influencers) use strategies in which consecutive guesses are very similar. For example, it is common to see players attempt one transposition at a time and slowly see their score increase. Motivated by these observations, we study the theoretical impact of two forms of "locality" in permutation Mastermind strategies: $\ell_k$-local strategies, in which any two consecutive guesses differ in at most $k$ positions, and the even more restrictive class of $w_k$-local strategies, in which consecutive guesses differ in a window of length at most $k$. We show that, in broad terms, the optimal number of guesses for local strategies is quadratic, and thus much worse than the $O(n \lg n)$ guesses that suffice for non-local strategies. We also show NP-hardness of the satisfiability version for $\ell_3$-local strategies, whereas in the $\ell_2$-local variant the problem admits a randomized polynomial algorithm.
@inproceedings{subercaseaux2026priceOfLocality, author = {Subercaseaux, Bernardo}, editor = {Iacono, John}, title = {Price of Locality in Permutation Mastermind: Are TikTok Influencers Chaotic Enough?}, booktitle = {13th International Conference on Fun with Algorithms, {FUN} 2026, Porquerolles, France, May 18-22, 2026}, series = {LIPIcs}, volume = {366}, pages = {39:1--39:21}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2026}, url = {https://doi.org/10.4230/LIPIcs.FUN.2026.39}, doi = {10.4230/LIPICS.FUN.2026.39} }
Near-Optimal Encodings of Cardinality Constraints

Andrew Krapivin, Benjamin Przybocki, and Bernardo Subercaseaux

In SAT 2026

arXiv HTML PDF

We present several novel encodings for cardinality constraints, which use fewer clauses than previous encodings and, more importantly, introduce new generally applicable techniques for constructing compact encodings. First, we present a CNF encoding for the $\text{AtMostOne}(x_1,\dots,x_n)$ constraint using $2n + 2 \sqrt{2n} + O(\sqrt[3]{n})$ clauses, thus refuting the conjectured optimality of Chen's product encoding. Our construction also yields a smaller monotone circuit for the threshold-2 function, improving on a 50-year-old construction of Adleman and incidentally solving a long-standing open problem in circuit complexity. On the other hand, we show that any encoding for this constraint requires at least $2n + \sqrt{n+1} - 2$ clauses, which is the first nontrivial unconditional lower bound for this constraint and answers a question of Kučera, Savický, and Vorel. We then turn our attention to encodings of $\text{AtMost}_k(x_1,\dots,x_n)$, where we introduce "grid compression", a technique inspired by hash tables, to give encodings using $2n + o(n)$ clauses as long as $k = o(\sqrt[3]{n})$ and $4n + o(n)$ clauses as long as $k = o(n)$. Previously, the smallest known encodings were of size $(k+1)n + o(n)$ for $k \le 5$ and $7n - o(n)$ for $k \ge 6$.
@inproceedings{krapivin2026nearOptimalEncodings, author = {Krapivin, Andrew and Przybocki, Benjamin and Subercaseaux, Bernardo}, editor = {Ignatiev, Alexey and Szeider, Stefan}, title = {Near-Optimal Encodings of Cardinality Constraints}, booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2026, Lisbon, Portugal, July 20-23, 2026}, series = {LIPIcs}, volume = {377}, pages = {23:1--23:17}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2026}, url = {https://doi.org/10.4230/LIPIcs.SAT.2026.23}, doi = {10.4230/LIPICS.SAT.2026.23} }
Automated Reencoding Meets Graph Theory

Benjamin Przybocki, Bernardo Subercaseaux, and Marijn J. H. Heule

In SAT 2026

arXiv HTML PDF

Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can be constructed by an idealized BVA algorithm. Based on this insight, we prove new results about the behavior and limitations of BVA and its interaction with other preprocessing techniques. We show that idealized BVA, plus some minor additional preprocessing (e.g., equivalent literal substitution), can reencode any 2-CNF formula with $n$ variables into an equivalent 2-CNF formula with $(\tfrac{\lg(3)}{4}+o(1))\,\tfrac{n^2}{\lg n}$ clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from $\tfrac{\lg(3)}{4} \approx 0.396$ to $1$, and that no reencoding method can achieve a constant below $0.25$. On the other hand, for the at-most-one constraint on $n$ variables, we prove that idealized BVA cannot reencode this constraint using fewer than $3n-6$ clauses, a bound that we prove is achieved by actual implementations. In particular, this shows that the product encoding for at-most-one, which uses $2n+o(n)$ clauses, cannot be constructed by BVA regardless of the heuristics used. Finally, our graph-theoretic characterization of BVA allows us to leverage recent work in algorithmic graph theory to develop a drastically more efficient implementation of BVA that achieves a comparable clause reduction on random monotone 2-CNF formulas.
@inproceedings{przybocki2026automatedReencoding, author = {Przybocki, Benjamin and Subercaseaux, Bernardo and Heule, Marijn J. H.}, editor = {Ignatiev, Alexey and Szeider, Stefan}, title = {Automated Reencoding Meets Graph Theory}, booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2026, Lisbon, Portugal, July 20-23, 2026}, series = {LIPIcs}, volume = {377}, pages = {29:1--29:17}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2026}, url = {https://doi.org/10.4230/LIPIcs.SAT.2026.29}, doi = {10.4230/LIPICS.SAT.2026.29} }
Optimal and Efficient Partite Decompositions of Hypergraphs

Andrew Krapivin, Benjamin Przybocki, Nicolás Sanhueza-Matamala, and Bernardo Subercaseaux

In STOC 2026

arXiv HTML PDF

We study the problem of partitioning the edges of a $d$-uniform hypergraph $H$ into a family $F$ of complete $d$-partite hypergraphs ($d$-cliques). We show that there is a partition $F$ in which every vertex $v \in V(H)$ belongs to at most $(\frac{1}{d!} + o_d(1))n^{d-1}/\lg n$ members of $F$. This settles the central question of a line of research initiated by Erdős and Pyber (1997) for graphs, and more recently by Csirmaz, Ligeti, and Tardos (2014) for hypergraphs. The $d=2$ case of this theorem answers a 40-year-old question of Chung, Erdős, and Spencer (1983). An immediate corollary of our result is an improved upper bound for the maximum share size for binary secret sharing schemes on uniform hypergraphs. Building on results of Nechiporuk (1969), we prove that every graph with fixed edge density $γ\in (0,1)$ has a biclique partition of total weight at most $(\tfrac{1}{2}+o(1))\cdot h_2(γ) \frac{n^2}{\lg n}$, where $h_2$ is the binary entropy function. Our construction implies that such biclique partitions can be constructed in time $O(m)$, which answers a question of Feder and Motwani (1995) and also improves upon results of Mubayi and Turán (2010) as well as Chavan, Rabinia, Grosu, and Brocanelli (2025). Using similar techniques, we also give an $n^{1+o(1)}$ algorithm for finding a subgraph $K_{t,t}$ with $t = (1-o(1)) \fracγ{h_2(γ)} \lg n$. Our results show that biclique partitions are information-theoretically optimal representations for graphs at every fixed density. We show that with this succinct representation one can answer independent set queries and cut queries in time $O(n^2/ \lg n)$, and if we increase the space usage by a constant factor, we can compute a $2α$-approximation for the densest subgraph problem in time $O(n^2/\lg α)$ for any $α> 1$.
@inproceedings{krapivin2025partiteDecompositions, author = {Krapivin, Andrew and Przybocki, Benjamin and Sanhueza{-}Matamala, Nicol{\'{a}}s and Subercaseaux, Bernardo}, editor = {Bhaskara, Aditya and Czumaj, Artur}, title = {Optimal and Efficient Partite Decompositions of Hypergraphs}, booktitle = {Proceedings of the 58th Annual {ACM} Symposium on Theory of Computing, {STOC} 2026, Salt Lake City, UT, USA, June 22-26, 2026}, pages = {2187--2198}, publisher = {{ACM}}, year = {2026}, url = {https://doi.org/10.1145/3798129.3800921}, doi = {10.1145/3798129.3800921} }
Accelerating Scientific Research with Gemini: Case Studies and Common Techniques

David P. Woodruff, Vincent Cohen-Addad, Lalit Jain, Jieming Mao, Song Zuo, MohammadHossein Bateni, Simina Brânzei, Michael P. Brenner, Lin Chen, Ying Feng, Lance Fortnow, Gang Fu, Ziyi Guan, Zahra Hadizadeh, Mohammad T. Hajiaghayi, Mahdi JafariRaviz, Adel Javanmard, Karthik C. S., Ken-ichi Kawarabayashi, Ravi Kumar, Silvio Lattanzi, Euiwoong Lee, Yi Li, Ioannis Panageas, Dimitris Paparas, Benjamin Przybocki, Bernardo Subercaseaux, Ola Svensson, Shayan Taherijam, Xuan Wu, Eylon Yogev, Morteza Zadimoghaddam, Samson Zhou, Yossi Matias, James Manyika, and Vahab Mirrokni

CoRR 2026

arXiv HTML PDF

Recent advances in large language models (LLMs) have opened new avenues for accelerating scientific research. While models are increasingly capable of assisting with routine tasks, their ability to contribute to novel, expert-level mathematical discovery is less understood. We present a collection of case studies demonstrating how researchers have successfully collaborated with advanced AI models, specifically Google's Gemini-based models (in particular Gemini Deep Think and its advanced variants), to solve open problems, refute conjectures, and generate new proofs across diverse areas in theoretical computer science, as well as other areas such as economics, optimization, and physics. Based on these experiences, we extract common techniques for effective human-AI collaboration in theoretical research, such as iterative refinement, problem decomposition, and cross-disciplinary knowledge transfer. While the majority of our results stem from this interactive, conversational methodology, we also highlight specific instances that push beyond standard chat interfaces. These include deploying the model as a rigorous adversarial reviewer to detect subtle flaws in existing proofs, and embedding it within a "neuro-symbolic" loop that autonomously writes and executes code to verify complex derivations. Together, these examples highlight the potential of AI not just as a tool for automation, but as a versatile, genuine partner in the creative process of scientific discovery.
@article{woodruff2026gemini, author = {Woodruff, David P. and Cohen{-}Addad, Vincent and Jain, Lalit and Mao, Jieming and Zuo, Song and Bateni, MohammadHossein and Br{\^{a}}nzei, Simina and Brenner, Michael P. and Chen, Lin and Feng, Ying and Fortnow, Lance and Fu, Gang and Guan, Ziyi and Hadizadeh, Zahra and Hajiaghayi, Mohammad T. and JafariRaviz, Mahdi and Javanmard, Adel and {Karthik {C. S.}} and Kawarabayashi, Ken{-}ichi and Kumar, Ravi and Lattanzi, Silvio and Lee, Euiwoong and Li, Yi and Panageas, Ioannis and Paparas, Dimitris and Przybocki, Benjamin and Subercaseaux, Bernardo and Svensson, Ola and Taherijam, Shayan and Wu, Xuan and Yogev, Eylon and Zadimoghaddam, Morteza and Zhou, Samson and Matias, Yossi and Manyika, James and Mirrokni, Vahab}, title = {Accelerating Scientific Research with Gemini: Case Studies and Common Techniques}, journal = {CoRR}, volume = {abs/2602.03837}, year = {2026}, url = {https://doi.org/10.48550/arXiv.2602.03837}, doi = {10.48550/ARXIV.2602.03837}, eprinttype = {arXiv}, eprint = {2602.03837} }
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery

Benjamin Przybocki, John Mackey, Marijn J. H. Heule, and Bernardo Subercaseaux

CoRR 2026

arXiv HTML PDF

Ramsey-good graphs are graphs that contain neither a clique of size $s$ nor an independent set of size $t$. We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of any edge necessarily creates an $s$-clique or a $t$-independent set. We present a method combining SAT solving with bespoke LLM-generated code to discover infinite families of such graphs, answering a question of Grinstead and Roberts from 1982. In addition, we use LLMs to generate and formalize correctness proofs in Lean. This case study highlights the potential of integrating automated reasoning, large language models, and formal verification to accelerate mathematical discovery. We argue that such tool-driven workflows will play an increasingly central role in experimental mathematics.
@article{przybocki2026doublySaturatedRamsey, author = {Przybocki, Benjamin and Mackey, John and Heule, Marijn J. H. and Subercaseaux, Bernardo}, title = {Doubly Saturated Ramsey Graphs: {A} Case Study in Computer-Assisted Mathematical Discovery}, journal = {CoRR}, volume = {abs/2604.21187}, year = {2026}, url = {https://doi.org/10.48550/arXiv.2604.21187}, doi = {10.48550/ARXIV.2604.21187}, eprinttype = {arXiv}, eprint = {2604.21187} }
On the Complexity of Counting Orderings in Graphs

Marcelo Arenas, Marı́a Alejandra Schild, and Bernardo Subercaseaux

CoRR 2026

arXiv HTML PDF

We study the computational complexity of several counting problems on graphs. Each of these problems consists of counting orderings of the vertices or edges with adjacency constraints. We show $\#P$-completeness for all of them via a common new technique. Given a counting function $C$ of interest, we define a parameterized family of instances $G_q$, where the parameter $q$ controls the amplification of a simple gadget. After multiplying by an explicit factor $f(q)$, we show that the values of $f(q) \cdot C(G_q)$, for positive integers $q$, agree with a rational function in $q$ whose numerator and denominator can be interpolated in polynomial time. We then recover a $\#P$-hard function by evaluating this rational function symbolically at a limiting value $L \in \mathbb{Q} \cup \{\infty, -\infty\}$. With this methodology, we show $\#P$-completeness for the following counting problems: (a) successive vertex orderings of bipartite graphs, (b) st-numberings of graphs, (c) shellings of bipartite graphs, (d) linear extensions of N-free posets of height $3$, and (e) linear extensions of posets of height $2$. Result (d) settles a conjecture of Felsner and Manneville (2015). Although result (e) was first proved by Dittmer and Pak (2018), we include an alternative proof, using our technique, that does not rely on the result of Brightwell and Winkler (1991) about the hardness of counting linear extensions for general posets.
@article{arenas2026countingOrderings, author = {Arenas, Marcelo and Schild, Mar{\'{\i}}a Alejandra and Subercaseaux, Bernardo}, title = {On the Complexity of Counting Orderings in Graphs}, journal = {CoRR}, volume = {abs/2606.29157}, year = {2026}, url = {https://doi.org/10.48550/arXiv.2606.29157}, doi = {10.48550/ARXIV.2606.29157}, eprinttype = {arXiv}, eprint = {2606.29157} }
ExplAIner: A Declarative Query Language for Explaining Classification Models

Marcelo Arenas, Pablo Barceló, Diego Bustamante, Jose Caraball, Marı́a Alejandra Schild, and Bernardo Subercaseaux

CoRR 2026

arXiv HTML PDF

The XAI community has studied a wide range of queries and scores for explaining predictions of ML models. From a data management perspective, this proliferation of explanation notions calls for declarative query languages in which such notions can be specified, combined, and analyzed uniformly. In this paper, we develop such a framework for Boolean models. We first revisit FOIL, an interpretability query language for black-box models, and show that it has two fundamental limitations: it cannot express central optimality-based explanation queries, and its evaluation problem over decision trees is hard for every level of the polynomial hierarchy. We then introduce ExplAIner, a query language based on FOIL with an extended vocabulary and a layered structure. We show that ExplAIner can express a broad family of explanation notions, including abductive, contrastive, feature-based, and distance-based queries. We also prove that the evaluation problem for each query in ExplAIner belongs to the Boolean hierarchy over every class of Boolean models for which some basic predicates can be evaluated in polynomial time. In particular, that property holds for deterministic and decomposable Boolean circuits. Finally, we introduce Opt-FOIL, an optimization-oriented fragment of ExplAIner for computing explanations that are minimal with respect to strict partial orders, and prove that its evaluation problem is in $\mathrm{FP}^{\mathrm{NP}}$ under the same tractability assumptions. These complexity results have a direct algorithmic consequence: a fixed ExplAIner query can be evaluated with a fixed number of calls to a SAT solver, while a notion of explanation specified in Opt-FOIL can be computed with a polynomial number of such calls. This is particularly relevant in formal XAI, where SAT solvers have been successfully used to compute explanations for several classes of ML models.
@article{arenas2026explainer, author = {Arenas, Marcelo and Barcel{\'{o}}, Pablo and Bustamante, Diego and Caraball, Jose and Schild, Mar{\'{\i}}a Alejandra and Subercaseaux, Bernardo}, title = {ExplAIner: {A} Declarative Query Language for Explaining Classification Models}, journal = {CoRR}, volume = {abs/2607.06407}, year = {2026}, url = {https://doi.org/10.48550/arXiv.2607.06407}, doi = {10.48550/ARXIV.2607.06407}, eprinttype = {arXiv}, eprint = {2607.06407} }

2025

On Computing Probabilistic Explanations for Decision Trees

Marcelo Arenas, Pablo Barceló, Alexander Kozachinskiy, Miguel Romero, and Bernardo Subercaseaux

J. Artif. Intell. Res. 2025

HTML

Formal XAI (explainable AI) is a growing area that focuses on computing explanations with mathematical guarantees for the decisions made by machine-learning models. Inside formal XAI, one of the most studied cases is that of explaining the choices taken by decision trees. Recent work has focused on sufficient reasons: 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 every other instance $z$ compatible with $y$ satisfies $T(z) = T(x)$. It has been argued, however, that sufficient reasons constitute a restrictive notion of explanation. We study their probabilistic counterpart, in which the probability that $T(z) = T(x)$ must be at least some value $\delta \in (0,1]$. We settle the computational complexity of $\delta$-sufficient reasons over decision trees, showing that finding reasons minimal either in size or inclusion-wise is computationally intractable. This is in stark contrast with the deterministic case ($\delta = 1$), where inclusion-wise minimal sufficient reasons are easy to compute. We answer open problems raised by Izza et al. and extend hardness results of Wäldchen et al. to decision trees. Furthermore, we present sharp non-approximability results under a widely believed complexity hypothesis. On the positive side, we identify structural restrictions of decision trees that make the problem tractable.
@article{arenas2025probabilisticDecisionTreesJAIR, author = {Arenas, Marcelo and Barcel{\'{o}}, Pablo and Kozachinskiy, Alexander and Romero, Miguel and Subercaseaux, Bernardo}, title = {On Computing Probabilistic Explanations for Decision Trees}, journal = {J. Artif. Intell. Res.}, volume = {83}, year = {2025}, url = {https://doi.org/10.1613/jair.1.17494}, doi = {10.1613/JAIR.1.17494} }
Explaining k-Nearest Neighbors: Abductive and Counterfactual Explanations

Pablo Barceló, Alexander Kozachinskiy, Miguel Romero, Bernardo Subercaseaux, and José Verschae

Proc. ACM Manag. Data 2025
- Distinguished paperPODS 2025
arXiv HTML PDF

Despite the wide use of $k$-Nearest Neighbors as classification models, their explainability properties remain poorly understood from a theoretical perspective. While nearest neighbors classifiers offer interpretability from a ``data perspective'', in which the classification of an input vector $\bar{x}$ is explained by identifying the vectors $\bar{v}_1, \ldots, \bar{v}_k$ in the training set that determine the classification of $\bar{x}$, we argue that such explanations can be impractical in high-dimensional applications, where each vector has hundreds or thousands of features and it is not clear what their relative importance is. Hence, we focus on understanding nearest neighbor classifications through a ``feature perspective'', in which the goal is to identify how the values of the features in $\bar{x}$ affect its classification. Concretely, we study abductive explanations such as ``minimum sufficient reasons'', which correspond to sets of features in $\bar{x}$ that are enough to guarantee its classification, and counterfactual explanations based on the minimum distance feature changes one would have to perform in $\bar{x}$ to change its classification. We present a detailed landscape of positive and negative complexity results for counterfactual and abductive explanations, distinguishing between discrete and continuous feature spaces, and considering the impact of the choice of distance function involved. Finally, we show that despite some negative complexity results, Integer Quadratic Programming and SAT solving allow for computing explanations in practice.
@article{subercaseauxExplainingKNearest2025, author = {Barcel{\'{o}}, Pablo and Kozachinskiy, Alexander and Romero, Miguel and Subercaseaux, Bernardo and Verschae, Jos{\'{e}}}, title = {Explaining k-Nearest Neighbors: Abductive and Counterfactual Explanations}, journal = {Proc. {ACM} Manag. Data}, volume = {3}, number = {2}, pages = {97:1--97:26}, year = {2025}, url = {https://doi.org/10.1145/3725234}, doi = {10.1145/3725234} }
Probabilistic Explanations for Linear Models

Bernardo Subercaseaux, Marcelo Arenas, and Kuldeep S. Meel

In AAAI 2025

arXiv HTML PDF

Formal XAI is an emerging field that focuses on providing explanations with mathematical guarantees for the decisions made by machine learning models. A significant amount of work in this area is centered on the computation of "sufficient reasons". Given a model $M$ and an input instance $\vec{x}$, a sufficient reason for the decision $M(\vec{x})$ is a subset $S$ of the features of $\vec{x}$ such that for any instance $\vec{z}$ that has the same values as $\vec{x}$ for every feature in $S$, it holds that $M(\vec{x}) = M(\vec{z})$. Intuitively, this means that the features in $S$ are sufficient to fully justify the classification of $\vec{x}$ by $M$. For sufficient reasons to be useful in practice, they should be as small as possible, and a natural way to reduce the size of sufficient reasons is to consider a probabilistic relaxation; the probability of $M(\vec{x}) = M(\vec{z})$ must be at least some value $δ\in (0,1]$, for a random instance $\vec{z}$ that coincides with $\vec{x}$ on the features in $S$. Computing small $δ$-sufficient reasons ($δ$-SRs) is known to be a theoretically hard problem; even over decision trees--traditionally deemed simple and interpretable models--strong inapproximability results make the efficient computation of small $δ$-SRs unlikely. We propose the notion of $(δ, ε)$-SR, a simple relaxation of $δ$-SRs, and show that this kind of explanation can be computed efficiently over linear models.
@inproceedings{subercaseaux2025linearModelsAAAI, author = {Subercaseaux, Bernardo and Arenas, Marcelo and Meel, Kuldeep S.}, editor = {Walsh, Toby and Shah, Julie and Kolter, Zico}, title = {Probabilistic Explanations for Linear Models}, booktitle = {Thirty-Ninth {AAAI} Conference on Artificial Intelligence, Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence, Fifteenth Symposium on Educational Advances in Artificial Intelligence, {AAAI} 2025, Philadelphia, PA, USA, February 25 - March 4, 2025}, pages = {20655--20662}, publisher = {{AAAI} Press}, year = {2025}, url = {https://doi.org/10.1609/aaai.v39i19.34276}, doi = {10.1609/AAAI.V39I19.34276} }
Unfolding Boxes with Local Constraints

Long Qian, Eric Wang, Bernardo Subercaseaux, and Marijn J. H. Heule

In CADE 2025

arXiv HTML PDF

We consider the problem of finding and enumerating polyominos that can be folded into multiple non-isomorphic boxes. While several computational approaches have been proposed, including SAT, randomized algorithms, and decision diagrams, none has been able to perform at scale. We argue that existing SAT encodings are hindered by the presence of global constraints (e.g., graph connectivity or acyclicity), which are generally hard to encode effectively and hard for solvers to reason about. In this work, we propose a new SAT-based approach that replaces these global constraints with simple local constraints that have substantially better propagation properties. Our approach dramatically improves the scalability of both computing and enumerating common box unfoldings: (i) while previous approaches could only find common unfoldings of two boxes up to area 88, ours easily scales beyond 150, and (ii) while previous approaches were only able to enumerate common unfoldings up to area 30, ours scales up to 60. This allows us to rule out 46, 54, and 58 as the smallest areas allowing a common unfolding of three boxes, thereby refuting a conjecture of Xu et al. (2017).
@inproceedings{subercaseauxUnfoldingBoxesLocalConstraints2025, author = {Qian, Long and Wang, Eric and Subercaseaux, Bernardo and Heule, Marijn J. H.}, editor = {Barrett, Clark W. and Waldmann, Uwe}, title = {Unfolding Boxes with Local Constraints}, booktitle = {Automated Deduction - {CADE} 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {15943}, pages = {736--754}, publisher = {Springer}, year = {2025}, url = {https://doi.org/10.1007/978-3-031-99984-0\_38}, doi = {10.1007/978-3-031-99984-0\_38} }
Latency Guarantees for Caching with Delayed Hits

Keerthana Gurushankar, Noah G. Singer, and Bernardo Subercaseaux

In INFOCOM 2025

arXiv HTML PDF

In the classical caching problem, when a requested page is not present in the cache (i.e., a "miss"), it is assumed to travel from the backing store into the cache "before" the next request arrives. However, in many real-life applications, such as content delivery networks, this assumption is unrealistic. The "delayed-hits" model for caching, introduced by Atre, Sherry, Wang, and Berger, accounts for the latency between a missed cache request and the corresponding arrival from the backing store. This theoretical model has two parameters: the "delay" $Z$, representing the ratio between the retrieval delay and the inter-request delay in an application, and the "cache size" $k$, as in classical caching. Classical caching corresponds to $Z=1$, whereas larger values of $Z$ model applications where retrieving missed requests is expensive. Despite the practical relevance of the delayed-hits model, its theoretical underpinnings are still poorly understood. We present the first tight theoretical guarantee for optimizing delayed-hits caching: The "Least Recently Used" algorithm, a natural, deterministic, online algorithm widely used in practice, is $O(Zk)$-competitive, meaning it incurs at most $O(Zk)$ times more latency than the (offline) optimal schedule. Our result extends to any so-called "marking" algorithm.
@inproceedings{gurushankar2025delayedHitsINFOCOM, author = {Gurushankar, Keerthana and Singer, Noah G. and Subercaseaux, Bernardo}, title = {Latency Guarantees for Caching with Delayed Hits}, booktitle = {{IEEE} {INFOCOM} 2025 - {IEEE} Conference on Computer Communications, London, United Kingdom, May 19-22, 2025}, pages = {1--10}, publisher = {{IEEE}}, year = {2025}, url = {https://doi.org/10.1109/INFOCOM55648.2025.11044511}, doi = {10.1109/INFOCOM55648.2025.11044511} }
Automated Symmetric Constructions in Discrete Geometry

Bernardo Subercaseaux, Ethan Mackey, Long Qian, and Marijn Heule

In CICM 2025
- Best paperCICM 2025
arXiv HTML PDF

We present a computational methodology for obtaining rotationally symmetric sets of points satisfying discrete geometric constraints, and demonstrate its applicability by discovering new solutions to some well-known problems in combinatorial geometry. Our approach takes the usage of SAT solvers in discrete geometry further by directly embedding rotational symmetry into the combinatorial encoding of geometric configurations. Then, to realize concrete point sets corresponding to abstract designs provided by a SAT solver, we introduce a novel local-search realizability solver, which shows excellent practical performance despite the intrinsic $\exists \mathbb{R}$-completeness of the problem. Leveraging this combined approach, we provide symmetric extremal solutions to the Erdős-Szekeres problem, as well as a minimal odd-sized solution with 21 points for the everywhere-unbalanced-points problem, improving on the previously known 23-point configuration. The imposed symmetries yield more aesthetically appealing solutions, enhancing human interpretability, and simultaneously offer computational benefits by significantly reducing the number of variables required to encode discrete geometric problems.
@inproceedings{subercaseauxAutomatedSymmetricConstructions2026, author = {Subercaseaux, Bernardo and Mackey, Ethan and Qian, Long and Heule, Marijn}, editor = {de Paiva, Valeria and Koepke, Peter}, title = {Automated Symmetric Constructions in Discrete Geometry}, booktitle = {Intelligent Computer Mathematics - 18th International Conference, {CICM} 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {16136}, pages = {29--47}, publisher = {Springer}, year = {2025}, url = {https://doi.org/10.1007/978-3-032-07021-0\_3}, doi = {10.1007/978-3-032-07021-0\_3} }
Asymptotically Smaller Encodings for Graph Problems and Scheduling

Bernardo Subercaseaux

CoRR 2025

arXiv HTML PDF

We show how several graph problems (e.g., vertex-cover, independent-set, $k$-coloring) can be encoded into CNF using only $O(|V|^2 / \lg |V|)$ many clauses, as opposed to the $Ω(|V|^2)$ constraints used by standard encodings. This somewhat surprising result is a simple consequence of a result of Erdős, Chung, and Spencer (1983) about biclique coverings of graphs, and opens theoretical avenues to understand the success of "Bounded Variable Addition'' (Manthey, Heule, and Biere, 2012) as a preprocessing tool. Finally, we show a novel encoding for independent sets in some dense interval graphs using only $O(|V| \lg |V|)$ clauses (the direct encoding uses $Ω(|V|^2)$), which we have successfully applied to a string-compression encoding posed by Bannai et al. (2022). As a direct byproduct, we obtain a reduction in the encoding size of a scheduling problem posed by Mayank and Modal (2020) from $O(NMT^2)$ to $O(NMT + M T^2 \lg T)$, where $N$ is the number of tasks, $T$ the total timespan, and $M$ the number of machines.
@article{subercaseaux2025smallerEncodings, author = {Subercaseaux, Bernardo}, title = {Asymptotically Smaller Encodings for Graph Problems and Scheduling}, journal = {CoRR}, volume = {abs/2506.14042}, year = {2025}, url = {https://doi.org/10.48550/arXiv.2506.14042}, doi = {10.48550/ARXIV.2506.14042}, eprinttype = {arXiv}, eprint = {2506.14042} }
From the Finite to the Infinite: Sharper Asymptotic Bounds on Norin’s Conjecture via SAT

Markus Kirchweger, Tomás Peitl, Bernardo Subercaseaux, and Stefan Szeider

CoRR 2025

arXiv HTML PDF

Norin (2008) conjectured that any $2$-edge-coloring of the hypercube $Q_n$ in which antipodal edges receive different colors must contain a monochromatic path between some pair of antipodal vertices. While the general conjecture remains elusive, progress thus far has been made on two fronts: finite cases and asymptotic relaxations. The best finite results are due to Frankston and Scheinerman (2024) who verified the conjecture for $n \leq 7$ using SAT solvers, and the best asymptotic result is due to Dvořák (2020), who showed that every $2$-edge-coloring of $Q_n$ admits an antipodal path of length $n$ with at most $0.375n + o(n)$ color changes. We improve on both fronts via SAT. First, we extend the verification to $n = 8$ by introducing a more compact and efficient SAT encoding, enhanced with symmetry breaking and cube-and-conquer parallelism. The versatility of this new encoding allows us to recast parts of Dvořák's asymptotic approach as a SAT problem, thereby improving the asymptotic upper bound to $0.3125n + O(1)$ color changes. Our work demonstrates how SAT-based methods can yield not only finite-case confirmations but also asymptotic progress on combinatorial conjectures.
@article{kirchweger2025norinConjecture, author = {Kirchweger, Markus and Peitl, Tom{\'{a}}s and Subercaseaux, Bernardo and Szeider, Stefan}, title = {From the Finite to the Infinite: Sharper Asymptotic Bounds on Norin's Conjecture via {SAT}}, journal = {CoRR}, volume = {abs/2511.08386}, year = {2025}, url = {https://doi.org/10.48550/arXiv.2511.08386}, doi = {10.48550/ARXIV.2511.08386}, eprinttype = {arXiv}, eprint = {2511.08386} }

2024

A Mathematical Analysis of PlaceIt: A Game of Perfect Online Sorting

Pablo Ruiz Cuevas, Casey Chock, and Bernardo Subercaseaux

In CG 2024

HTML

In the single-player game of PlaceIt, a player must sort a random sequence of numbers in an online fashion. The game begins by sampling a sequence $S = (s_1, \ldots, s_{20})$ of numbers uniformly at random from $\{1, \ldots, 999\}$ without replacement. The elements of $S$ are presented one by one to the player. Upon seeing an element $s_i$, a player must try to guess its rank, that is, the number $n$ such that $s_i$ is the $n^{\text{th}}$ smallest number in $S$. The player must guess the rank of all 20 numbers correctly to win the game. Additionally, the game requires each guess to be consistent with previous guesses. If at any point the player cannot make a consistent guess, they lose immediately, and once a rank has been assigned it cannot be changed. We prove that the optimal strategy wins with probability close to 0.0001335, and extend our analysis to a continuous variant of the game.
@inproceedings{cuevas2024placeIt, author = {Cuevas, Pablo Ruiz and Chock, Casey and Subercaseaux, Bernardo}, editor = {Hartisch, Michael and Hsueh, Chu{-}Hsuan and Schaeffer, Jonathan}, title = {A Mathematical Analysis of PlaceIt: {A} Game of Perfect Online Sorting}, booktitle = {Computers and Games - 12th International Conference, {CG} 2024, Virtual Event, November 25-29, 2024, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {15550}, pages = {185--196}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-86585-5\_15}, doi = {10.1007/978-3-031-86585-5\_15} }
PackIt!: Gamified Rectangle Packing

Thomas Garrison, Marijn J. H. Heule, and Bernardo Subercaseaux

In FUN 2024

arXiv HTML PDF

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 \emph{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.
@inproceedings{garrison2024packit, author = {Garrison, Thomas and Heule, Marijn J. H. and Subercaseaux, Bernardo}, editor = {Broder, Andrei Z. and Tamir, Tami}, title = {PackIt!: Gamified Rectangle Packing}, booktitle = {12th International Conference on Fun with Algorithms, {FUN} 2024, Island of La Maddalena, Sardinia, Italy, June 4-8, 2024}, series = {LIPIcs}, volume = {291}, pages = {14:1--14:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2024}, url = {https://doi.org/10.4230/LIPIcs.FUN.2024.14}, doi = {10.4230/LIPICS.FUN.2024.14} }
Formal Verification of the Empty Hexagon Number

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, and Marijn J. H. Heule

In ITP 2024

arXiv HTML PDF

A recent breakthrough in computer-assisted mathematics showed that every set of $30$ points in the plane in general position (i.e., without three on a common line) contains an empty convex hexagon, thus closing a line of research dating back to the 1930s. Through a combination of geometric insights and automated reasoning techniques, Heule and Scheucher constructed a CNF formula $φ_n$, with $O(n^4)$ clauses, whose unsatisfiability implies that no set of $n$ points in general position can avoid an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17300 CPU hours of parallel computation, thus implying that the empty hexagon number h(6) is equal to 30. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers discrete computational geometry ideas and SAT encoding techniques that have been successfully applied to similar Erdős-Szekeres-type problems. In particular, our framework provides tools to connect standard mathematical objects to propositional assignments, which represents a key step towards the formal verification of other SAT-based mathematical results. Overall, we hope that this work sets a new standard for verification when extensive computation is used for discrete geometry problems, and that it increases the trust the mathematical community has in computer-assisted proofs in this area.
@inproceedings{subercaseauxFormalVerificationEmpty2024, author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden R. and Carneiro, Mario and Heule, Marijn J. H.}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, title = {Formal Verification of the Empty Hexagon Number}, booktitle = {15th International Conference on Interactive Theorem Proving, {ITP} 2024, Tbilisi, Georgia, September 9-14, 2024}, series = {LIPIcs}, volume = {309}, pages = {35:1--35:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2024}, url = {https://doi.org/10.4230/LIPIcs.ITP.2024.35}, doi = {10.4230/LIPICS.ITP.2024.35} }
A Uniform Language to Explain Decision Trees

Marcelo Arenas, Pablo Barceló, Diego Bustamante, Jose Caraball, and Bernardo Subercaseaux

In KR 2024

arXiv HTML PDF

The formal XAI community has studied a plethora of interpretability queries aiming to understand the classifications made by decision trees. However, a more uniform understanding of what questions we can hope to answer about these models, traditionally deemed to be easily interpretable, has remained elusive. In an initial attempt to understand uniform languages for interpretability, Arenas et al. (2021) proposed FOIL, a logic for explaining black-box ML models, and showed that it can express a variety of interpretability queries. However, we show that FOIL is limited in two important senses: (i) it is not expressive enough to capture some crucial queries, and (ii) its model agnostic nature results in a high computational complexity for decision trees. In this paper, we carefully craft two fragments of first-order logic that allow for efficiently interpreting decision trees: Q-DT-FOIL and its optimization variant OPT-DT-FOIL. We show that our proposed logics can express not only a variety of interpretability queries considered by previous literature, but also elegantly allows users to specify different objectives the sought explanations should optimize for. Using finite model-theoretic techniques, we show that the different ingredients of Q-DT-FOIL are necessary for its expressiveness, and yet that queries in Q-DT-FOIL can be evaluated with a polynomial number of queries to a SAT solver, as well as their optimization versions in OPT-DT-FOIL. Besides our theoretical results, we provide a SAT-based implementation of the evaluation for OPT-DT-FOIL that is performant on industry-size decision trees.
@inproceedings{arenas2024uniformLanguage, author = {Arenas, Marcelo and Barcel{\'{o}}, Pablo and Bustamante, Diego and Caraball, Jose and Subercaseaux, Bernardo}, editor = {Marquis, Pierre and Ortiz, Magdalena and Pagnucco, Maurice}, title = {A Uniform Language to Explain Decision Trees}, booktitle = {Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, {KR} 2024, Hanoi, Vietnam. November 2-8, 2024}, year = {2024}, url = {https://doi.org/10.24963/kr.2024/6}, doi = {10.24963/KR.2024/6} }
Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition

Bernardo Subercaseaux

In LPAR 2024

HTML PDF

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.
@inproceedings{BCA2024LPAR, author = {Subercaseaux, Bernardo}, editor = {Bj{\o}rner, Nikolaj S. and Heule, Marijn and Voronkov, Andrei}, title = {Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition}, booktitle = {{LPAR} 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024}, series = {EPiC Series in Computing}, volume = {100}, pages = {408--425}, publisher = {EasyChair}, year = {2024}, url = {https://doi.org/10.29007/p5mc}, doi = {10.29007/P5MC} }
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane

Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, and Ruben Martins

In CICM 2024
- Best-paper runner-upCICM 2024
arXiv HTML PDF

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 $μ_{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: $μ_{5}(n) \leq \binom{\lfloor n/2 \rfloor}{5} + \binom{\lceil n/2 \rceil}{5}$, and we conjecture it is optimal. In the second stage, we turn our focus to verifying this conjecture. Using MaxSAT, we confirm that $μ_5(n)$ matches the conjectured values for $n \leq 16$, thereby improving both the existing lower and upper bounds for $n \in [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.
@inproceedings{subercaseauxAutomatedMathematicalDiscovery2024, author = {Subercaseaux, Bernardo and Mackey, John and Heule, Marijn J. H. and Martins, Ruben}, editor = {Kohlhase, Andrea and Kov{\'{a}}cs, Laura}, title = {Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane}, booktitle = {Intelligent Computer Mathematics - 17th International Conference, {CICM} 2024, Montr{\'{e}}al, QC, Canada, August 5-9, 2024, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {14960}, pages = {21--41}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-66997-2\_2}, doi = {10.1007/978-3-031-66997-2\_2} }
Assortment Optimization For Conference Goodies With Indifferent Attendees

Fernanda Gutiérrez, and Bernardo Subercaseaux

CoRR 2024

arXiv HTML PDF

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.
@article{gutierrez2024assortment, author = {Guti{\'{e}}rrez, Fernanda and Subercaseaux, Bernardo}, title = {Assortment Optimization For Conference Goodies With Indifferent Attendees}, journal = {CoRR}, volume = {abs/2403.03330}, year = {2024}, url = {https://doi.org/10.48550/arXiv.2403.03330}, doi = {10.48550/ARXIV.2403.03330}, eprinttype = {arXiv}, eprint = {2403.03330} }
Pentagon Minimization without Computation

John Mackey, and Bernardo Subercaseaux

CoRR 2024

arXiv HTML PDF

Erdős and Guy initiated a line of research studying $μ_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 \infty} μ_k(n)/\binom{n}{k}$ 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 using semi-definite programming. In this article we prove a more modest lower bound of $\frac{5\sqrt{5}-11}{4} \approx 0.04508$ without any computation; we exploit``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.
@article{mackey2024pentagonminimizationcomputation, author = {Mackey, John and Subercaseaux, Bernardo}, title = {Pentagon Minimization without Computation}, journal = {CoRR}, volume = {abs/2409.17098}, year = {2024}, url = {https://doi.org/10.48550/arXiv.2409.17098}, doi = {10.48550/ARXIV.2409.17098}, eprinttype = {arXiv}, eprint = {2409.17098} }
A proof long enough to stump Leonhard Euler

Bernardo Subercaseaux, and Marijn J. H. Heule

Nieuw Archief voor Wiskunde (NAW) 2024

PDF

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.
@article{subercaseauxHeuleNAW, author = {Subercaseaux, Bernardo and Heule, Marijn J. H.}, title = {A proof long enough to stump Leonhard Euler}, year = {2024}, journal = {Nieuw Archief voor Wiskunde (NAW)} }

2023

Toward Optimal Radio Colorings of Hypercubes via SAT-solving

Bernardo Subercaseaux, and Marijn Heule

In LPAR 2023
- Best paperLPAR 2023
HTML PDF

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.
@inproceedings{sh2023LPAR, author = {Subercaseaux, Bernardo and Heule, Marijn}, editor = {Piskac, Ruzica and Voronkov, Andrei}, title = {Toward Optimal Radio Colorings of Hypercubes via SAT-solving}, booktitle = {{LPAR} 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023}, series = {EPiC Series in Computing}, volume = {94}, pages = {386--404}, publisher = {EasyChair}, year = {2023}, url = {https://doi.org/10.29007/qrmp}, doi = {10.29007/QRMP} }
The Packing Chromatic Number of the Infinite Square Grid is 15

Bernardo Subercaseaux, and Marijn J. H. Heule

In TACAS 2023
- Best-paper nomineeTACAS 2023
arXiv HTML PDF

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 \in \{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 and surprisingly effective propositional encoding. Additionally, we developed a new 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.
@inproceedings{sh2023, author = {Subercaseaux, Bernardo and Heule, Marijn J. H.}, editor = {Sankaranarayanan, Sriram and Sharygina, Natasha}, title = {The Packing Chromatic Number of the Infinite Square Grid is 15}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, {TACAS} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2023, Paris, France, April 22-27, 2023, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {13993}, pages = {389--406}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-30823-9\_20}, doi = {10.1007/978-3-031-30823-9\_20} }

2022

On the expressiveness of Lara: A proposal for unifying linear and relational algebra

Pablo Barceló, Nelson Higuera, Jorge Pérez, and Bernardo Subercaseaux

Theor. Comput. Sci. 2022

arXiv HTML PDF

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.
@article{barcelo2022laraTCS, author = {Barcel{\'{o}}, Pablo and Higuera, Nelson and P{\'{e}}rez, Jorge and Subercaseaux, Bernardo}, title = {On the expressiveness of Lara: {A} proposal for unifying linear and relational algebra}, journal = {Theor. Comput. Sci.}, volume = {935}, pages = {105--127}, year = {2022}, url = {https://doi.org/10.1016/j.tcs.2022.09.003}, doi = {10.1016/J.TCS.2022.09.003} }
Wordle Is NP-Hard

Daniel Lokshtanov, and Bernardo Subercaseaux

In FUN 2022

arXiv HTML PDF

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 $\ell$ 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 $\ell$ if the player can guarantee to discover the secret word within $\ell$ 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.
@inproceedings{ls2022, author = {Lokshtanov, Daniel and Subercaseaux, Bernardo}, editor = {Fraigniaud, Pierre and Uno, Yushi}, title = {Wordle Is NP-Hard}, booktitle = {11th International Conference on Fun with Algorithms, {FUN} 2022, Island of Favignana, Sicily, Italy, May 30 - June 3, 2022}, series = {LIPIcs}, volume = {226}, pages = {19:1--19:8}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2022}, url = {https://doi.org/10.4230/LIPIcs.FUN.2022.19}, doi = {10.4230/LIPICS.FUN.2022.19} }
Augmenting Online Algorithms with ε-Accurate Predictions

Anupam Gupta, Debmalya Panigrahi, Bernardo Subercaseaux, and Kevin Sun

In NeurIPS 2022

HTML PDF

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/ε))-competitive algorithm for caching, and a simple O(1/ε)-competitive algorithm for a large family of covering problems, including set cover and facility location, with ε-accurate predictions.
@inproceedings{gpss2022, author = {Gupta, Anupam and Panigrahi, Debmalya and Subercaseaux, Bernardo and Sun, Kevin}, editor = {Koyejo, Sanmi and Mohamed, S. and Agarwal, A. and Belgrave, Danielle and Cho, K. and Oh, A.}, title = {Augmenting Online Algorithms with ε-Accurate Predictions}, booktitle = {Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022}, year = {2022}, url = {https://papers.nips.cc/paper\_files/paper/2022/hash/0ea048312aa812b2711fe765a9e9ef05-Abstract-Conference.html} }
On Computing Probabilistic Explanations for Decision Trees

Marcelo Arenas, Pablo Barceló, Miguel A. Romero Orth, and Bernardo Subercaseaux

In NeurIPS 2022

arXiv HTML PDF

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, and thus 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 $δ\in (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. 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.
@inproceedings{abrs2022, author = {Arenas, Marcelo and Barcel{\'{o}}, Pablo and Orth, Miguel A. Romero and Subercaseaux, Bernardo}, editor = {Koyejo, Sanmi and Mohamed, S. and Agarwal, A. and Belgrave, Danielle and Cho, K. and Oh, A.}, title = {On Computing Probabilistic Explanations for Decision Trees}, booktitle = {Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022}, year = {2022}, url = {https://papers.nips.cc/paper\_files/paper/2022/hash/b8963f6a0a72e686dfa98ac3e7260f73-Abstract-Conference.html} }
The Packing Chromatic Number of the Infinite Square Grid Is at Least 14

Bernardo Subercaseaux, and Marijn J. H. Heule

In SAT 2022

HTML PDF

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.
@inproceedings{sh2022, author = {Subercaseaux, Bernardo and Heule, Marijn J. H.}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, title = {The Packing Chromatic Number of the Infinite Square Grid Is at Least 14}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2022, Haifa, Israel, August 2-5, 2022}, series = {LIPIcs}, volume = {236}, pages = {21:1--21:16}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2022}, url = {https://doi.org/10.4230/LIPIcs.SAT.2022.21}, doi = {10.4230/LIPICS.SAT.2022.21} }

2021

The Computational Complexity of Evil Hangman

Jérémy Barbay, and Bernardo Subercaseaux

In FUN 2021

arXiv HTML PDF

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.
@inproceedings{bs2021, author = {Barbay, J{\'{e}}r{\'{e}}my and Subercaseaux, Bernardo}, editor = {Farach{-}Colton, Martin and Prencipe, Giuseppe and Uehara, Ryuhei}, title = {The Computational Complexity of Evil Hangman}, booktitle = {10th International Conference on Fun with Algorithms, {FUN} 2021, Favignana Island, Sicily, Italy, May 30 - June 1, 2021}, series = {LIPIcs}, volume = {157}, pages = {23:1--23:12}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/LIPIcs.FUN.2021.23}, doi = {10.4230/LIPICS.FUN.2021.23} }
Foundations of Symbolic Languages for Model Interpretability

Marcelo Arenas, Daniel Báez, Pablo Barceló, Jorge Pérez, and Bernardo Subercaseaux

In NeurIPS 2021
- SpotlightNeurIPS 2021
arXiv HTML PDF

Several queries and scores have recently been proposed to explain individual predictions over ML models. 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 two classes of ML models often deemed to be easily interpretable: decision trees and OBDDs. Since the number of possible inputs for an ML model is exponential in its dimension, the 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.
@inproceedings{abbps2021, author = {Arenas, Marcelo and B{\'{a}}ez, Daniel and Barcel{\'{o}}, Pablo and P{\'{e}}rez, Jorge and Subercaseaux, Bernardo}, editor = {Ranzato, Marc'Aurelio and Beygelzimer, Alina and Dauphin, Yann N. and Liang, Percy and Vaughan, Jennifer Wortman}, title = {Foundations of Symbolic Languages for Model Interpretability}, booktitle = {Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual}, pages = {11690--11701}, year = {2021}, url = {https://proceedings.neurips.cc/paper/2021/hash/60cb558c40e4f18479664069d9642d5a-Abstract.html} }

2020

On the Expressiveness of LARA: A Unified Language for Linear and Relational Algebra

Pablo Barceló, Nelson Higuera, Jorge Pérez, and Bernardo Subercaseaux

In ICDT 2020

arXiv HTML PDF

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.
@inproceedings{bhps2020, author = {Barcel{\'{o}}, Pablo and Higuera, Nelson and P{\'{e}}rez, Jorge and Subercaseaux, Bernardo}, editor = {Lutz, Carsten and Jung, Jean Christoph}, title = {On the Expressiveness of {LARA:} {A} Unified Language for Linear and Relational Algebra}, booktitle = {23rd International Conference on Database Theory, {ICDT} 2020, Copenhagen, Denmark, March 30 - April 2, 2020}, series = {LIPIcs}, volume = {155}, pages = {6:1--6:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2020}, url = {https://doi.org/10.4230/LIPIcs.ICDT.2020.6}, doi = {10.4230/LIPICS.ICDT.2020.6} }
Model Interpretability through the lens of Computational Complexity

Pablo Barceló, Mikaël Monet, Jorge Pérez, and Bernardo Subercaseaux

In NeurIPS 2020

arXiv HTML PDF

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 $\mathcal{C}_1$ of models is more interpretable than another class $\mathcal{C}_2$, if the computational complexity of answering post-hoc queries for models in $\mathcal{C}_2$ is higher than for those in $\mathcal{C}_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$\neq$NP), 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.
@inproceedings{bpms2020, author = {Barcel{\'{o}}, Pablo and Monet, Mika{\"{e}}l and P{\'{e}}rez, Jorge and Subercaseaux, Bernardo}, editor = {Larochelle, Hugo and Ranzato, Marc'Aurelio and Hadsell, Raia and Balcan, Maria{-}Florina and Lin, Hsuan{-}Tien}, title = {Model Interpretability through the lens of Computational Complexity}, booktitle = {Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual}, year = {2020}, url = {https://proceedings.neurips.cc/paper/2020/hash/b1adda14824f50ef24ff1c05bb66faf3-Abstract.html} }
Foundations of Languages for Interpretability and Bias Detection

Pablo Barceló, Jorge Pérez, and Bernardo Subercaseaux

AFCI workshop at NeurIPS 2020. Algorithmic Fairness through the Lens of Causality and Interpretability 2020
- SpotlightAFCI @ NeurIPS 2020
PDF

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.
@article{bps2020, author = {Barcel{\'{o}}, Pablo and P{\'{e}}rez, Jorge and Subercaseaux, Bernardo}, journal = {AFCI workshop at NeurIPS 2020. Algorithmic Fairness through the Lens of Causality and Interpretability}, title = {Foundations of Languages for Interpretability and Bias Detection}, year = {2020} }

2019

Expressiveness of Matrix and Tensor Query Languages in terms of ML Operators

Pablo Barceló, Nelson Higuera, Jorge Pérez, and Bernardo Subercaseaux

In DEEM@SIGMOD 2019

HTML PDF

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.
@inproceedings{bhps2019, author = {Barcel{\'{o}}, Pablo and Higuera, Nelson and P{\'{e}}rez, Jorge and Subercaseaux, Bernardo}, editor = {Schelter, Sebastian and Polyzotis, Neoklis and Seufert, Stephan and Vartak, Manasi}, title = {Expressiveness of Matrix and Tensor Query Languages in terms of {ML} Operators}, booktitle = {Proceedings of the 3rd International Workshop on Data Management for End-to-End Machine Learning, DEEM@SIGMOD 2019, Amsterdam, The Netherlands, June 30, 2019}, pages = {9:1--9:5}, publisher = {{ACM}}, year = {2019}, url = {https://doi.org/10.1145/3329486.3329498}, doi = {10.1145/3329486.3329498} }

2018

2017

2016

Wavelet Trees for Competitive Programming

Robinson Castro, Nico Lehmann, Jorge Pérez, and Bernardo Subercaseaux

Olympiads in Informatics Jul 2016

HTML PDF

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.
@article{clps2016, author = {Castro, Robinson and Lehmann, Nico and P{\'e}rez, Jorge and Subercaseaux, Bernardo}, doi = {10.15388/ioi.2016.02}, journal = {Olympiads in Informatics}, month = jul, number = {1}, pages = {19--37}, publisher = {Vilnius University Press}, select = {true}, title = {Wavelet Trees for Competitive Programming}, url = {https://doi.org/10.15388/ioi.2016.02}, volume = {10}, year = {2016} }

Some datapoints

Citations by year

Papers

2026

Computing NP-hard Repetitiveness Measures via MAX-SAT

A Demigod’s Number for the Rubik’s Cube

Solving Small Rubik’s Cubes as Slowly as Possible

Price of Locality in Permutation Mastermind: Are TikTok Influencers Chaotic Enough?

Near-Optimal Encodings of Cardinality Constraints

Automated Reencoding Meets Graph Theory

Optimal and Efficient Partite Decompositions of Hypergraphs

Accelerating Scientific Research with Gemini: Case Studies and Common Techniques

Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery

On the Complexity of Counting Orderings in Graphs

ExplAIner: A Declarative Query Language for Explaining Classification Models

2025

On Computing Probabilistic Explanations for Decision Trees

Explaining k-Nearest Neighbors: Abductive and Counterfactual Explanations

Probabilistic Explanations for Linear Models

Unfolding Boxes with Local Constraints

Latency Guarantees for Caching with Delayed Hits

Automated Symmetric Constructions in Discrete Geometry

Asymptotically Smaller Encodings for Graph Problems and Scheduling

From the Finite to the Infinite: Sharper Asymptotic Bounds on Norin’s Conjecture via SAT

2024

A Mathematical Analysis of PlaceIt: A Game of Perfect Online Sorting

PackIt!: Gamified Rectangle Packing

Formal Verification of the Empty Hexagon Number

A Uniform Language to Explain Decision Trees

Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition

Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane

Assortment Optimization For Conference Goodies With Indifferent Attendees

Pentagon Minimization without Computation

A proof long enough to stump Leonhard Euler

2023

Toward Optimal Radio Colorings of Hypercubes via SAT-solving

The Packing Chromatic Number of the Infinite Square Grid is 15

2022

On the expressiveness of Lara: A proposal for unifying linear and relational algebra

Wordle Is NP-Hard

Augmenting Online Algorithms with ε-Accurate Predictions

On Computing Probabilistic Explanations for Decision Trees

The Packing Chromatic Number of the Infinite Square Grid Is at Least 14

2021

The Computational Complexity of Evil Hangman

Foundations of Symbolic Languages for Model Interpretability

2020

On the Expressiveness of LARA: A Unified Language for Linear and Relational Algebra

Model Interpretability through the lens of Computational Complexity

Foundations of Languages for Interpretability and Bias Detection

2019

Expressiveness of Matrix and Tensor Query Languages in terms of ML Operators

2018

2017

2016

Wavelet Trees for Competitive Programming