28 Search Results for "Atserias, Albert"


Document
Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051)

Authors: Albert Atserias, Christoph Berkholz, Kousha Etessami, and Joanna Ochremiak

Published in: Dagstuhl Reports, Volume 12, Issue 1 (2022)


Abstract
Finite and algorithmic model theory (FAMT) studies the expressive power of logical languages on finite structures or, more generally, structures that can be finitely presented. These are the structures that serve as input to computation, and for this reason the study of FAMT is intimately connected with computer science. Over the last four decades, the subject has developed through a close interaction between theoretical computer science and related areas of mathematics, including logic and combinatorics. This report documents the program and the outcomes of Dagstuhl Seminar 22051 "Finite and Algorithmic Model Theory".

Cite as

Albert Atserias, Christoph Berkholz, Kousha Etessami, and Joanna Ochremiak. Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051). In Dagstuhl Reports, Volume 12, Issue 1, pp. 101-118, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{atserias_et_al:DagRep.12.1.101,
  author =	{Atserias, Albert and Berkholz, Christoph and Etessami, Kousha and Ochremiak, Joanna},
  title =	{{Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051)}},
  pages =	{101--118},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{1},
  editor =	{Atserias, Albert and Berkholz, Christoph and Etessami, Kousha and Ochremiak, Joanna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.1.101},
  URN =		{urn:nbn:de:0030-drops-169232},
  doi =		{10.4230/DagRep.12.1.101},
  annote =	{Keywords: automata and game theory, database theory, descriptive complexity, finite model theory, homomorphism counts, Query enumeration}
}
Document
On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares

Authors: Ilario Bonacina, Nicola Galesi, and Massimo Lauria

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)


Abstract
Vanishing sums of roots of unity can be seen as a natural generalization of knapsack from Boolean variables to variables taking values over the roots of unity. We show that these sums are hard to prove for polynomial calculus and for sum-of-squares, both in terms of degree and size.

Cite as

Ilario Bonacina, Nicola Galesi, and Massimo Lauria. On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 23:1-23:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.MFCS.2022.23,
  author =	{Bonacina, Ilario and Galesi, Nicola and Lauria, Massimo},
  title =	{{On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{23:1--23:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.23},
  URN =		{urn:nbn:de:0030-drops-168211},
  doi =		{10.4230/LIPIcs.MFCS.2022.23},
  annote =	{Keywords: polynomial calculus, sum-of-squares, roots of unity, knapsack}
}
Document
Automating OBDD proofs is NP-hard

Authors: Dmitry Itsykson and Artur Riazanov

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)


