22 Search Results for "Subercaseaux, Bernardo"

Document
DOI: 10.4230/LIPIcs.SAT.2026.23
Near-Optimal Encodings of Cardinality Constraints

Authors: Andrew Krapivin, Benjamin Przybocki, and Bernardo Subercaseaux

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
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 AtMostOne(x_1,…,x_n) constraint using 2n + 2 √{2n} + O(∛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 + √{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 AtMost_k(x_1,…,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(∛{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 ≤ 5 and 7n - o(n) for k ≥ 6.
Cite as

Andrew Krapivin, Benjamin Przybocki, and Bernardo Subercaseaux. Near-Optimal Encodings of Cardinality Constraints. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{krapivin_et_al:LIPIcs.SAT.2026.23,
  author =	{Krapivin, Andrew and Przybocki, Benjamin and Subercaseaux, Bernardo},
  title =	{{Near-Optimal Encodings of Cardinality Constraints}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.23},
  URN =		{urn:nbn:de:0030-drops-263294},
  doi =		{10.4230/LIPIcs.SAT.2026.23},
  annote =	{Keywords: CNF encodings, cardinality constraints, circuit complexity}
}
Document
DOI: 10.4230/LIPIcs.SAT.2026.29
Automated Reencoding Meets Graph Theory

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

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
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 (lg(3)/4 + o(1)) n²/(lg n) clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from lg(3)/4 ≈ 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.
Cite as

Benjamin Przybocki, Bernardo Subercaseaux, and Marijn J. H. Heule. Automated Reencoding Meets Graph Theory. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{przybocki_et_al:LIPIcs.SAT.2026.29,
  author =	{Przybocki, Benjamin and Subercaseaux, Bernardo and Heule, Marijn J. H.},
  title =	{{Automated Reencoding Meets Graph Theory}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.29},
  URN =		{urn:nbn:de:0030-drops-263358},
  doi =		{10.4230/LIPIcs.SAT.2026.29},
  annote =	{Keywords: SAT solving, CNF encodings, BVA, Rectifier networks}
}
Document
DOI: 10.4230/LIPIcs.FUN.2026.2
Man, These New York Times Games Are Hard! A Computational Perspective

Authors: Alessandro Giovanni Alberti, Flavio Chierichetti, Mirko Giacchini, Daniele Muscillo, Alessandro Panconesi, and Erasmo Tani

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract
The New York Times (NYT) games have found widespread popularity in recent years and reportedly account for an increasing fraction of the newspaper’s readership. In this paper, we bring the computational lens to the study of New York Times games and consider four of them not previously studied: Letter Boxed, Pips, Strands and Tiles. We show that these games can be just as hard as they are fun. In particular, we characterize the hardness of several variants of computational problems related to these popular puzzle games. For Letter Boxed, we show that deciding whether an instance is solvable is in general NP-Complete, while in some parameter settings it can be done in polynomial time. Similarly, for Pips we prove that deciding whether a puzzle has a solution is NP-Complete even in some restricted classes of instances. We then show that one natural computational problem arising from Strands is NP-Complete in most parameter settings. Finally, we demonstrate that deciding whether a Tiles puzzle is solvable with a single, uninterrupted combo requires polynomial time.
Cite as

Alessandro Giovanni Alberti, Flavio Chierichetti, Mirko Giacchini, Daniele Muscillo, Alessandro Panconesi, and Erasmo Tani. Man, These New York Times Games Are Hard! A Computational Perspective. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{alberti_et_al:LIPIcs.FUN.2026.2,
  author =	{Alberti, Alessandro Giovanni and Chierichetti, Flavio and Giacchini, Mirko and Muscillo, Daniele and Panconesi, Alessandro and Tani, Erasmo},
  title =	{{Man, These New York Times Games Are Hard! A Computational Perspective}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{2:1--2:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.2},
  URN =		{urn:nbn:de:0030-drops-257219},
  doi =		{10.4230/LIPIcs.FUN.2026.2},
  annote =	{Keywords: NP-Hardness, Puzzles, Games, New York Times, Pips, Letter Boxed, Strands, Tiles}
}
Document
DOI: 10.4230/LIPIcs.FUN.2026.31
A Demigod’s Number for the Rubik’s Cube

Authors: Arturo Merino and Bernardo Subercaseaux

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract
It is by now well-known that any state of the 3× 3 × 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 diameter at most twice the average distance (of which we give a much simpler proof than in the literature). Then, 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 ± 0.18, from where the diameter is at most 36.
Cite as

Arturo Merino and Bernardo Subercaseaux. A Demigod’s Number for the Rubik’s Cube. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{merino_et_al:LIPIcs.FUN.2026.31,
  author =	{Merino, Arturo and Subercaseaux, Bernardo},
  title =	{{A Demigod’s Number for the Rubik’s Cube}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{31:1--31:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.31},
  URN =		{urn:nbn:de:0030-drops-257505},
  doi =		{10.4230/LIPIcs.FUN.2026.31},
  annote =	{Keywords: Diameter, Rubik’s Cube, Experimental mathematics}
}
Document
DOI: 10.4230/LIPIcs.FUN.2026.38
Solving Small Rubik’s Cubes as Slowly as Possible

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

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract
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 × 2 × 3 or 1 × 3 × 3 cuboids, which have under 200 states. This approach, however, becomes infeasible for the 2 × 2 × 2, which has over 3.6 million states. Our main result is then showing that the Strong Lovász Conjecture holds for the 2 × 2 × 2 cube, using a careful graph-theoretic construction based on the subgroup induced by the R and U turns.
Cite as

Jenny Quan, Noah Kim, Bernardo Subercaseaux, and John Mackey. Solving Small Rubik’s Cubes as Slowly as Possible. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{quan_et_al:LIPIcs.FUN.2026.38,
  author =	{Quan, Jenny and Kim, Noah and Subercaseaux, Bernardo and Mackey, John},
  title =	{{Solving Small Rubik’s Cubes as Slowly as Possible}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{38:1--38:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.38},
  URN =		{urn:nbn:de:0030-drops-257570},
  doi =		{10.4230/LIPIcs.FUN.2026.38},
  annote =	{Keywords: Hamilton connectivity, Rubik’s Cube, Finite group theory}
}
Document
DOI: 10.4230/LIPIcs.FUN.2026.39
Price of Locality in Permutation Mastermind: Are TikTok Influencers Chaotic Enough?

Authors: Bernardo Subercaseaux

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract
In the permutation Mastermind game, the goal is to uncover a secret permutation σ^⋆ : [n] → [n] by making a series of guesses π₁, …, π_T which must also be permutations of [n], and receiving as feedback after guess π_t the number of positions i for which σ^⋆(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: 𝓁_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 𝓁₃-local strategies, whereas in the 𝓁₂-local variant the problem admits a randomized polynomial-time algorithm.
Cite as

Bernardo Subercaseaux. Price of Locality in Permutation Mastermind: Are TikTok Influencers Chaotic Enough?. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{subercaseaux:LIPIcs.FUN.2026.39,
  author =	{Subercaseaux, Bernardo},
  title =	{{Price of Locality in Permutation Mastermind: Are TikTok Influencers Chaotic Enough?}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{39:1--39:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.39},
  URN =		{urn:nbn:de:0030-drops-257585},
  doi =		{10.4230/LIPIcs.FUN.2026.39},
  annote =	{Keywords: Permutation Mastermind, Locality, NP-hard}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2026.1
Query Languages for Machine-Learning Models (Invited Talk)

Authors: Martin Grohe

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
In my invited talk and this accompanying paper, I discuss two logics for weighted finite structures: first-order logic with summation (FO(SUM)) and its recursive extension IFP(SUM). These logics originate from foundational work by Grädel, Gurevich, and Meer in the 1990s. In recent joint work with Standke, Steegmans, and Van den Bussche, we have investigated these logics as query languages for machine learning models, specifically neural networks, which are naturally represented as weighted graphs. I present illustrative examples of queries to neural networks that can be expressed in these logics and discuss fundamental results on their expressiveness and computational complexity.
Cite as

Martin Grohe. Query Languages for Machine-Learning Models (Invited Talk). In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{grohe:LIPIcs.STACS.2026.1,
  author =	{Grohe, Martin},
  title =	{{Query Languages for Machine-Learning Models}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{1:1--1:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.1},
  URN =		{urn:nbn:de:0030-drops-254904},
  doi =		{10.4230/LIPIcs.STACS.2026.1},
  annote =	{Keywords: Expressive power of query languages, fixed-point logics, weighted structures, neural networks, explainable AI}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.24
Formally Verifying a Vertical Cell Decomposition Algorithm

Authors: Yves Bertot and Thomas Portet

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The broad context of this work is the application of formal methods to geometry and robotics. We describe an algorithm to decompose a working area containing obstacles into a collection of safe cells and the formal proof that this algorithm is correct. We expect such an algorithm will be useful to compute safe trajectories. To our knowledge, this is one of the first formalization of such an algorithm to decompose a working space into elementary cells that are suitable for later applications, with the proof of correctness that guarantees that large parts of the working space are safe. Techniques to perform this proof go from algebraic reasoning on coordinates and determinants to sorting. The main difficulty comes from the possible existence of degenerate cases, which are treated in a principled way.
Cite as

Yves Bertot and Thomas Portet. Formally Verifying a Vertical Cell Decomposition Algorithm. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2025.24,
  author =	{Bertot, Yves and Portet, Thomas},
  title =	{{Formally Verifying a Vertical Cell Decomposition Algorithm}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.24},
  URN =		{urn:nbn:de:0030-drops-246222},
  doi =		{10.4230/LIPIcs.ITP.2025.24},
  annote =	{Keywords: Formal Verification, Motion planning, algorithmic geometry}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.15
RustSAT: A Library for SAT Solving in Rust

Authors: Christoph Jabs

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems. To encourage their widespread adoption, the relatively high barrier of entry following from the low level syntax of SAT and the expert knowledge required to achieve tight integration with SAT solvers should be further reduced. We present RustSAT, a library with the aim of making SAT solving technology readily available in the Rust programming language. RustSAT provides functionality for helping with generating (Max)SAT instances, writing them to, or reading them from files. Furthermore, RustSAT includes interfaces to various state-of-the-art SAT solvers available with a unified Rust API. Lastly, RustSAT implements several encodings for higher level constraints (at-most-one, cardinality, and pseudo-Boolean), which are also available via a C and Python API.
Cite as

Christoph Jabs. RustSAT: A Library for SAT Solving in Rust. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 15:1-15:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jabs:LIPIcs.SAT.2025.15,
  author =	{Jabs, Christoph},
  title =	{{RustSAT: A Library for SAT Solving in Rust}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{15:1--15:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.15},
  URN =		{urn:nbn:de:0030-drops-237498},
  doi =		{10.4230/LIPIcs.SAT.2025.15},
  annote =	{Keywords: Rust, library, SAT solvers, constraint encodings}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.3
Problem Partitioning via Proof Prefixes

Authors: Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Satisfiability solvers have been instrumental in tackling hard problems, including mathematical challenges that require years of computation. A key obstacle in efficiently solving such problems lies in effectively partitioning them into many, frequently millions of subproblems. Existing automated partitioning techniques, primarily based on lookahead methods, perform well on some instances but fail to generate effective partitions for many others. This paper introduces a powerful partitioning approach that leverages prefixes of proofs derived from conflict-driven clause-learning solvers. This method enables non-experts to harness the power of massively parallel SAT solving for their problems. We also propose a semantically-driven partitioning technique tailored for problems with large cardinality constraints, which frequently arise in optimization tasks. We evaluate our methods on diverse benchmarks, including combinatorial problems and formulas from SAT and MaxSAT competitions. Our results demonstrate that these techniques outperform existing partitioning strategies in many cases, offering improved scalability and efficiency.
Cite as

Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule. Problem Partitioning via Proof Prefixes. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{battleman_et_al:LIPIcs.SAT.2025.3,
  author =	{Battleman, Zachary and Reeves, Joseph E. and Heule, Marijn J. H.},
  title =	{{Problem Partitioning via Proof Prefixes}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.3},
  URN =		{urn:nbn:de:0030-drops-237378},
  doi =		{10.4230/LIPIcs.SAT.2025.3},
  annote =	{Keywords: Satisfiability solving, parallel computing, problem partitioning}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.9
Query Languages for Neural Networks

Authors: Martin Grohe, Christoph Standke, Juno Steegmans, and Jan Van den Bussche

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
We lay the foundations for a database-inspired approach to interpreting and understanding neural network models by querying them using declarative languages. Towards this end we study different query languages, based on first-order logic, that mainly differ in their access to the neural network model. First-order logic over the reals naturally yields a language which views the network as a black box; only the input-output function defined by the network can be queried. This is essentially the approach of constraint query languages. On the other hand, a white-box language can be obtained by viewing the network as a weighted graph, and extending first-order logic with summation over weight terms. The latter approach is essentially an abstraction of SQL . In general, the two approaches are incomparable in expressive power, as we will show. Under natural circumstances, however, the white-box approach can subsume the black-box approach; this is our main result. We prove the result concretely for linear constraint queries over real functions definable by feedforward neural networks with a fixed number of hidden layers and piecewise linear activation functions.
Cite as

Martin Grohe, Christoph Standke, Juno Steegmans, and Jan Van den Bussche. Query Languages for Neural Networks. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grohe_et_al:LIPIcs.ICDT.2025.9,
  author =	{Grohe, Martin and Standke, Christoph and Steegmans, Juno and Van den Bussche, Jan},
  title =	{{Query Languages for Neural Networks}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.9},
  URN =		{urn:nbn:de:0030-drops-229508},
  doi =		{10.4230/LIPIcs.ICDT.2025.9},
  annote =	{Keywords: Expressive power of query languages, Machine learning models, languages for interpretability, explainable AI}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2025.81
Online Balanced Allocation of Dynamic Components

Authors: Rajmohan Rajaraman and Omer Wasim

Published in: LIPIcs, Volume 325, 16th Innovations in Theoretical Computer Science Conference (ITCS 2025)

Abstract
We introduce Online Balanced Allocation of Dynamic Components (OBADC), a problem motivated by the practical challenge of dynamic resource allocation for large-scale distributed applications. In OBADC, we need to allocate a dynamic set of at most k𝓁 vertices (representing processes) in 𝓁 > 0 clusters. We consider an over-provisioned setup in which each cluster can hold at most k(1+ε) vertices, for an arbitrary constant ε > 0. The communication requirements among the vertices are modeled by the notion of a dynamically changing component, which is a subset of vertices that need to be co-located in the same cluster. At each time t, a request r_t of one of the following types arrives: 1) insertion of a vertex v forming a singleton component v at unit cost. 2) merge of (u,v) requiring that the components containing u and v be merged and co-located thereafter. 3) deletion of an existing vertex v at zero cost. Before serving any request, an algorithm can migrate vertices from one cluster to another, at a unit migration cost per vertex. We seek an online algorithm to minimize the total migration cost incurred for an arbitrary request sequence σ = (r_t)_{t > 0}, while simultaneously minimizing the number of clusters utilized. We analyze competitiveness with respect to an optimal clairvoyant offline algorithm with identical (over-provisioned) capacity constraints. We give an O(log k)-competitive algorithm for OBADC, and a matching lower-bound. The number of clusters utilized by our algorithm is always within a (2+ε) factor of the minimum. Furthermore, in a resource augmented setting where the optimal offline algorithm is constrained to capacity k per cluster, our algorithm obtains O(log k) competitiveness and utilizes a number of clusters within (1+ε) factor of the minimum. We also consider OBADC in the context of machine-learned predictions, where for each newly inserted vertex v at time t: i) with probability η > 0, the set of vertices (that exist at time t) in the component of v is revealed and, ii) with probability 1-η, no information is revealed. For OBADC with predictions, we give a O(1)-consistent and O(min(log 1/(η), log k))-robust algorithm.
Cite as

Rajmohan Rajaraman and Omer Wasim. Online Balanced Allocation of Dynamic Components. In 16th Innovations in Theoretical Computer Science Conference (ITCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 325, pp. 81:1-81:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rajaraman_et_al:LIPIcs.ITCS.2025.81,
  author =	{Rajaraman, Rajmohan and Wasim, Omer},
  title =	{{Online Balanced Allocation of Dynamic Components}},
  booktitle =	{16th Innovations in Theoretical Computer Science Conference (ITCS 2025)},
  pages =	{81:1--81:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-361-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{325},
  editor =	{Meka, Raghu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2025.81},
  URN =		{urn:nbn:de:0030-drops-227090},
  doi =		{10.4230/LIPIcs.ITCS.2025.81},
  annote =	{Keywords: online algorithms, competitive ratio, algorithms with predictions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.17
Description Complexity of Unary Structures in First-Order Logic with Links to Entropy

Authors: Reijo Jaakkola, Antti Kuusisto, and Miikka Vilander

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
The description complexity of a model is the length of the shortest formula that defines the model. We study the description complexity of unary structures in first-order logic FO, also drawing links to semantic complexity in the form of entropy. The class of unary structures provides, e.g., a simple way to represent tabular Boolean data sets as relational structures. We define structures with FO-formulas that are strictly linear in the size of the model as opposed to using the naive quadratic ones, and we use arguments based on formula size games to obtain related lower bounds for description complexity. For a typical structure the upper and lower bounds in fact match up to a sublinear term, leading to a precise asymptotic result on the expected description complexity of a randomly selected structure. We then give bounds on the relationship between Shannon entropy and description complexity. We extend this relationship also to Boltzmann entropy by establishing an asymptotic match between the two entropies. Despite the simplicity of unary structures, our arguments require the use of formula size games, Stirling’s approximation and Chernoff bounds.
Cite as

Reijo Jaakkola, Antti Kuusisto, and Miikka Vilander. Description Complexity of Unary Structures in First-Order Logic with Links to Entropy. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jaakkola_et_al:LIPIcs.CSL.2025.17,
  author =	{Jaakkola, Reijo and Kuusisto, Antti and Vilander, Miikka},
  title =	{{Description Complexity of Unary Structures in First-Order Logic with Links to Entropy}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.17},
  URN =		{urn:nbn:de:0030-drops-227749},
  doi =		{10.4230/LIPIcs.CSL.2025.17},
  annote =	{Keywords: formula size, finite model theory, formula size games, entropy, randomness}
}
Artifact
Software
DOI: 10.4230/artifacts.22467
EmptyHexagonLean

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

Abstract
Cite as

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, Marijn J. H. Heule. EmptyHexagonLean (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22467,
   title = {{EmptyHexagonLean}}, 
   author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:29dc0e7145296997bcb1230b4e03cd14c8d75617;origin=https://github.com/bsubercaseaux/EmptyHexagonLean;visit=swh:1:snp:0e11d6564bd15317306605932e0acd87cf3d7f80;anchor=swh:1:rev:d7f798ffc8deabc2f3ca1ae36e92e0250e57c205}{\texttt{swh:1:dir:29dc0e7145296997bcb1230b4e03cd14c8d75617}} (visited on 2024-11-28)},
   url = {https://github.com/bsubercaseaux/EmptyHexagonLean/tree/itp2024},
   doi = {10.4230/artifacts.22467},
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.35
Formal Verification of the Empty Hexagon Number

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

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
A recent breakthrough in computer-assisted mathematics showed that every set of 30 points in the plane in general position (i.e., no three points on a common line) contains an empty convex hexagon. Heule and Scheucher solved this problem with a combination of geometric insights and automated reasoning techniques by constructing CNF formulas ϕ_n, with O(n⁴) clauses, such that if ϕ_n is unsatisfiable then every set of n points in general position must contain an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17 300 CPU hours of parallel computation. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers ideas in discrete computational geometry and SAT encoding techniques by introducing a framework that connects geometric objects to propositional assignments. We see this as a key step towards the formal verification of other SAT-based results in geometry, since the abstractions we use have been successfully applied to similar problems. Overall, we hope that our work sets a new standard for the verification of geometry problems relying on extensive computation, and that it increases the trust the mathematical community places in computer-assisted proofs.
Cite as

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. Formal Verification of the Empty Hexagon Number. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{subercaseaux_et_al:LIPIcs.ITP.2024.35,
  author =	{Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.},
  title =	{{Formal Verification of the Empty Hexagon Number}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35},
  URN =		{urn:nbn:de:0030-drops-207633},
  doi =		{10.4230/LIPIcs.ITP.2024.35},
  annote =	{Keywords: Empty Hexagon Number, Discrete Computational Geometry, Erd\H{o}s-Szekeres}
}
  • Refine by Type
  • 21 Document/PDF
  • 11 Document/HTML
  • 1 Artifact

  • Refine by Publication Year
  • 7 2026
  • 6 2025
  • 4 2024
  • 1 2023
  • 2 2022
  • Show More...

  • Refine by Author
  • 12 Subercaseaux, Bernardo
  • 6 Heule, Marijn J. H.
  • 2 Carneiro, Mario
  • 2 Codel, Cayden
  • 2 Gallicchio, James
  • Show More...

  • Refine by Series/Journal
  • 21 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Automated reasoning
  • 3 Theory of computation → Constraint and logic programming
  • 3 Theory of computation → Logic and verification
  • 2 Mathematics of computing → Combinatorics
  • 2 Mathematics of computing → Paths and connectivity problems
  • Show More...

  • Refine by Keyword
  • 2 CNF encodings
  • 2 Expressive power of query languages
  • 2 Rubik’s Cube
  • 2 SAT solvers
  • 2 explainable AI
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact