Search Results

Documents authored by Tóran, Jacobo

Found 2 Possible Name Variants:

Torán, Jacobo

Document
DOI: 10.4230/LIPIcs.MFCS.2024.64
Pebble Games and Algebraic Proof Systems

Authors: Lisa-Marie Jaser and Jacobo Torán

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
Analyzing refutations of the well known pebbling formulas Peb(G) we prove some new strong connections between pebble games and algebraic proof system, showing that there is a parallelism between the reversible, black and black-white pebbling games on one side, and the three algebraic proof systems Nullstellensatz, Monomial Calculus and Polynomial Calculus on the other side. In particular we prove that for any DAG G with a single sink, if there is a Monomial Calculus refutation for Peb(G) having simultaneously degree s and size t then there is a black pebbling strategy on G with space s and time t+s. Also if there is a black pebbling strategy for G with space s and time t it is possible to extract from it a MC refutation for Peb(G) having simultaneously degree s and size ts. These results are analogous to those proven in [Susanna F. de Rezende et al., 2021] for the case of reversible pebbling and Nullstellensatz. Using them we prove degree separations between NS, MC and PC, as well as strong degree-size tradeoffs for MC. We also notice that for any directed acyclic graph G the space needed in a pebbling strategy on G, for the three versions of the game, reversible, black and black-white, exactly matches the variable space complexity of a refutation of the corresponding pebbling formula Peb(G) in each of the algebraic proof systems NS,MC and PC. Using known pebbling bounds on graphs, this connection implies separations between the corresponding variable space measures.
Cite as

Lisa-Marie Jaser and Jacobo Torán. Pebble Games and Algebraic Proof Systems. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 64:1-64:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jaser_et_al:LIPIcs.MFCS.2024.64,
  author =	{Jaser, Lisa-Marie and Tor\'{a}n, Jacobo},
  title =	{{Pebble Games and Algebraic Proof Systems}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{64:1--64:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.64},
  URN =		{urn:nbn:de:0030-drops-206200},
  doi =		{10.4230/LIPIcs.MFCS.2024.64},
  annote =	{Keywords: Proof Complexity, Algebraic Proof Systems, Pebble Games}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.26
Cutting Planes Width and the Complexity of Graph Isomorphism Refutations

Authors: Jacobo Torán and Florian Wörz

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

Abstract
The width complexity measure plays a central role in Resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most extended method for proving size lower bounds, and it is known that for these systems, proofs with small width also imply the existence of proofs with small size. Not much has been studied, however, about the width parameter in the Cutting Planes (CP) proof system, a measure that was introduced by Dantchev and Martin in 2011 under the name of CP cutwidth. In this paper, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs G and H, we show a direct connection between the Weisfeiler-Leman differentiation number WL(G, H) of the graphs and the width of a CP refutation for the corresponding isomorphism formula Iso(G, H). In particular, we show that if WL(G, H) ≤ k, then there is a CP refutation of Iso(G, H) with width k, and if WL(G, H) > k, then there are no CP refutations of Iso(G, H) with width k-2. Similar results are known for other proof systems, like Resolution, Sherali-Adams, or Polynomial Calculus. We also obtain polynomial-size CP refutations from our width bound for isomorphism formulas for graphs with constant WL-dimension.
Cite as

Jacobo Torán and Florian Wörz. Cutting Planes Width and the Complexity of Graph Isomorphism Refutations. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{toran_et_al:LIPIcs.SAT.2023.26,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Cutting Planes Width and the Complexity of Graph Isomorphism Refutations}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{26:1--26:20},
  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.26},
  URN =		{urn:nbn:de:0030-drops-184884},
  doi =		{10.4230/LIPIcs.SAT.2023.26},
  annote =	{Keywords: Cutting Planes, Proof Complexity, Linear Programming, Combinatorial Optimization, Weisfeiler-Leman Algorithm, Graph Isomorphism}
}
Document
DOI: 10.4230/DagRep.12.9.41
Algebraic and Analytic Methods in Computational Complexity (Dagstuhl Seminar 22371)

Authors: Markus Bläser, Valentine Kabanets, Ronen Shaltiel, and Jacobo Torán

Published in: Dagstuhl Reports, Volume 12, Issue 9 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 2237 "Algebraic and Analytic Methods in Computational Complexity". Computational Complexity is concerned with the resources that are required for algorithms to detect properties of combinatorial objects and structures. It has often proven true that the best way to argue about these combinatorial objects is by establishing a connection (perhaps approximate) to a more well-behaved algebraic setting. Beside algebraic methods, analytic methods have been used for quite some time in theoretical computer science. These methods can also be used to solve algebraic problems as show by many recent examples in the areas of derandomization, coding theory or circuit lower bounds. These new directions were in the focus of the Dagstuhl Seminar and reflect the developments in the field since the previous Dagstuhl Seminar 18391. This Dagstuhl Seminar brought together researchers who are using a diverse array of algebraic and analytic methods in a variety of settings. Researchers in these areas are relying on ever more sophisticated and specialized mathematics and this seminar played a role in educating a diverse community about the latest new techniques, spurring further progress.
Cite as