Abstract
We prove that the proof system OBDD(∧, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of [Albert Atserias and Moritz Müller, 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n+1 participants was proved by [Göös et al., 2020] to establish the hardness of automatability result for Cutting Planes.

Cite as

Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 59:1-59:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.MFCS.2022.59,
  author =	{Itsykson, Dmitry and Riazanov, Artur},
  title =	{{Automating OBDD proofs is NP-hard}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{59:1--59:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.59},
  URN =		{urn:nbn:de:0030-drops-168575},
  doi =		{10.4230/LIPIcs.MFCS.2022.59},
  annote =	{Keywords: proof complexity, OBDD, automatability, lifting, dag-like communication}
}
Document
Invited Talk
Towards a Theory of Algorithmic Proof Complexity (Invited Talk)

Authors: Albert Atserias

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
A possibly unexpected by-product of the mathematical study of the lengths of proofs, as is done in the field of propositional proof complexity, is, I claim, that it may lead to new polynomial-time algorithms. To explain this, I will first recall the origins of proof complexity as a field, and then explain why some of the recent progress in it could lead to some new algorithms.

Cite as

Albert Atserias. Towards a Theory of Algorithmic Proof Complexity (Invited Talk). In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 1:1-1:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{atserias:LIPIcs.ICALP.2022.1,
  author =	{Atserias, Albert},
  title =	{{Towards a Theory of Algorithmic Proof Complexity}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.1},
  URN =		{urn:nbn:de:0030-drops-163423},
  doi =		{10.4230/LIPIcs.ICALP.2022.1},
  annote =	{Keywords: proof complexity, logic, computational complexity}
}
Document
Track A: Algorithms, Complexity and Games
A Study of Weisfeiler-Leman Colorings on Planar Graphs

Authors: Sandra Kiefer and Daniel Neuen

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
The Weisfeiler-Leman (WL) algorithm is a combinatorial procedure that computes colorings on graphs, which can often be used to detect their (non-)isomorphism. Particularly the 1- and 2-dimensional versions 1-WL and 2-WL have received much attention, due to their numerous links to other areas of computer science. Knowing the expressive power of a certain dimension of the algorithm usually amounts to understanding the computed colorings. An increase in the dimension leads to finer computed colorings and, thus, more graphs can be distinguished. For example, on the class of planar graphs, 3-WL solves the isomorphism problem. However, the expressive power of 2-WL on the class is poorly understood (and, in particular, it may even well be that it decides isomorphism). In this paper, we investigate the colorings computed by 2-WL on planar graphs. Towards this end, we analyze the graphs induced by edge color classes in the graph. Based on the obtained classification, we show that for every 3-connected planar graph, it holds that: a) after coloring all pairs with their 2-WL color, the graph has fixing number 1 with respect to 1-WL, or b) there is a 2-WL-definable matching that can be used to transform the graph into a smaller one, or c) 2-WL detects a connected subgraph that is essentially the graph of a Platonic or Archimedean solid, a prism, a cycle, or a bipartite graph K_{2,𝓁}. In particular, the graphs from case (a) are identified by 2-WL.

Cite as

Sandra Kiefer and Daniel Neuen. A Study of Weisfeiler-Leman Colorings on Planar Graphs. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 81:1-81:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.ICALP.2022.81,
  author =	{Kiefer, Sandra and Neuen, Daniel},
  title =	{{A Study of Weisfeiler-Leman Colorings on Planar Graphs}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{81:1--81:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.81},
  URN =		{urn:nbn:de:0030-drops-164228},
  doi =		{10.4230/LIPIcs.ICALP.2022.81},
  annote =	{Keywords: Weisfeiler-Leman algorithm, planar graphs, edge-transitive graphs, fixing number}
}
Document
Lower Bounds for Symmetric Circuits for the Determinant

Authors: Anuj Dawar and Gregory Wilsenach

Published in: LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)


Abstract
Dawar and Wilsenach (ICALP 2020) introduce the model of symmetric arithmetic circuits and show an exponential separation between the sizes of symmetric circuits for computing the determinant and the permanent. The symmetry restriction is that the circuits which take a matrix input are unchanged by a permutation applied simultaneously to the rows and columns of the matrix. Under such restrictions we have polynomial-size circuits for computing the determinant but no subexponential size circuits for the permanent. Here, we consider a more stringent symmetry requirement, namely that the circuits are unchanged by arbitrary even permutations applied separately to rows and columns, and prove an exponential lower bound even for circuits computing the determinant. The result requires substantial new machinery. We develop a general framework for proving lower bounds for symmetric circuits with restricted symmetries, based on a new support theorem and new two-player restricted bijection games. These are applied to the determinant problem with a novel construction of matrices that are bi-adjacency matrices of graphs based on the CFI construction. Our general framework opens the way to exploring a variety of symmetry restrictions and studying trade-offs between symmetry and other resources used by arithmetic circuits.

Cite as

Anuj Dawar and Gregory Wilsenach. Lower Bounds for Symmetric Circuits for the Determinant. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 52:1-52:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.ITCS.2022.52,
  author =	{Dawar, Anuj and Wilsenach, Gregory},
  title =	{{Lower Bounds for Symmetric Circuits for the Determinant}},
  booktitle =	{13th Innovations in Theoretical Computer Science Conference (ITCS 2022)},
  pages =	{52:1--52:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-217-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{215},
  editor =	{Braverman, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.52},
  URN =		{urn:nbn:de:0030-drops-156480},
  doi =		{10.4230/LIPIcs.ITCS.2022.52},
  annote =	{Keywords: arithmetic circuits, symmetric arithmetic circuits, Boolean circuits, symmetric circuits, permanent, determinant, counting width, Weisfeiler-Leman dimension, Cai-F\"{u}rer-Immerman constructions}
}
Document
On the Power and Limitations of Branch and Cut

Authors: Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)


