8 Search Results for "Subercaseaux, Bernardo"

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}
}
Document
DOI: 10.4230/LIPIcs.FUN.2024.14
PackIt!: Gamified Rectangle Packing

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

Published in: LIPIcs, Volume 291, 12th International Conference on Fun with Algorithms (FUN 2024)

Abstract
We present and analyze PackIt!, a turn-based game consisting of packing rectangles on an n × n grid. PackIt! can be easily played on paper, either as a competitive two-player game or in solitaire fashion. On the t-th turn, a rectangle of area t or t+1 must be placed in the grid. In the two-player format of PackIt! whichever player places a rectangle last wins, whereas the goal in the solitaire variant is to perfectly pack the n × n grid. We analyze necessary conditions for the existence of a perfect packing over n × 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.
Cite as

Thomas Garrison, Marijn J. H. Heule, and Bernardo Subercaseaux. PackIt!: Gamified Rectangle Packing. In 12th International Conference on Fun with Algorithms (FUN 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 291, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{garrison_et_al:LIPIcs.FUN.2024.14,
  author =	{Garrison, Thomas and Heule, Marijn J. H. and Subercaseaux, Bernardo},
  title =	{{PackIt!: Gamified Rectangle Packing}},
  booktitle =	{12th International Conference on Fun with Algorithms (FUN 2024)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-314-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{291},
  editor =	{Broder, Andrei Z. and Tamir, Tami},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2024.14},
  URN =		{urn:nbn:de:0030-drops-199226},
  doi =		{10.4230/LIPIcs.FUN.2024.14},
  annote =	{Keywords: PackIt!, rectangle packing, SAT, NP-hardness}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.59
Lower Bounds for Set-Blocked Clauses Proofs

Authors: Emre Yolcu

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built on resolution. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution - all "without new variables." They may be viewed as weak versions of extended resolution (ER) since they are defined by first generalizing the extension rule and then taking away the ability to introduce new variables. Except for SBC⁻, they are known to be strictly between resolution and extended resolution. Several separations between these systems were proved earlier by exploiting the fact that they effectively simulate ER. We answer the questions left open: We prove exponential lower bounds for SBC⁻ proofs of a binary encoding of the pigeonhole principle, which separates ER from SBC⁻. Using this new separation, we prove that both RAT⁻ and GER⁻ are exponentially separated from SBC⁻. This completes the picture of their relative strengths.
Cite as

Emre Yolcu. Lower Bounds for Set-Blocked Clauses Proofs. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 59:1-59:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{yolcu:LIPIcs.STACS.2024.59,
  author =	{Yolcu, Emre},
  title =	{{Lower Bounds for Set-Blocked Clauses Proofs}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{59:1--59:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.59},
  URN =		{urn:nbn:de:0030-drops-197698},
  doi =		{10.4230/LIPIcs.STACS.2024.59},
  annote =	{Keywords: proof complexity, separations, resolution, extended resolution, blocked clauses}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.11
Effective Auxiliary Variables via Structured Reencoding

Authors: Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
Extended resolution shows that auxiliary variables are very powerful in theory. However, attempts to exploit this potential in practice have had limited success. One reasonably effective method in this regard is bounded variable addition (BVA), which automatically reencodes formulas by introducing new variables and eliminating clauses, often significantly reducing formula size. We find motivating examples suggesting that the performance improvement caused by BVA stems not only from this size reduction but also from the introduction of effective auxiliary variables. Analyzing specific packing-coloring instances, we discover that BVA is fragile with respect to formula randomization, relying on variable order to break ties. With this understanding, we augment BVA with a heuristic for breaking ties in a structured way. We evaluate our new preprocessing technique, Structured BVA (SBVA), on more than 29 000 formulas from previous SAT competitions and show that it is robust to randomization. In a simulated competition setting, our implementation outperforms BVA on both randomized and original formulas, and appears to be well-suited for certain families of formulas.
Cite as

Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective Auxiliary Variables via Structured Reencoding. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{haberlandt_et_al:LIPIcs.SAT.2023.11,
  author =	{Haberlandt, Andrew and Green, Harrison and Heule, Marijn J. H.},
  title =	{{Effective Auxiliary Variables via Structured Reencoding}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.11},
  URN =		{urn:nbn:de:0030-drops-184736},
  doi =		{10.4230/LIPIcs.SAT.2023.11},
  annote =	{Keywords: Reencoding, Auxiliary Variables, Extended Resolution}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.21
The Packing Chromatic Number of the Infinite Square Grid Is at Least 14

Authors: Bernardo Subercaseaux and Marijn J.H. Heule

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
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.
Cite as

Bernardo Subercaseaux and Marijn J.H. Heule. The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{subercaseaux_et_al:LIPIcs.SAT.2022.21,
  author =	{Subercaseaux, Bernardo and Heule, Marijn J.H.},
  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)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.21},
  URN =		{urn:nbn:de:0030-drops-166951},
  doi =		{10.4230/LIPIcs.SAT.2022.21},
  annote =	{Keywords: packing coloring, SAT solvers, encodings}
}
Document
DOI: 10.4230/LIPIcs.FUN.2022.19
Wordle Is NP-Hard

Authors: Daniel Lokshtanov and Bernardo Subercaseaux

Published in: LIPIcs, Volume 226, 11th International Conference on Fun with Algorithms (FUN 2022)

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

Daniel Lokshtanov and Bernardo Subercaseaux. Wordle Is NP-Hard. In 11th International Conference on Fun with Algorithms (FUN 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 226, pp. 19:1-19:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lokshtanov_et_al:LIPIcs.FUN.2022.19,
  author =	{Lokshtanov, Daniel and Subercaseaux, Bernardo},
  title =	{{Wordle Is NP-Hard}},
  booktitle =	{11th International Conference on Fun with Algorithms (FUN 2022)},
  pages =	{19:1--19:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-232-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{226},
  editor =	{Fraigniaud, Pierre and Uno, Yushi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2022.19},
  URN =		{urn:nbn:de:0030-drops-159893},
  doi =		{10.4230/LIPIcs.FUN.2022.19},
  annote =	{Keywords: wordle, np-hardness, complexity}
}
Document
DOI: 10.4230/LIPIcs.FUN.2021.23
The Computational Complexity of Evil Hangman

Authors: Jérémy Barbay and Bernardo Subercaseaux

Published in: LIPIcs, Volume 157, 10th International Conference on Fun with Algorithms (FUN 2021) (2020)

Abstract
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.
Cite as

Jérémy Barbay and Bernardo Subercaseaux. The Computational Complexity of Evil Hangman. In 10th International Conference on Fun with Algorithms (FUN 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 157, pp. 23:1-23:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{barbay_et_al:LIPIcs.FUN.2021.23,
  author =	{Barbay, J\'{e}r\'{e}my and Subercaseaux, Bernardo},
  title =	{{The Computational Complexity of Evil Hangman}},
  booktitle =	{10th International Conference on Fun with Algorithms (FUN 2021)},
  pages =	{23:1--23:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-145-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{157},
  editor =	{Farach-Colton, Martin and Prencipe, Giuseppe and Uehara, Ryuhei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2021.23},
  URN =		{urn:nbn:de:0030-drops-127840},
  doi =		{10.4230/LIPIcs.FUN.2021.23},
  annote =	{Keywords: combinatorial game theory, computational complexity, decidability, hangman}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2020.6
On the Expressiveness of LARA: A Unified Language for Linear and Relational Algebra

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

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)

Abstract
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.
Cite as

Pablo Barceló, Nelson Higuera, Jorge Pérez, and Bernardo Subercaseaux. On the Expressiveness of LARA: A Unified Language for Linear and Relational Algebra. In 23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{barcelo_et_al:LIPIcs.ICDT.2020.6,
  author =	{Barcel\'{o}, Pablo and Higuera, Nelson and P\'{e}rez, Jorge and Subercaseaux, Bernardo},
  title =	{{On the Expressiveness of LARA: A Unified Language for Linear and Relational Algebra}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020.6},
  URN =		{urn:nbn:de:0030-drops-119305},
  doi =		{10.4230/LIPIcs.ICDT.2020.6},
  annote =	{Keywords: languages for linear and relational algebra, expressive power, first order logic with aggregation, matrix convolution, matrix inverse, query genericity, locality of queries, safety}
}
  • Refine by Author
  • 6 Subercaseaux, Bernardo
  • 3 Heule, Marijn J. H.
  • 1 Barbay, Jérémy
  • 1 Barceló, Pablo
  • 1 Carneiro, Mario
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Problems, reductions and completeness
  • 1 Information systems → Query languages
  • 1 Mathematics of computing → Combinatoric problems
  • 1 Mathematics of computing → Combinatorics
  • Show More...

  • Refine by Keyword
  • 1 Auxiliary Variables
  • 1 Discrete Computational Geometry
  • 1 Empty Hexagon Number
  • 1 Erdős-Szekeres
  • 1 Extended Resolution
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 3 2024
  • 2 2020
  • 2 2022
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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