Markus Bläser, Valentine Kabanets, Ronen Shaltiel, and Jacobo Torán. Algebraic and Analytic Methods in Computational Complexity (Dagstuhl Seminar 22371). In Dagstuhl Reports, Volume 12, Issue 9, pp. 41-59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{blaser_et_al:DagRep.12.9.41,
  author =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Shaltiel, Ronen and Tor\'{a}n, Jacobo},
  title =	{{Algebraic and Analytic Methods in Computational Complexity (Dagstuhl Seminar 22371)}},
  pages =	{41--59},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{9},
  editor =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Shaltiel, Ronen and Tor\'{a}n, Jacobo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.9.41},
  URN =		{urn:nbn:de:0030-drops-178092},
  doi =		{10.4230/DagRep.12.9.41},
  annote =	{Keywords: (de-)randomization, algebra, circuits, coding, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.36
Number of Variables for Graph Differentiation and the Resolution of GI Formulas

Authors: Jacobo Torán and Florian Wörz

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and positive depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution. Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular, we show that if k is the number of variables needed to distinguish two graphs with n vertices each, then there is an n^O(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2^(k-1) and k for the tree-like resolution size and resolution clause space for this formula. We also show a (normal) resolution size lower bound of exp(Ω(k²/n)) for the case of colored graphs with constant color class sizes. Applying these results, we prove the first exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule, thereby answering an open question posed by Schweitzer and Seebach.
Cite as

Jacobo Torán and Florian Wörz. Number of Variables for Graph Differentiation and the Resolution of GI Formulas. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{toran_et_al:LIPIcs.CSL.2022.36,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Number of Variables for Graph Differentiation and the Resolution of GI Formulas}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.36},
  URN =		{urn:nbn:de:0030-drops-157564},
  doi =		{10.4230/LIPIcs.CSL.2022.36},
  annote =	{Keywords: Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, k-variable fragment first-order logic 𝔏\underlinek, Immerman’s Pebble Game, Symmetry Rule, SRC-1}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.60
Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space

Authors: Jacobo Torán and Florian Wörz

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
We show a new connection between the space measure in tree-like resolution and the reversible pebble game in graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the space complexity measure in tree-like and general resolution. We show that these separations are not far from optimal by proving upper bounds for tree-like resolution space in terms of general resolution clause and variable space. In particular we show that for any formula F, its tree-like resolution space is upper bounded by space(π)log(time(π)), where π is any general resolution refutation of F. This holds considering as space(π) the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas, we are able to improve this bound to the optimal bound space(π)log n, where n is the number of vertices of the corresponding graph.
Cite as

Jacobo Torán and Florian Wörz. Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 60:1-60:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{toran_et_al:LIPIcs.STACS.2020.60,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{60:1--60:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.60},
  URN =		{urn:nbn:de:0030-drops-119213},
  doi =		{10.4230/LIPIcs.STACS.2020.60},
  annote =	{Keywords: Proof Complexity, Resolution, Tree-like Resolution, Pebble Game, Reversible Pebbling, Prover-Delayer Game, Raz - McKenzie Game, Clause Space, Variable Space}
}
Document
DOI: 10.4230/DagRep.8.9.133
Algebraic Methods in Computational Complexity (Dagstuhl Seminar 18391)

Authors: Markus Bläser, Valentine Kabanets, Jacobo Torán, and Christopher Umans

Published in: Dagstuhl Reports, Volume 8, Issue 9 (2019)

Abstract
Computational Complexity is concerned with the resources that are required for algorithms to detect properties of combinatorial objects and structures. It has often proven true that the best way to argue about these combinatorial objects is by establishing a connection (perhaps approximate) to a more well-behaved algebraic setting. Indeed, many of the deepest and most powerful results in Computational Complexity rely on algebraic proof techniques. The Razborov-Smolensky polynomial-approximation method for proving constant-depth circuit lower bounds, the PCP characterization of NP, and the Agrawal-Kayal-Saxena polynomial-time primality test are some of the most prominent examples. In some of the most exciting recent progress in Computational Complexity the algebraic theme still plays a central role. There have been significant recent advances in algebraic circuit lower bounds, and the so-called chasm at depth 4 suggests that the restricted models now being considered are not so far from ones that would lead to a general result. There have been similar successes concerning the related problems of polynomial identity testing and circuit reconstruction in the algebraic model (and these are tied to central questions regarding the power of randomness in computation). Also the areas of derandomization and coding theory have experimented important advances. The seminar aimed to capitalize on recent progress and bring together researchers who are using a diverse array of algebraic methods in a variety of settings. Researchers in these areas are relying on ever more sophisticated and specialized mathematics and the goal of the seminar was to play an important role in educating a diverse community about the latest new techniques.
Cite as

Markus Bläser, Valentine Kabanets, Jacobo Torán, and Christopher Umans. Algebraic Methods in Computational Complexity (Dagstuhl Seminar 18391). In Dagstuhl Reports, Volume 8, Issue 9, pp. 133-153, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{blaser_et_al:DagRep.8.9.133,
  author =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Tor\'{a}n, Jacobo and Umans, Christopher},
  title =	{{Algebraic Methods in Computational Complexity (Dagstuhl Seminar 18391)}},
  pages =	{133--153},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{8},
  number =	{9},
  editor =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Tor\'{a}n, Jacobo and Umans, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.9.133},
  URN =		{urn:nbn:de:0030-drops-103438},
  doi =		{10.4230/DagRep.8.9.133},
  annote =	{Keywords: computational complexity, algebra, (de-) randomization, circuits, coding, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2017.2
Finding Small Weight Isomorphisms with Additional Constraints is Fixed-Parameter Tractable

Authors: Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán

Published in: LIPIcs, Volume 89, 12th International Symposium on Parameterized and Exact Computation (IPEC 2017)

Abstract
Lubiw showed that several variants of Graph Isomorphism are NP-complete, where the solutions are required to satisfy certain additional constraints [SICOMP 10, 1981]. One of these, called Isomorphism With Restrictions, is to decide for two given graphs X_1=(V,E_1) and X_2=(V,E_2) and a subset R\subseteq V\times V of forbidden pairs whether there is an isomorphism \pi from X_1 to X_2 such that i^\pi\ne j for all (i,j)\in R. We prove that this problem and several of its generalizations are in fact in \FPT: - The problem of deciding whether there is an isomorphism between two graphs that moves k vertices and satisfies Lubiw-style constraints is in FPT, with k and the size of R as parameters. The problem remains in FPT even if a conjunction of disjunctions of such constraints is allowed. As a consequence of the main result it follows that the problem to decide whether there is an isomorphism that moves exactly k vertices is in FPT. This solves a question left open in our article on exact weight automorphisms [STACS 2017]. - When the number of moved vertices is unrestricted, finding isomorphisms that satisfy a CNF of Lubiw-style constraints can be solved in FPT with access to a GI oracle. - Checking if there is an isomorphism π between two graphs with complexity t is also in FPT with t as parameter, where the complexity of a permutation is the Cayley measure defined as the minimum number t such that \pi can be expressed as a product of t transpositions. - We consider a more general problem in which the vertex set of a graph X is partitioned into Red and Blue, and we are interested in an automorphism that stabilizes Red and Blue and moves exactly k vertices in Blue, where k is the parameter. This problem was introduced by [Downey and Fellows 1999], and we showed [STACS 2017] that it is W[1]-hard even with color classes of size 4 inside Red. Now, for color classes of size at most 3 inside Red, we show the problem is in FPT. In the non-parameterized setting, all these problems are NP-complete. Also, they all generalize in several ways the problem to decide whether there is an isomorphism between two graphs that moves at most k vertices, shown to be in FPT by Schweitzer [ESA 2011].
Cite as

Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán. Finding Small Weight Isomorphisms with Additional Constraints is Fixed-Parameter Tractable. In 12th International Symposium on Parameterized and Exact Computation (IPEC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 89, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{arvind_et_al:LIPIcs.IPEC.2017.2,
  author =	{Arvind, Vikraman and K\"{o}bler, Johannes and Kuhnert, Sebastian and Tor\'{a}n, Jacobo},
  title =	{{Finding Small Weight Isomorphisms with Additional Constraints is Fixed-Parameter Tractable}},
  booktitle =	{12th International Symposium on Parameterized and Exact Computation (IPEC 2017)},
  pages =	{2:1--2:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-051-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{89},
  editor =	{Lokshtanov, Daniel and Nishimura, Naomi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2017.2},
  URN =		{urn:nbn:de:0030-drops-85690},
  doi =		{10.4230/LIPIcs.IPEC.2017.2},
  annote =	{Keywords: parameterized algorithms, hypergraph isomorphism, mislabeled graphs}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.7
Parameterized Complexity of Small Weight Automorphisms

Authors: Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
We show that checking if a given hypergraph has an automorphism that moves exactly k vertices is fixed parameter tractable, using k and additionally either the maximum hyperedge size or the maximum color class size as parameters. In particular, it suffices to use k as parameter if the hyperedge size is at most polylogarithmic in the size of the given hypergraph. As a building block for our algorithms, we generalize Schweitzer's FPT algorithm [ESA 2011] that, given two graphs on the same vertex set and a parameter k, decides whether there is an isomorphism between the two graphs that moves at most k vertices. We extend this result to hypergraphs, using the maximum hyperedge size as a second parameter. Another key component of our algorithm is an orbit-shrinking technique that preserves permutations that move few points and that may be of independent interest. Applying it to a suitable subgroup of the automorphism group allows us to switch from bounded hyperedge size to bounded color classes in the exactly-k case.
Cite as

Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán. Parameterized Complexity of Small Weight Automorphisms. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 7:1-7:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{arvind_et_al:LIPIcs.STACS.2017.7,
  author =	{Arvind, Vikraman and K\"{o}bler, Johannes and Kuhnert, Sebastian and Tor\'{a}n, Jacobo},
  title =	{{Parameterized Complexity of Small Weight Automorphisms}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{7:1--7:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.7},
  URN =		{urn:nbn:de:0030-drops-70278},
  doi =		{10.4230/LIPIcs.STACS.2017.7},
  annote =	{Keywords: Parameterized algorithms, hypergraph isomorphism.}
}
Document
DOI: 10.4230/DagRep.6.10.13
Algebraic Methods in Computational Complexity (Dagstuhl Seminar 16411)

Authors: Valentine Kabanets, Thomas Thierauf, Jacobo Tóran, and Christopher Umans

Published in: Dagstuhl Reports, Volume 6, Issue 10 (2017)

Abstract
Computational Complexity is concerned with the resources that are required for algorithms to detect properties of combinatorial objects and structures. It has often proven true that the best way to argue about these combinatorial objects is by establishing a connection (perhaps approximate) to a more well-behaved algebraic setting. Indeed, many of the deepest and most powerful results in Computational Complexity rely on algebraic proof techniques. The Razborov-Smolensky polynomial-approximation method for proving constant-depth circuit lower bounds, the PCP characterization of NP, and the Agrawal-Kayal-Saxena polynomial-time primality test are some of the most prominent examples. The algebraic theme continues in some of the most exciting recent progress in computational complexity. There have been significant recent advances in algebraic circuit lower bounds, and the so-called chasm at depth 4 suggests that the restricted models now being considered are not so far from ones that would lead to a general result. There have been similar successes concerning the related problems of polynomial identity testing and circuit reconstruction in the algebraic model (and these are tied to central questions regarding the power of randomness in computation). Another surprising connection is that the algebraic techniques invented to show lower bounds now prove useful to develop efficient algorithms. For example, Williams showed how to use the polynomial method to obtain faster all-pair-shortest-path algorithms. This emphases once again the central role of algebra in computer science. The seminar aims to capitalize on recent progress and bring together researchers who are using a diverse array of algebraic methods in a variety of settings. Researchers in these areas are relying on ever more sophisticated and specialized mathematics and this seminar can play an important role in educating a diverse community about the latest new techniques, spurring further progress.
Cite as

Valentine Kabanets, Thomas Thierauf, Jacobo Tóran, and Christopher Umans. Algebraic Methods in Computational Complexity (Dagstuhl Seminar 16411). In Dagstuhl Reports, Volume 6, Issue 10, pp. 13-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{kabanets_et_al:DagRep.6.10.13,
  author =	{Kabanets, Valentine and Thierauf, Thomas and T\'{o}ran, Jacobo and Umans, Christopher},
  title =	{{Algebraic Methods in Computational Complexity (Dagstuhl Seminar 16411)}},
  pages =	{13--32},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{10},
  editor =	{Kabanets, Valentine and Thierauf, Thomas and T\'{o}ran, Jacobo and Umans, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.10.13},
  URN =		{urn:nbn:de:0030-drops-69504},
  doi =		{10.4230/DagRep.6.10.13},
  annote =	{Keywords: Computational Complexity, lower bounds, approximation, pseudo-randomness, derandomization, circuits}
}
Document
DOI: 10.4230/DagRep.5.12.1
The Graph Isomorphism Problem (Dagstuhl Seminar 15511)

Authors: László Babai, Anuj Dawar, Pascal Schweitzer, and Jacobo Torán

Published in: Dagstuhl Reports, Volume 5, Issue 12 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15511 "The Graph Isomorphism Problem". The goal of the seminar was to bring together researchers working on the numerous topics closely related to the Isomorphism Problem to foster their collaboration. To this end the participants of the seminar included researchers working on the theoretical and practical aspects of isomorphism ranging from the fields of algorithmic group theory, finite model theory, combinatorial optimization to algorithmics. A highlight of the conference was the presentation of a new quasi-polynomial time algorithm for the Graph Isomorphism Problem, providing the first improvement since 1983.
Cite as

László Babai, Anuj Dawar, Pascal Schweitzer, and Jacobo Torán. The Graph Isomorphism Problem (Dagstuhl Seminar 15511). In Dagstuhl Reports, Volume 5, Issue 12, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{babai_et_al:DagRep.5.12.1,
  author =	{Babai, L\'{a}szl\'{o} and Dawar, Anuj and Schweitzer, Pascal and Tor\'{a}n, Jacobo},
  title =	{{The Graph Isomorphism Problem (Dagstuhl Seminar 15511)}},
  pages =	{1--17},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{12},
  editor =	{Babai, L\'{a}szl\'{o} and Dawar, Anuj and Schweitzer, Pascal and Tor\'{a}n, Jacobo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.12.1},
  URN =		{urn:nbn:de:0030-drops-58028},
  doi =		{10.4230/DagRep.5.12.1},
  annote =	{Keywords: canonical forms, complexity, computational group theory, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.317
Graph Isomorphism is not AC^0 reducible to Group Isomorphism

Authors: Arkadev Chattopadhyay, Jacobo Torán, and Fabian Wagner

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
We give a new upper bound for the Group and Quasigroup Isomorphism problems when the input structures are given explicitly by multiplication tables. We show that these problems can be computed by polynomial size nondeterministic circuits of unbounded fan-in with $O(\log\log n)$ depth and $O(\log^2 n)$ nondeterministic bits, where $n$ is the number of group elements. This improves the existing upper bound from \cite{Wolf 94} for the problems. In the previous upper bound the circuits have bounded fan-in but depth $O(\log^2 n)$ and also $O(\log^2 n)$ nondeterministic bits. We then prove that the kind of circuits from our upper bound cannot compute the Parity function. Since Parity is AC0 reducible to Graph Isomorphism, this implies that Graph Isomorphism is strictly harder than Group or Quasigroup Isomorphism under the ordering defined by AC0 reductions.
Cite as

Arkadev Chattopadhyay, Jacobo Torán, and Fabian Wagner. Graph Isomorphism is not AC^0 reducible to Group Isomorphism. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 317-326, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.FSTTCS.2010.317,
  author =	{Chattopadhyay, Arkadev and Tor\'{a}n, Jacobo and Wagner, Fabian},
  title =	{{Graph Isomorphism is not AC^0 reducible to Group Isomorphism}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{317--326},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.317},
  URN =		{urn:nbn:de:0030-drops-28748},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.317},
  annote =	{Keywords: Complexity, Algorithms, Group Isomorphism Problem, Circuit Com plexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2457
Restricted Space Algorithms for Isomorphism on Bounded Treewidth Graphs

Authors: Bireswar Das, Jacobo Torán, and Fabian Wagner

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
The Graph Isomorphism problem restricted to graphs of bounded treewidth or bounded tree distance width are known to be solvable in polynomial time~\cite{Bo90},\cite{YBFT}.We give restricted space algorithms for these problems proving the following results: \begin{itemize} \item Isomorphism for bounded tree distance width graphs is in \Log\ and thus complete for the class. We also show that for this kind of graphs a canon can be computed within logspace. \item For bounded treewidth graphs, when both input graphs are given together with a tree decomposition, the problem of whether there is an isomorphism which respects the decompositions (i.e.\ considering only isomorphisms mapping bags in one decomposition blockwise onto bags in the other decomposition) is in \Log. \item For bounded treewidth graphs, when one of the input graphs is given with a tree decomposition the isomorphism problem is in \LogCFL. \item As a corollary the isomorphism problem for bounded treewidth graphs is in \LogCFL. This improves the known \TCone\ upper bound for the problem given by Grohe and Verbitsky~\cite{GV06}. \end{itemize}
Cite as

Bireswar Das, Jacobo Torán, and Fabian Wagner. Restricted Space Algorithms for Isomorphism on Bounded Treewidth Graphs. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 227-238, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.STACS.2010.2457,
  author =	{Das, Bireswar and Tor\'{a}n, Jacobo and Wagner, Fabian},
  title =	{{Restricted Space Algorithms for Isomorphism on Bounded Treewidth Graphs}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{227--238},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2457},
  URN =		{urn:nbn:de:0030-drops-24570},
  doi =		{10.4230/LIPIcs.STACS.2010.2457},
  annote =	{Keywords: Complexity, Algorithms, Graph Isomorphism Problem, Treewidth, LogCFL}
}
Document
DOI: 10.4230/DagSemProc.06451.3
A note on the size of Craig Interpolants

Authors: Uwe Schöning and Jacobo Torán

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)

Abstract
Mundici considered the question of whether the interpolant of two propositional formulas of the form $F ightarrow G$ can always have a short circuit description, and showed that if this is the case then every problem in NP $cap$ co-NP would have polynomial size circuits. In this note we observe further consequences of the interpolant having short circuit descriptions, namely that UP $subseteq$ P$/$poly, and that every single valued NP function has a total extension in FP$/$poly. We also relate this question with other Complexity Theory assumptions.
Cite as

Uwe Schöning and Jacobo Torán. A note on the size of Craig Interpolants. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{schoning_et_al:DagSemProc.06451.3,
  author =	{Sch\"{o}ning, Uwe and Tor\'{a}n, Jacobo},
  title =	{{A note on the size of Craig Interpolants}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.3},
  URN =		{urn:nbn:de:0030-drops-9735},
  doi =		{10.4230/DagSemProc.06451.3},
  annote =	{Keywords: Interpolant, non-uniform complexity}
}

Tóran, Jacobo

Document
DOI: 10.4230/LIPIcs.MFCS.2024.64
Pebble Games and Algebraic Proof Systems

Authors: Lisa-Marie Jaser and Jacobo Torán

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
Analyzing refutations of the well known pebbling formulas Peb(G) we prove some new strong connections between pebble games and algebraic proof system, showing that there is a parallelism between the reversible, black and black-white pebbling games on one side, and the three algebraic proof systems Nullstellensatz, Monomial Calculus and Polynomial Calculus on the other side. In particular we prove that for any DAG G with a single sink, if there is a Monomial Calculus refutation for Peb(G) having simultaneously degree s and size t then there is a black pebbling strategy on G with space s and time t+s. Also if there is a black pebbling strategy for G with space s and time t it is possible to extract from it a MC refutation for Peb(G) having simultaneously degree s and size ts. These results are analogous to those proven in [Susanna F. de Rezende et al., 2021] for the case of reversible pebbling and Nullstellensatz. Using them we prove degree separations between NS, MC and PC, as well as strong degree-size tradeoffs for MC. We also notice that for any directed acyclic graph G the space needed in a pebbling strategy on G, for the three versions of the game, reversible, black and black-white, exactly matches the variable space complexity of a refutation of the corresponding pebbling formula Peb(G) in each of the algebraic proof systems NS,MC and PC. Using known pebbling bounds on graphs, this connection implies separations between the corresponding variable space measures.
Cite as

Lisa-Marie Jaser and Jacobo Torán. Pebble Games and Algebraic Proof Systems. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 64:1-64:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jaser_et_al:LIPIcs.MFCS.2024.64,
  author =	{Jaser, Lisa-Marie and Tor\'{a}n, Jacobo},
  title =	{{Pebble Games and Algebraic Proof Systems}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{64:1--64:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.64},
  URN =		{urn:nbn:de:0030-drops-206200},
  doi =		{10.4230/LIPIcs.MFCS.2024.64},
  annote =	{Keywords: Proof Complexity, Algebraic Proof Systems, Pebble Games}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.26
Cutting Planes Width and the Complexity of Graph Isomorphism Refutations

Authors: Jacobo Torán and Florian Wörz

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

Abstract
The width complexity measure plays a central role in Resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most extended method for proving size lower bounds, and it is known that for these systems, proofs with small width also imply the existence of proofs with small size. Not much has been studied, however, about the width parameter in the Cutting Planes (CP) proof system, a measure that was introduced by Dantchev and Martin in 2011 under the name of CP cutwidth. In this paper, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs G and H, we show a direct connection between the Weisfeiler-Leman differentiation number WL(G, H) of the graphs and the width of a CP refutation for the corresponding isomorphism formula Iso(G, H). In particular, we show that if WL(G, H) ≤ k, then there is a CP refutation of Iso(G, H) with width k, and if WL(G, H) > k, then there are no CP refutations of Iso(G, H) with width k-2. Similar results are known for other proof systems, like Resolution, Sherali-Adams, or Polynomial Calculus. We also obtain polynomial-size CP refutations from our width bound for isomorphism formulas for graphs with constant WL-dimension.
Cite as

Jacobo Torán and Florian Wörz. Cutting Planes Width and the Complexity of Graph Isomorphism Refutations. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{toran_et_al:LIPIcs.SAT.2023.26,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Cutting Planes Width and the Complexity of Graph Isomorphism Refutations}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{26:1--26:20},
  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.26},
  URN =		{urn:nbn:de:0030-drops-184884},
  doi =		{10.4230/LIPIcs.SAT.2023.26},
  annote =	{Keywords: Cutting Planes, Proof Complexity, Linear Programming, Combinatorial Optimization, Weisfeiler-Leman Algorithm, Graph Isomorphism}
}
Document
DOI: 10.4230/DagRep.12.9.41
Algebraic and Analytic Methods in Computational Complexity (Dagstuhl Seminar 22371)

Authors: Markus Bläser, Valentine Kabanets, Ronen Shaltiel, and Jacobo Torán

Published in: Dagstuhl Reports, Volume 12, Issue 9 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 2237 "Algebraic and Analytic Methods in Computational Complexity". Computational Complexity is concerned with the resources that are required for algorithms to detect properties of combinatorial objects and structures. It has often proven true that the best way to argue about these combinatorial objects is by establishing a connection (perhaps approximate) to a more well-behaved algebraic setting. Beside algebraic methods, analytic methods have been used for quite some time in theoretical computer science. These methods can also be used to solve algebraic problems as show by many recent examples in the areas of derandomization, coding theory or circuit lower bounds. These new directions were in the focus of the Dagstuhl Seminar and reflect the developments in the field since the previous Dagstuhl Seminar 18391. This Dagstuhl Seminar brought together researchers who are using a diverse array of algebraic and analytic methods in a variety of settings. Researchers in these areas are relying on ever more sophisticated and specialized mathematics and this seminar played a role in educating a diverse community about the latest new techniques, spurring further progress.
Cite as

Markus Bläser, Valentine Kabanets, Ronen Shaltiel, and Jacobo Torán. Algebraic and Analytic Methods in Computational Complexity (Dagstuhl Seminar 22371). In Dagstuhl Reports, Volume 12, Issue 9, pp. 41-59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{blaser_et_al:DagRep.12.9.41,
  author =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Shaltiel, Ronen and Tor\'{a}n, Jacobo},
  title =	{{Algebraic and Analytic Methods in Computational Complexity (Dagstuhl Seminar 22371)}},
  pages =	{41--59},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{9},
  editor =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Shaltiel, Ronen and Tor\'{a}n, Jacobo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.9.41},
  URN =		{urn:nbn:de:0030-drops-178092},
  doi =		{10.4230/DagRep.12.9.41},
  annote =	{Keywords: (de-)randomization, algebra, circuits, coding, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.36
Number of Variables for Graph Differentiation and the Resolution of GI Formulas

Authors: Jacobo Torán and Florian Wörz

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and positive depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution. Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular, we show that if k is the number of variables needed to distinguish two graphs with n vertices each, then there is an n^O(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2^(k-1) and k for the tree-like resolution size and resolution clause space for this formula. We also show a (normal) resolution size lower bound of exp(Ω(k²/n)) for the case of colored graphs with constant color class sizes. Applying these results, we prove the first exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule, thereby answering an open question posed by Schweitzer and Seebach.
Cite as

Jacobo Torán and Florian Wörz. Number of Variables for Graph Differentiation and the Resolution of GI Formulas. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{toran_et_al:LIPIcs.CSL.2022.36,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Number of Variables for Graph Differentiation and the Resolution of GI Formulas}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.36},
  URN =		{urn:nbn:de:0030-drops-157564},
  doi =		{10.4230/LIPIcs.CSL.2022.36},
  annote =	{Keywords: Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, k-variable fragment first-order logic 𝔏\underlinek, Immerman’s Pebble Game, Symmetry Rule, SRC-1}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.60
Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space

Authors: Jacobo Torán and Florian Wörz

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
We show a new connection between the space measure in tree-like resolution and the reversible pebble game in graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the space complexity measure in tree-like and general resolution. We show that these separations are not far from optimal by proving upper bounds for tree-like resolution space in terms of general resolution clause and variable space. In particular we show that for any formula F, its tree-like resolution space is upper bounded by space(π)log(time(π)), where π is any general resolution refutation of F. This holds considering as space(π) the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas, we are able to improve this bound to the optimal bound space(π)log n, where n is the number of vertices of the corresponding graph.
Cite as

Jacobo Torán and Florian Wörz. Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 60:1-60:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{toran_et_al:LIPIcs.STACS.2020.60,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Reversible Pebble Games and the Relation Between Tree-Like and General Resolution Space}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{60:1--60:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.60},
  URN =		{urn:nbn:de:0030-drops-119213},
  doi =		{10.4230/LIPIcs.STACS.2020.60},
  annote =	{Keywords: Proof Complexity, Resolution, Tree-like Resolution, Pebble Game, Reversible Pebbling, Prover-Delayer Game, Raz - McKenzie Game, Clause Space, Variable Space}
}
Document
DOI: 10.4230/DagRep.8.9.133
Algebraic Methods in Computational Complexity (Dagstuhl Seminar 18391)

Authors: Markus Bläser, Valentine Kabanets, Jacobo Torán, and Christopher Umans

Published in: Dagstuhl Reports, Volume 8, Issue 9 (2019)

Abstract
Computational Complexity is concerned with the resources that are required for algorithms to detect properties of combinatorial objects and structures. It has often proven true that the best way to argue about these combinatorial objects is by establishing a connection (perhaps approximate) to a more well-behaved algebraic setting. Indeed, many of the deepest and most powerful results in Computational Complexity rely on algebraic proof techniques. The Razborov-Smolensky polynomial-approximation method for proving constant-depth circuit lower bounds, the PCP characterization of NP, and the Agrawal-Kayal-Saxena polynomial-time primality test are some of the most prominent examples. In some of the most exciting recent progress in Computational Complexity the algebraic theme still plays a central role. There have been significant recent advances in algebraic circuit lower bounds, and the so-called chasm at depth 4 suggests that the restricted models now being considered are not so far from ones that would lead to a general result. There have been similar successes concerning the related problems of polynomial identity testing and circuit reconstruction in the algebraic model (and these are tied to central questions regarding the power of randomness in computation). Also the areas of derandomization and coding theory have experimented important advances. The seminar aimed to capitalize on recent progress and bring together researchers who are using a diverse array of algebraic methods in a variety of settings. Researchers in these areas are relying on ever more sophisticated and specialized mathematics and the goal of the seminar was to play an important role in educating a diverse community about the latest new techniques.
Cite as

Markus Bläser, Valentine Kabanets, Jacobo Torán, and Christopher Umans. Algebraic Methods in Computational Complexity (Dagstuhl Seminar 18391). In Dagstuhl Reports, Volume 8, Issue 9, pp. 133-153, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{blaser_et_al:DagRep.8.9.133,
  author =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Tor\'{a}n, Jacobo and Umans, Christopher},
  title =	{{Algebraic Methods in Computational Complexity (Dagstuhl Seminar 18391)}},
  pages =	{133--153},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{8},
  number =	{9},
  editor =	{Bl\"{a}ser, Markus and Kabanets, Valentine and Tor\'{a}n, Jacobo and Umans, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.9.133},
  URN =		{urn:nbn:de:0030-drops-103438},
  doi =		{10.4230/DagRep.8.9.133},
  annote =	{Keywords: computational complexity, algebra, (de-) randomization, circuits, coding, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2017.2
Finding Small Weight Isomorphisms with Additional Constraints is Fixed-Parameter Tractable

Authors: Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán

Published in: LIPIcs, Volume 89, 12th International Symposium on Parameterized and Exact Computation (IPEC 2017)

Abstract
Lubiw showed that several variants of Graph Isomorphism are NP-complete, where the solutions are required to satisfy certain additional constraints [SICOMP 10, 1981]. One of these, called Isomorphism With Restrictions, is to decide for two given graphs X_1=(V,E_1) and X_2=(V,E_2) and a subset R\subseteq V\times V of forbidden pairs whether there is an isomorphism \pi from X_1 to X_2 such that i^\pi\ne j for all (i,j)\in R. We prove that this problem and several of its generalizations are in fact in \FPT: - The problem of deciding whether there is an isomorphism between two graphs that moves k vertices and satisfies Lubiw-style constraints is in FPT, with k and the size of R as parameters. The problem remains in FPT even if a conjunction of disjunctions of such constraints is allowed. As a consequence of the main result it follows that the problem to decide whether there is an isomorphism that moves exactly k vertices is in FPT. This solves a question left open in our article on exact weight automorphisms [STACS 2017]. - When the number of moved vertices is unrestricted, finding isomorphisms that satisfy a CNF of Lubiw-style constraints can be solved in FPT with access to a GI oracle. - Checking if there is an isomorphism π between two graphs with complexity t is also in FPT with t as parameter, where the complexity of a permutation is the Cayley measure defined as the minimum number t such that \pi can be expressed as a product of t transpositions. - We consider a more general problem in which the vertex set of a graph X is partitioned into Red and Blue, and we are interested in an automorphism that stabilizes Red and Blue and moves exactly k vertices in Blue, where k is the parameter. This problem was introduced by [Downey and Fellows 1999], and we showed [STACS 2017] that it is W[1]-hard even with color classes of size 4 inside Red. Now, for color classes of size at most 3 inside Red, we show the problem is in FPT. In the non-parameterized setting, all these problems are NP-complete. Also, they all generalize in several ways the problem to decide whether there is an isomorphism between two graphs that moves at most k vertices, shown to be in FPT by Schweitzer [ESA 2011].
Cite as

Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán. Finding Small Weight Isomorphisms with Additional Constraints is Fixed-Parameter Tractable. In 12th International Symposium on Parameterized and Exact Computation (IPEC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 89, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{arvind_et_al:LIPIcs.IPEC.2017.2,
  author =	{Arvind, Vikraman and K\"{o}bler, Johannes and Kuhnert, Sebastian and Tor\'{a}n, Jacobo},
  title =	{{Finding Small Weight Isomorphisms with Additional Constraints is Fixed-Parameter Tractable}},
  booktitle =	{12th International Symposium on Parameterized and Exact Computation (IPEC 2017)},
  pages =	{2:1--2:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-051-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{89},
  editor =	{Lokshtanov, Daniel and Nishimura, Naomi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2017.2},
  URN =		{urn:nbn:de:0030-drops-85690},
  doi =		{10.4230/LIPIcs.IPEC.2017.2},
  annote =	{Keywords: parameterized algorithms, hypergraph isomorphism, mislabeled graphs}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.7
Parameterized Complexity of Small Weight Automorphisms

Authors: Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
We show that checking if a given hypergraph has an automorphism that moves exactly k vertices is fixed parameter tractable, using k and additionally either the maximum hyperedge size or the maximum color class size as parameters. In particular, it suffices to use k as parameter if the hyperedge size is at most polylogarithmic in the size of the given hypergraph. As a building block for our algorithms, we generalize Schweitzer's FPT algorithm [ESA 2011] that, given two graphs on the same vertex set and a parameter k, decides whether there is an isomorphism between the two graphs that moves at most k vertices. We extend this result to hypergraphs, using the maximum hyperedge size as a second parameter. Another key component of our algorithm is an orbit-shrinking technique that preserves permutations that move few points and that may be of independent interest. Applying it to a suitable subgroup of the automorphism group allows us to switch from bounded hyperedge size to bounded color classes in the exactly-k case.
Cite as

Vikraman Arvind, Johannes Köbler, Sebastian Kuhnert, and Jacobo Torán. Parameterized Complexity of Small Weight Automorphisms. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 7:1-7:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{arvind_et_al:LIPIcs.STACS.2017.7,
  author =	{Arvind, Vikraman and K\"{o}bler, Johannes and Kuhnert, Sebastian and Tor\'{a}n, Jacobo},
  title =	{{Parameterized Complexity of Small Weight Automorphisms}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{7:1--7:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.7},
  URN =		{urn:nbn:de:0030-drops-70278},
  doi =		{10.4230/LIPIcs.STACS.2017.7},
  annote =	{Keywords: Parameterized algorithms, hypergraph isomorphism.}
}
Document
DOI: 10.4230/DagRep.6.10.13
Algebraic Methods in Computational Complexity (Dagstuhl Seminar 16411)

Authors: Valentine Kabanets, Thomas Thierauf, Jacobo Tóran, and Christopher Umans

Published in: Dagstuhl Reports, Volume 6, Issue 10 (2017)

Abstract
Computational Complexity is concerned with the resources that are required for algorithms to detect properties of combinatorial objects and structures. It has often proven true that the best way to argue about these combinatorial objects is by establishing a connection (perhaps approximate) to a more well-behaved algebraic setting. Indeed, many of the deepest and most powerful results in Computational Complexity rely on algebraic proof techniques. The Razborov-Smolensky polynomial-approximation method for proving constant-depth circuit lower bounds, the PCP characterization of NP, and the Agrawal-Kayal-Saxena polynomial-time primality test are some of the most prominent examples. The algebraic theme continues in some of the most exciting recent progress in computational complexity. There have been significant recent advances in algebraic circuit lower bounds, and the so-called chasm at depth 4 suggests that the restricted models now being considered are not so far from ones that would lead to a general result. There have been similar successes concerning the related problems of polynomial identity testing and circuit reconstruction in the algebraic model (and these are tied to central questions regarding the power of randomness in computation). Another surprising connection is that the algebraic techniques invented to show lower bounds now prove useful to develop efficient algorithms. For example, Williams showed how to use the polynomial method to obtain faster all-pair-shortest-path algorithms. This emphases once again the central role of algebra in computer science. The seminar aims to capitalize on recent progress and bring together researchers who are using a diverse array of algebraic methods in a variety of settings. Researchers in these areas are relying on ever more sophisticated and specialized mathematics and this seminar can play an important role in educating a diverse community about the latest new techniques, spurring further progress.
Cite as

Valentine Kabanets, Thomas Thierauf, Jacobo Tóran, and Christopher Umans. Algebraic Methods in Computational Complexity (Dagstuhl Seminar 16411). In Dagstuhl Reports, Volume 6, Issue 10, pp. 13-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{kabanets_et_al:DagRep.6.10.13,
  author =	{Kabanets, Valentine and Thierauf, Thomas and T\'{o}ran, Jacobo and Umans, Christopher},
  title =	{{Algebraic Methods in Computational Complexity (Dagstuhl Seminar 16411)}},
  pages =	{13--32},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{10},
  editor =	{Kabanets, Valentine and Thierauf, Thomas and T\'{o}ran, Jacobo and Umans, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.10.13},
  URN =		{urn:nbn:de:0030-drops-69504},
  doi =		{10.4230/DagRep.6.10.13},
  annote =	{Keywords: Computational Complexity, lower bounds, approximation, pseudo-randomness, derandomization, circuits}
}
Document
DOI: 10.4230/DagRep.5.12.1
The Graph Isomorphism Problem (Dagstuhl Seminar 15511)

Authors: László Babai, Anuj Dawar, Pascal Schweitzer, and Jacobo Torán

Published in: Dagstuhl Reports, Volume 5, Issue 12 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15511 "The Graph Isomorphism Problem". The goal of the seminar was to bring together researchers working on the numerous topics closely related to the Isomorphism Problem to foster their collaboration. To this end the participants of the seminar included researchers working on the theoretical and practical aspects of isomorphism ranging from the fields of algorithmic group theory, finite model theory, combinatorial optimization to algorithmics. A highlight of the conference was the presentation of a new quasi-polynomial time algorithm for the Graph Isomorphism Problem, providing the first improvement since 1983.
Cite as

László Babai, Anuj Dawar, Pascal Schweitzer, and Jacobo Torán. The Graph Isomorphism Problem (Dagstuhl Seminar 15511). In Dagstuhl Reports, Volume 5, Issue 12, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{babai_et_al:DagRep.5.12.1,
  author =	{Babai, L\'{a}szl\'{o} and Dawar, Anuj and Schweitzer, Pascal and Tor\'{a}n, Jacobo},
  title =	{{The Graph Isomorphism Problem (Dagstuhl Seminar 15511)}},
  pages =	{1--17},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{12},
  editor =	{Babai, L\'{a}szl\'{o} and Dawar, Anuj and Schweitzer, Pascal and Tor\'{a}n, Jacobo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.12.1},
  URN =		{urn:nbn:de:0030-drops-58028},
  doi =		{10.4230/DagRep.5.12.1},
  annote =	{Keywords: canonical forms, complexity, computational group theory, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.317
Graph Isomorphism is not AC^0 reducible to Group Isomorphism

Authors: Arkadev Chattopadhyay, Jacobo Torán, and Fabian Wagner

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
We give a new upper bound for the Group and Quasigroup Isomorphism problems when the input structures are given explicitly by multiplication tables. We show that these problems can be computed by polynomial size nondeterministic circuits of unbounded fan-in with $O(\log\log n)$ depth and $O(\log^2 n)$ nondeterministic bits, where $n$ is the number of group elements. This improves the existing upper bound from \cite{Wolf 94} for the problems. In the previous upper bound the circuits have bounded fan-in but depth $O(\log^2 n)$ and also $O(\log^2 n)$ nondeterministic bits. We then prove that the kind of circuits from our upper bound cannot compute the Parity function. Since Parity is AC0 reducible to Graph Isomorphism, this implies that Graph Isomorphism is strictly harder than Group or Quasigroup Isomorphism under the ordering defined by AC0 reductions.
Cite as

Arkadev Chattopadhyay, Jacobo Torán, and Fabian Wagner. Graph Isomorphism is not AC^0 reducible to Group Isomorphism. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 317-326, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.FSTTCS.2010.317,
  author =	{Chattopadhyay, Arkadev and Tor\'{a}n, Jacobo and Wagner, Fabian},
  title =	{{Graph Isomorphism is not AC^0 reducible to Group Isomorphism}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{317--326},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.317},
  URN =		{urn:nbn:de:0030-drops-28748},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.317},
  annote =	{Keywords: Complexity, Algorithms, Group Isomorphism Problem, Circuit Com plexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2457
Restricted Space Algorithms for Isomorphism on Bounded Treewidth Graphs

Authors: Bireswar Das, Jacobo Torán, and Fabian Wagner

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
The Graph Isomorphism problem restricted to graphs of bounded treewidth or bounded tree distance width are known to be solvable in polynomial time~\cite{Bo90},\cite{YBFT}.We give restricted space algorithms for these problems proving the following results: \begin{itemize} \item Isomorphism for bounded tree distance width graphs is in \Log\ and thus complete for the class. We also show that for this kind of graphs a canon can be computed within logspace. \item For bounded treewidth graphs, when both input graphs are given together with a tree decomposition, the problem of whether there is an isomorphism which respects the decompositions (i.e.\ considering only isomorphisms mapping bags in one decomposition blockwise onto bags in the other decomposition) is in \Log. \item For bounded treewidth graphs, when one of the input graphs is given with a tree decomposition the isomorphism problem is in \LogCFL. \item As a corollary the isomorphism problem for bounded treewidth graphs is in \LogCFL. This improves the known \TCone\ upper bound for the problem given by Grohe and Verbitsky~\cite{GV06}. \end{itemize}
Cite as

Bireswar Das, Jacobo Torán, and Fabian Wagner. Restricted Space Algorithms for Isomorphism on Bounded Treewidth Graphs. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 227-238, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.STACS.2010.2457,
  author =	{Das, Bireswar and Tor\'{a}n, Jacobo and Wagner, Fabian},
  title =	{{Restricted Space Algorithms for Isomorphism on Bounded Treewidth Graphs}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{227--238},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2457},
  URN =		{urn:nbn:de:0030-drops-24570},
  doi =		{10.4230/LIPIcs.STACS.2010.2457},
  annote =	{Keywords: Complexity, Algorithms, Graph Isomorphism Problem, Treewidth, LogCFL}
}
Document
DOI: 10.4230/DagSemProc.06451.3
A note on the size of Craig Interpolants

Authors: Uwe Schöning and Jacobo Torán

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)

Abstract
Mundici considered the question of whether the interpolant of two propositional formulas of the form $F ightarrow G$ can always have a short circuit description, and showed that if this is the case then every problem in NP $cap$ co-NP would have polynomial size circuits. In this note we observe further consequences of the interpolant having short circuit descriptions, namely that UP $subseteq$ P$/$poly, and that every single valued NP function has a total extension in FP$/$poly. We also relate this question with other Complexity Theory assumptions.
Cite as

Uwe Schöning and Jacobo Torán. A note on the size of Craig Interpolants. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{schoning_et_al:DagSemProc.06451.3,
  author =	{Sch\"{o}ning, Uwe and Tor\'{a}n, Jacobo},
  title =	{{A note on the size of Craig Interpolants}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.3},
  URN =		{urn:nbn:de:0030-drops-9735},
  doi =		{10.4230/DagSemProc.06451.3},
  annote =	{Keywords: Interpolant, non-uniform complexity}
}
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