Abstract
The Stabbing Planes proof system [Paul Beame et al., 2018] was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas - certain unsatisfiable systems of linear equations od 2 - which are canonical hard examples for many algebraic proof systems. In a recent (and surprising) result, Dadush and Tiwari [Daniel Dadush and Samarth Tiwari, 2020] showed that these short refutations of the Tseitin formulas could be translated into quasi-polynomial size and depth Cutting Planes proofs, refuting a long-standing conjecture. This translation raises several interesting questions. First, whether all Stabbing Planes proofs can be efficiently simulated by Cutting Planes. This would allow for the substantial analysis done on the Cutting Planes system to be lifted to practical mixed integer programming solvers. Second, whether the quasi-polynomial depth of these proofs is inherent to Cutting Planes. In this paper we make progress towards answering both of these questions. First, we show that any Stabbing Planes proof with bounded coefficients (SP*) can be translated into Cutting Planes. As a consequence of the known lower bounds for Cutting Planes, this establishes the first exponential lower bounds on SP*. Using this translation, we extend the result of Dadush and Tiwari to show that Cutting Planes has short refutations of any unsatisfiable system of linear equations over a finite field. Like the Cutting Planes proofs of Dadush and Tiwari, our refutations also incur a quasi-polynomial blow-up in depth, and we conjecture that this is inherent. As a step towards this conjecture, we develop a new geometric technique for proving lower bounds on the depth of Cutting Planes proofs. This allows us to establish the first lower bounds on the depth of Semantic Cutting Planes proofs of the Tseitin formulas.

Cite as

Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the Power and Limitations of Branch and Cut. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 6:1-6:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.CCC.2021.6,
  author =	{Fleming, Noah and G\"{o}\"{o}s, Mika and Impagliazzo, Russell and Pitassi, Toniann and Robere, Robert and Tan, Li-Yang and Wigderson, Avi},
  title =	{{On the Power and Limitations of Branch and Cut}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{6:1--6:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.6},
  URN =		{urn:nbn:de:0030-drops-142809},
  doi =		{10.4230/LIPIcs.CCC.2021.6},
  annote =	{Keywords: Proof Complexity, Integer Programming, Cutting Planes, Branch and Cut, Stabbing Planes}
}
Document
Branching Programs with Bounded Repetitions and Flow Formulas

Authors: Anastasia Sofronova and Dmitry Sokolov

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)


Abstract
Restricted branching programs capture various complexity measures like space in Turing machines or length of proofs in proof systems. In this paper, we focus on the application in the proof complexity that was discovered by Lovasz et al. [László Lovász et al., 1995] who showed the equivalence between regular Resolution and read-once branching programs for "unsatisfied clause search problem" (Search_φ). This connection is widely used, in particular, in the recent breakthrough result about the Clique problem in regular Resolution by Atserias et al. [Albert Atserias et al., 2018]. We study the branching programs with bounded repetitions, so-called (1,+k)-BPs (Sieling [Detlef Sieling, 1996]) in application to the Search_φ problem. On the one hand, it is a natural generalization of read-once branching programs. On the other hand, this model gives a powerful proof system that can efficiently certify the unsatisfiability of a wide class of formulas that is hard for Resolution (Knop [Alexander Knop, 2017]). We deal with Search_φ that is "relatively easy" compared to all known hard examples for the (1,+k)-BPs. We introduce the first technique for proving exponential lower bounds for the (1,+k)-BPs on Search_φ. To do it we combine a well-known technique for proving lower bounds on the size of branching programs [Detlef Sieling, 1996; Detlef Sieling and Ingo Wegener, 1994; Stasys Jukna and Alexander A. Razborov, 1998] with the modification of the "closure" technique [Michael Alekhnovich et al., 2004; Michael Alekhnovich and Alexander A. Razborov, 2003]. In contrast with most Resolution lower bounds, our technique uses not only "local" properties of the formula, but also a "global" structure. Our hard examples are based on the Flow formulas introduced in [Michael Alekhnovich and Alexander A. Razborov, 2003].

