9 Search Results for "Chen, Joshua"

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.CP.2024.20
Constraint Modelling with LLMs Using In-Context Learning

Authors: Kostis Michailidis, Dimos Tsouros, and Tias Guns

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Constraint Programming (CP) allows for the modelling and solving of a wide range of combinatorial problems. However, modelling such problems using constraints over decision variables still requires significant expertise, both in conceptual thinking and syntactic use of modelling languages. In this work, we explore the potential of using pre-trained Large Language Models (LLMs) as coding assistants, to transform textual problem descriptions into concrete and executable CP specifications. We present different transformation pipelines with explicit intermediate representations, and we investigate the potential benefit of various retrieval-augmented example selection strategies for in-context learning. We evaluate our approach on 2 datasets from the literature, namely NL4Opt (optimisation) and Logic Grid Puzzles (satisfaction), and a heterogeneous set of exercises from a CP course. The results show that pre-trained LLMs have promising potential for initialising the modelling process, with retrieval-augmented in-context learning significantly enhancing their modelling capabilities.
Cite as

Kostis Michailidis, Dimos Tsouros, and Tias Guns. Constraint Modelling with LLMs Using In-Context Learning. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{michailidis_et_al:LIPIcs.CP.2024.20,
  author =	{Michailidis, Kostis and Tsouros, Dimos and Guns, Tias},
  title =	{{Constraint Modelling with LLMs Using In-Context Learning}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{20:1--20:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.20},
  URN =		{urn:nbn:de:0030-drops-207053},
  doi =		{10.4230/LIPIcs.CP.2024.20},
  annote =	{Keywords: Constraint Modelling, Constraint Acquisition, Constraint Programming, Large Language Models, In-Context Learning, Natural Language Processing, Named Entity Recognition, Retrieval-Augmented Generation, Optimisation}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2024.31
On the Complexity of Isomorphism Problems for Tensors, Groups, and Polynomials III: Actions by Classical Groups

Authors: Zhili Chen, Joshua A. Grochow, Youming Qiao, Gang Tang, and Chuanqi Zhang

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
We study the complexity of isomorphism problems for d-way arrays, or tensors, under natural actions by classical groups such as orthogonal, unitary, and symplectic groups. These problems arise naturally in statistical data analysis and quantum information. We study two types of complexity-theoretic questions. First, for a fixed action type (isomorphism, conjugacy, etc.), we relate the complexity of the isomorphism problem over a classical group to that over the general linear group. Second, for a fixed group type (orthogonal, unitary, or symplectic), we compare the complexity of the isomorphism problems for different actions. Our main results are as follows. First, for orthogonal and symplectic groups acting on 3-way arrays, the isomorphism problems reduce to the corresponding problems over the general linear group. Second, for orthogonal and unitary groups, the isomorphism problems of five natural actions on 3-way arrays are polynomial-time equivalent, and the d-tensor isomorphism problem reduces to the 3-tensor isomorphism problem for any fixed d > 3. For unitary groups, the preceding result implies that LOCC classification of tripartite quantum states is at least as difficult as LOCC classification of d-partite quantum states for any d. Lastly, we also show that the graph isomorphism problem reduces to the tensor isomorphism problem over orthogonal and unitary groups.
Cite as

Zhili Chen, Joshua A. Grochow, Youming Qiao, Gang Tang, and Chuanqi Zhang. On the Complexity of Isomorphism Problems for Tensors, Groups, and Polynomials III: Actions by Classical Groups. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITCS.2024.31,
  author =	{Chen, Zhili and Grochow, Joshua A. and Qiao, Youming and Tang, Gang and Zhang, Chuanqi},
  title =	{{On the Complexity of Isomorphism Problems for Tensors, Groups, and Polynomials III: Actions by Classical Groups}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{31:1--31:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.31},
  URN =		{urn:nbn:de:0030-drops-195595},
  doi =		{10.4230/LIPIcs.ITCS.2024.31},
  annote =	{Keywords: complexity class, tensor isomorphism, polynomial isomorphism, group isomorphism, local operations and classical communication}
}
Document
DOI: 10.4230/LIPIcs.DNA.29.8
Thermodynamically Driven Signal Amplification

Authors: Joshua Petrack, David Soloveichik, and David Doty

Published in: LIPIcs, Volume 276, 29th International Conference on DNA Computing and Molecular Programming (DNA 29) (2023)

Abstract
The field of chemical computation attempts to model computational behavior that arises when molecules, typically nucleic acids, are mixed together. By modeling this physical phenomenon at different levels of specificity, different operative computational behavior is observed. Thermodynamic binding networks (TBNs) is a highly abstracted model that focuses on which molecules are bound to each other in a "thermodynamically stable" sense. Stability is measured based only on how many bonds are formed and how many total complexes are in a configuration, without focusing on how molecules are binding or how they became bound. By defocusing on kinetic processes, TBNs attempt to naturally model the long-term behavior of a mixture (i.e., its thermodynamic equilibrium). We study the problem of signal amplification: detecting a small quantity of some molecule and amplifying its signal to something more easily detectable. This problem has natural applications such as disease diagnosis. By focusing on thermodynamically favored outcomes, we seek to design chemical systems that perform the task of signal amplification robustly without relying on kinetic pathways that can be error prone and require highly controlled conditions (e.g., PCR amplification). It might appear that a small change in concentrations can result in only small changes to the thermodynamic equilibrium of a molecular system. However, we show that it is possible to design a TBN that can "exponentially amplify" a signal represented by a single copy of a monomer called the analyte: this TBN has exactly one stable state before adding the analyte and exactly one stable state afterward, and those two states "look very different" from each other. In particular, their difference is exponential in the number of types of molecules and their sizes. The system can be programmed to any desired level of resilience to false positives and false negatives. To prove these results, we introduce new concepts to the TBN model, particularly the notions of a TBN’s entropy gap to describe how unlikely it is to be observed in an undesirable state, and feed-forward TBNs that have a strong upper bound on the number of polymers in a stable configuration. We also show a corresponding negative result: a doubly exponential upper bound, meaning that there is no TBN that can amplify a signal by an amount more than doubly exponential in the number and sizes of different molecules that comprise it. We leave as an open question to close this gap by either proving an exponential upper bound, or giving a construction with a doubly-exponential difference between the stable configurations before and after the analyte is added. Our work informs the fundamental question of how a thermodynamic equilibrium can change as a result of a small change to the system (adding a single molecule copy). While exponential amplification is traditionally viewed as inherently a non-equilibrium phenomenon, we find that in a strong sense exponential amplification can occur at thermodynamic equilibrium as well - where the "effect" (e.g., fluorescence) is exponential in types and complexity of the chemical components.
Cite as

Joshua Petrack, David Soloveichik, and David Doty. Thermodynamically Driven Signal Amplification. In 29th International Conference on DNA Computing and Molecular Programming (DNA 29). Leibniz International Proceedings in Informatics (LIPIcs), Volume 276, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{petrack_et_al:LIPIcs.DNA.29.8,
  author =	{Petrack, Joshua and Soloveichik, David and Doty, David},
  title =	{{Thermodynamically Driven Signal Amplification}},
  booktitle =	{29th International Conference on DNA Computing and Molecular Programming (DNA 29)},
  pages =	{8:1--8:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-297-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{276},
  editor =	{Chen, Ho-Lin and Evans, Constantine G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.29.8},
  URN =		{urn:nbn:de:0030-drops-187917},
  doi =		{10.4230/LIPIcs.DNA.29.8},
  annote =	{Keywords: Thermodynamic binding networks, signal amplification, integer programming}
}
Document
DOI: 10.4230/LIPIcs.CPM.2021.24
AWLCO: All-Window Length Co-Occurrence

Authors: Joshua Sobel, Noah Bertram, Chen Ding, Fatemeh Nargesian, and Daniel Gildea

Published in: LIPIcs, Volume 191, 32nd Annual Symposium on Combinatorial Pattern Matching (CPM 2021)

Abstract
Analyzing patterns in a sequence of events has applications in text analysis, computer programming, and genomics research. In this paper, we consider the all-window-length analysis model which analyzes a sequence of events with respect to windows of all lengths. We study the exact co-occurrence counting problem for the all-window-length analysis model. Our first algorithm is an offline algorithm that counts all-window-length co-occurrences by performing multiple passes over a sequence and computing single-window-length co-occurrences. This algorithm has the time complexity O(n) for each window length and thus a total complexity of O(n²) and the space complexity O(|I|) for a sequence of size n and an itemset of size |I|. We propose AWLCO, an online algorithm that computes all-window-length co-occurrences in a single pass with the time complexity of O(n) and space complexity of O(√{n|I|}), assuming perfect hashing. Following this, we generalize our use case to patterns in which we propose an algorithm that computes all-window-length co-occurrence with time complexity O(n|I|), assuming perfect hashing, with an additional pre-processing step and space complexity O(√{n|I|}+|I|), plus the overhead of the Aho-Corasick algorithm [Aho and Corasick, 1975].
Cite as

Joshua Sobel, Noah Bertram, Chen Ding, Fatemeh Nargesian, and Daniel Gildea. AWLCO: All-Window Length Co-Occurrence. In 32nd Annual Symposium on Combinatorial Pattern Matching (CPM 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 191, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{sobel_et_al:LIPIcs.CPM.2021.24,
  author =	{Sobel, Joshua and Bertram, Noah and Ding, Chen and Nargesian, Fatemeh and Gildea, Daniel},
  title =	{{AWLCO: All-Window Length Co-Occurrence}},
  booktitle =	{32nd Annual Symposium on Combinatorial Pattern Matching (CPM 2021)},
  pages =	{24:1--24:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-186-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{191},
  editor =	{Gawrychowski, Pawe{\l} and Starikovskaya, Tatiana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2021.24},
  URN =		{urn:nbn:de:0030-drops-139759},
  doi =		{10.4230/LIPIcs.CPM.2021.24},
  annote =	{Keywords: Itemsets, Data Sequences, Co-occurrence}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.12
Homotopy Type Theory in Isabelle

Authors: Joshua Chen

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle’s existing logical framework infrastructure to implement essential automation, such as type checking and term elaboration, that is usually handled on the source code level of dependently typed systems. I also integrate the propositions-as-types paradigm with the declarative Isar proof language, providing an alternative to the tactic-based proofs of Coq and the proof terms of Agda. The infrastructure developed is then used to formalize foundational results from the Homotopy Type Theory book.
Cite as

Joshua Chen. Homotopy Type Theory in Isabelle. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 12:1-12:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{chen:LIPIcs.ITP.2021.12,
  author =	{Chen, Joshua},
  title =	{{Homotopy Type Theory in Isabelle}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{12:1--12:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.12},
  URN =		{urn:nbn:de:0030-drops-139072},
  doi =		{10.4230/LIPIcs.ITP.2021.12},
  annote =	{Keywords: Proof assistants, Logical frameworks, Dependent type theory, Homotopy type theory}
}
Document
DOI: 10.4230/LIPIcs.FUN.2021.7
1 X 1 Rush Hour with Fixed Blocks Is PSPACE-Complete

Authors: Josh Brunner, Lily Chung, Erik D. Demaine, Dylan Hendrickson, Adam Hesterberg, Adam Suhl, and Avi Zeff

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

Abstract
Consider n²-1 unit-square blocks in an n × n square board, where each block is labeled as movable horizontally (only), movable vertically (only), or immovable - a variation of Rush Hour with only 1 × 1 cars and fixed blocks. We prove that it is PSPACE-complete to decide whether a given block can reach the left edge of the board, by reduction from Nondeterministic Constraint Logic via 2-color oriented Subway Shuffle. By contrast, polynomial-time algorithms are known for deciding whether a given block can be moved by one space, or when each block either is immovable or can move both horizontally and vertically. Our result answers a 15-year-old open problem by Tromp and Cilibrasi, and strengthens previous PSPACE-completeness results for Rush Hour with vertical 1 × 2 and horizontal 2 × 1 movable blocks and 4-color Subway Shuffle.
Cite as

Josh Brunner, Lily Chung, Erik D. Demaine, Dylan Hendrickson, Adam Hesterberg, Adam Suhl, and Avi Zeff. 1 X 1 Rush Hour with Fixed Blocks Is PSPACE-Complete. In 10th International Conference on Fun with Algorithms (FUN 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 157, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{brunner_et_al:LIPIcs.FUN.2021.7,
  author =	{Brunner, Josh and Chung, Lily and Demaine, Erik D. and Hendrickson, Dylan and Hesterberg, Adam and Suhl, Adam and Zeff, Avi},
  title =	{{1 X 1 Rush Hour with Fixed Blocks Is PSPACE-Complete}},
  booktitle =	{10th International Conference on Fun with Algorithms (FUN 2021)},
  pages =	{7:1--7:14},
  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.7},
  URN =		{urn:nbn:de:0030-drops-127681},
  doi =		{10.4230/LIPIcs.FUN.2021.7},
  annote =	{Keywords: puzzles, sliding blocks, PSPACE-hardness}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.113
Counting Answers to Existential Questions (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Holger Dell, Marc Roth, and Philip Wellnitz

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Conjunctive queries select and are expected to return certain tuples from a relational database. We study the potentially easier problem of counting all selected tuples, rather than enumerating them. In particular, we are interested in the problem’s parameterized and data complexity, where the query is considered to be small or even fixed, and the database is considered to be large. We identify two structural parameters for conjunctive queries that capture their inherent complexity: The dominating star size and the linked matching number. If the dominating star size of a conjunctive query is large, then we show that counting solution tuples to the query is at least as hard as counting dominating sets, which yields a fine-grained complexity lower bound under the Strong Exponential Time Hypothesis (SETH) as well as a #W[2]-hardness result in parameterized complexity. Moreover, if the linked matching number of a conjunctive query is large, then we show that the structure of the query is so rich that arbitrary queries up to a certain size can be encoded into it; in the language of parameterized complexity, this essentially establishes a #A[2]-completeness result. Using ideas stemming from Lovász (1967), we lift complexity results from the class of conjunctive queries to arbitrary existential or universal formulas that might contain inequalities and negations on constraints over the free variables. As a consequence, we obtain a complexity classification that refines and generalizes previous results of Chen, Durand, and Mengel (ToCS 2015; ICDT 2015; PODS 2016) for conjunctive queries and of Curticapean and Marx (FOCS 2014) for the subgraph counting problem. Our proof also relies on graph minors, and we show a strengthening of the Excluded-Grid-Theorem which might be of independent interest: If the linked matching number (and thus the treewidth) is large, then not only can we find a large grid somewhere in the graph, but we can find a large grid whose diagonal has disjoint paths leading into an assumed node-well-linked set.
Cite as

Holger Dell, Marc Roth, and Philip Wellnitz. Counting Answers to Existential Questions (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 113:1-113:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dell_et_al:LIPIcs.ICALP.2019.113,
  author =	{Dell, Holger and Roth, Marc and Wellnitz, Philip},
  title =	{{Counting Answers to Existential Questions}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{113:1--113:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.113},
  URN =		{urn:nbn:de:0030-drops-106894},
  doi =		{10.4230/LIPIcs.ICALP.2019.113},
  annote =	{Keywords: Conjunctive queries, graph homomorphisms, counting complexity, parameterized complexity, fine-grained complexity}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2018.43
Computational Topology and the Unique Games Conjecture

Authors: Joshua A. Grochow and Jamie Tucker-Foltz

Published in: LIPIcs, Volume 99, 34th International Symposium on Computational Geometry (SoCG 2018)

Abstract
Covering spaces of graphs have long been useful for studying expanders (as "graph lifts") and unique games (as the "label-extended graph"). In this paper we advocate for the thesis that there is a much deeper relationship between computational topology and the Unique Games Conjecture. Our starting point is Linial's 2005 observation that the only known problems whose inapproximability is equivalent to the Unique Games Conjecture - Unique Games and Max-2Lin - are instances of Maximum Section of a Covering Space on graphs. We then observe that the reduction between these two problems (Khot-Kindler-Mossel-O'Donnell, FOCS '04; SICOMP '07) gives a well-defined map of covering spaces. We further prove that inapproximability for Maximum Section of a Covering Space on (cell decompositions of) closed 2-manifolds is also equivalent to the Unique Games Conjecture. This gives the first new "Unique Games-complete" problem in over a decade. Our results partially settle an open question of Chen and Freedman (SODA, 2010; Disc. Comput. Geom., 2011) from computational topology, by showing that their question is almost equivalent to the Unique Games Conjecture. (The main difference is that they ask for inapproximability over Z_2, and we show Unique Games-completeness over Z_k for large k.) This equivalence comes from the fact that when the structure group G of the covering space is Abelian - or more generally for principal G-bundles - Maximum Section of a G-Covering Space is the same as the well-studied problem of 1-Homology Localization. Although our most technically demanding result is an application of Unique Games to computational topology, we hope that our observations on the topological nature of the Unique Games Conjecture will lead to applications of algebraic topology to the Unique Games Conjecture in the future.
Cite as

Joshua A. Grochow and Jamie Tucker-Foltz. Computational Topology and the Unique Games Conjecture. In 34th International Symposium on Computational Geometry (SoCG 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 99, pp. 43:1-43:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{grochow_et_al:LIPIcs.SoCG.2018.43,
  author =	{Grochow, Joshua A. and Tucker-Foltz, Jamie},
  title =	{{Computational Topology and the Unique Games Conjecture}},
  booktitle =	{34th International Symposium on Computational Geometry (SoCG 2018)},
  pages =	{43:1--43:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-066-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{99},
  editor =	{Speckmann, Bettina and T\'{o}th, Csaba D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2018.43},
  URN =		{urn:nbn:de:0030-drops-87566},
  doi =		{10.4230/LIPIcs.SoCG.2018.43},
  annote =	{Keywords: Unique Games Conjecture, homology localization, inapproximability, computational topology, graph lift, covering graph, permutation voltage graph, cell}
}
  • Refine by Author
  • 2 Grochow, Joshua A.
  • 1 Bertram, Noah
  • 1 Brunner, Josh
  • 1 Carneiro, Mario
  • 1 Chen, Joshua
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Co-occurrence
  • 1 Conjunctive queries
  • 1 Constraint Acquisition
  • 1 Constraint Modelling
  • 1 Constraint Programming
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 3 2024
  • 2 2021
  • 1 2018
  • 1 2019
  • 1 2020
  • Show More...

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 About DROPS Imprint Privacy Contact