Cite as

Anastasia Sofronova and Dmitry Sokolov. Branching Programs with Bounded Repetitions and Flow Formulas. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 17:1-17:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{sofronova_et_al:LIPIcs.CCC.2021.17,
  author =	{Sofronova, Anastasia and Sokolov, Dmitry},
  title =	{{Branching Programs with Bounded Repetitions and Flow Formulas}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{17:1--17:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.17},
  URN =		{urn:nbn:de:0030-drops-142915},
  doi =		{10.4230/LIPIcs.CCC.2021.17},
  annote =	{Keywords: proof complexity, branching programs, bounded repetitions, lower bounds}
}
Document
Invited Talk
Proofs of Soundness and Proof Search (Invited Talk)

Authors: Albert Atserias

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)


Abstract
Let P be a sound proof system for propositional logic. For each CNF formula F, let SAT(F) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with those of F (e.g., F itself). For each integer s, let REF(F,s) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with the P-refutations of F of length s. Since P is sound, it is obvious that the conjunction formula SAT(F) & REF(F,s) is unsatisfiable for any choice of F and s. It has been long known that, for many natural proof systems P and for the most natural formalizations of the formulas SAT and REF, the unsatisfiability of SAT(F) & REF(F,s) can be established by a short refutation. In addition, for many P, these short refutations live in the proof system P itself. This is the case for all Frege proof systems. In contrast it was known since the early 2000’s that Resolution proofs of Resolution’s soundness statements must have superpolynomial length. In this talk I will explain how the soundness formulas for a proof system P relate to the computational complexity of the proof search problem for P. In particular, I will explain how such formulas are used in the recent proof that the problem of approximating the minimum proof-length for Resolution is NP-hard (Atserias-Müller 2019). Besides playing a key role in this hardness of approximation result, the renewed interest in the soundness formulas led to a complete answer to the question whether Resolution has subexponential-length proofs of its own soundness statements (Garlík 2019).

Cite as

Albert Atserias. Proofs of Soundness and Proof Search (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{atserias:LIPIcs.FSTTCS.2020.2,
  author =	{Atserias, Albert},
  title =	{{Proofs of Soundness and Proof Search}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.2},
  URN =		{urn:nbn:de:0030-drops-132439},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.2},
  annote =	{Keywords: Proof complexity, automatability, Resolution, proof search, consistency statements, lower bounds, reflection principle, satisfiability}
}
Document
Track A: Algorithms, Complexity and Games
Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares

Authors: Tuomas Hakoniemi

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
We prove that both Polynomial Calculus and Sums-of-Squares proof systems admit a strong form of feasible interpolation property for sets of polynomial equality constraints. Precisely, given two sets P(x,z) and Q(y,z) of equality constraints, a refutation Π of P(x,z) ∪ Q(y,z), and any assignment a to the variables z, one can find a refutation of P(x,a) or a refutation of Q(y,a) in time polynomial in the length of the bit-string encoding the refutation Π. For Sums-of-Squares we rely on the use of Boolean axioms, but for Polynomial Calculus we do not assume their presence.

Cite as

Tuomas Hakoniemi. Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 63:1-63:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{hakoniemi:LIPIcs.ICALP.2020.63,
  author =	{Hakoniemi, Tuomas},
  title =	{{Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{63:1--63:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.63},
  URN =		{urn:nbn:de:0030-drops-124707},
  doi =		{10.4230/LIPIcs.ICALP.2020.63},
  annote =	{Keywords: Proof Complexity, Feasible Interpolation, Sums-of-Squares, Polynomial Calculus}
}
Document
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

Authors: Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)


Abstract
We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.

Cite as

Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.TIME.2019.6,
  author =	{de Almeida Borges, Ana and Conejero Rodr{\'\i}guez, Juan Jos\'{e} and Fern\'{a}ndez-Duque, David and Gonz\'{a}lez Bedmar, Mireia and Joosten, Joost J.},
  title =	{{The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.6},
  URN =		{urn:nbn:de:0030-drops-113649},
  doi =		{10.4230/LIPIcs.TIME.2019.6},
  annote =	{Keywords: linear temporal logic, monadic second order logic, formalized law, transport regulations}
}
Document
On the Symmetries of and Equivalence Test for Design Polynomials

Authors: Nikhil Gupta and Chandan Saha

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
In a Nisan-Wigderson design polynomial (in short, a design polynomial), every pair of monomials share a few common variables. A useful example of such a polynomial, introduced in [Neeraj Kayal et al., 2014], is the following: NW_{d,k}({x}) = sum_{h in F_d[z], deg(h) <= k}{ prod_{i=0}^{d-1}{x_{i, h(i)}}}, where d is a prime, F_d is the finite field with d elements, and k << d. The degree of the gcd of every pair of monomials in NW_{d,k} is at most k. For concreteness, we fix k = ceil[sqrt{d}]. The family of polynomials NW := {NW_{d,k} : d is a prime} and close variants of it have been used as hard explicit polynomial families in several recent arithmetic circuit lower bound proofs. But, unlike the permanent, very little is known about the various structural and algorithmic/complexity aspects of NW beyond the fact that NW in VNP. Is NW_{d,k} characterized by its symmetries? Is it circuit-testable, i.e., given a circuit C can we check efficiently if C computes NW_{d,k}? What is the complexity of equivalence test for NW, i.e., given black-box access to a f in F[{x}], can we check efficiently if there exists an invertible linear transformation A such that f = NW_{d,k}(A * {x})? Characterization of polynomials by their symmetries plays a central role in the geometric complexity theory program. Here, we answer the first two questions and partially answer the third. We show that NW_{d,k} is characterized by its group of symmetries over C, but not over R. We also show that NW_{d,k} is characterized by circuit identities which implies that NW_{d,k} is circuit-testable in randomized polynomial time. As another application of this characterization, we obtain the "flip theorem" for NW. We give an efficient equivalence test for NW in the case where the transformation A is a block-diagonal permutation-scaling matrix. The design of this algorithm is facilitated by an almost complete understanding of the group of symmetries of NW_{d,k}: We show that if A is in the group of symmetries of NW_{d,k} then A = D * P, where D and P are diagonal and permutation matrices respectively. This is proved by completely characterizing the Lie algebra of NW_{d,k}, and using an interplay between the Hessian of NW_{d,k} and the evaluation dimension.

Cite as

Nikhil Gupta and Chandan Saha. On the Symmetries of and Equivalence Test for Design Polynomials. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 53:1-53:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gupta_et_al:LIPIcs.MFCS.2019.53,
  author =	{Gupta, Nikhil and Saha, Chandan},
  title =	{{On the Symmetries of and Equivalence Test for Design Polynomials}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{53:1--53:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.53},
  URN =		{urn:nbn:de:0030-drops-109979},
  doi =		{10.4230/LIPIcs.MFCS.2019.53},
  annote =	{Keywords: Nisan-Wigderson design polynomial, characterization by symmetries, Lie algebra, group of symmetries, circuit testability, flip theorem, equivalence test}
}
Document
Resolution Lower Bounds for Refutation Statements

Authors: Michal Garlík

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in [Atserias and Müller, 2019] asks whether a certain natural propositional encoding of the above statement is hard for Resolution. We answer by giving an exponential size lower bound. (2) We show exponential resolution size lower bounds for reflection principles, thereby improving a result in [Albert Atserias and María Luisa Bonet, 2004]. (3) We provide new examples of CNFs that exponentially separate Res(2) from Resolution (an exponential separation of these two proof systems was originally proved in [Nathan Segerlind et al., 2004]).

Cite as

Michal Garlík. Resolution Lower Bounds for Refutation Statements. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 37:1-37:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{garlik:LIPIcs.MFCS.2019.37,
  author =	{Garl{\'\i}k, Michal},
  title =	{{Resolution Lower Bounds for Refutation Statements}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{37:1--37:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.37},
  URN =		{urn:nbn:de:0030-drops-109817},
  doi =		{10.4230/LIPIcs.MFCS.2019.37},
  annote =	{Keywords: reflection principles, refutation statements, Resolution, proof complexity}
}
Document
The Power of the Weisfeiler-Leman Algorithm to Decompose Graphs

Authors: Sandra Kiefer and Daniel Neuen

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
The Weisfeiler-Leman procedure is a widely-used approach for graph isomorphism testing that works by iteratively computing an isomorphism-invariant coloring of vertex tuples. Meanwhile, a fundamental tool in structural graph theory, which is often exploited in approaches to tackle the graph isomorphism problem, is the decomposition into bi- and triconnected components. We prove that the 2-dimensional Weisfeiler-Leman algorithm implicitly computes the decomposition of a graph into its triconnected components. Thus, the dimension of the algorithm needed to distinguish two given graphs is at most the dimension required to distinguish the corresponding decompositions into 3-connected components (assuming dimension at least 2). This result implies that for k >= 2, the k-dimensional algorithm distinguishes k-separators, i.e., k-tuples of vertices that separate the graph, from other vertex k-tuples. As a byproduct, we also obtain insights about the connectivity of constituent graphs of association schemes. In an application of the results, we show the new upper bound of k on the Weisfeiler-Leman dimension of graphs of treewidth at most k. Using a construction by Cai, Fürer, and Immerman, we also provide a new lower bound that is asymptotically tight up to a factor of 2.

Cite as

Sandra Kiefer and Daniel Neuen. The Power of the Weisfeiler-Leman Algorithm to Decompose Graphs. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 45:1-45:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.MFCS.2019.45,
  author =	{Kiefer, Sandra and Neuen, Daniel},
  title =	{{The Power of the Weisfeiler-Leman Algorithm to Decompose Graphs}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{45:1--45:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.45},
  URN =		{urn:nbn:de:0030-drops-109893},
  doi =		{10.4230/LIPIcs.MFCS.2019.45},
  annote =	{Keywords: Weisfeiler-Leman, separators, first-order logic, counting quantifiers}
}
Document
Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling

Authors: Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere

Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)


Abstract
We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatz refutation of the pebbling formula over G in size t+1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.

Cite as

Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere. Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{derezende_et_al:LIPIcs.CCC.2019.18,
  author =	{de Rezende, Susanna F. and Nordstr\"{o}m, Jakob and Meir, Or and Robere, Robert},
  title =	{{Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling}},
  booktitle =	{34th Computational Complexity Conference (CCC 2019)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-116-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{137},
  editor =	{Shpilka, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.18},
  URN =		{urn:nbn:de:0030-drops-108403},
  doi =		{10.4230/LIPIcs.CCC.2019.18},
  annote =	{Keywords: proof complexity, Nullstellensatz, pebble games, trade-offs, size, degree}
}
  • Refine by Author
  • 10 Atserias, Albert
  • 3 Nordström, Jakob
  • 2 Bonacina, Ilario
  • 2 Dawar, Anuj
  • 2 Galesi, Nicola
  • Show More...

  • Refine by Classification
  • 9 Theory of computation → Proof complexity
  • 5 Theory of computation → Finite Model Theory
  • 2 Mathematics of computing → Combinatorial algorithms
  • 2 Theory of computation → Algebraic complexity theory
  • 2 Theory of computation → Complexity theory and logic
  • Show More...

  • Refine by Keyword
  • 7 proof complexity
  • 4 Proof complexity
  • 3 Proof Complexity
  • 3 degree
  • 3 lower bounds
  • Show More...

  • Refine by Type
  • 28 document

  • Refine by Publication Year
  • 7 2019
  • 6 2022
  • 5 2015
  • 3 2018
  • 2 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