13 Search Results for "Lid�n, Tomas"


Document
Proving Unsatisfiability with Hitting Formulas

Authors: Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals

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


Abstract
A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since [Iwama, 1989] and, based on experimental evidence, Peitl and Szeider [Tomás Peitl and Stefan Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution. Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system {{rmHitting}}: a refutation of a CNF in {{rmHitting}} is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that {{rmHitting}} is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and {{rmHitting}} are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, {{rmHitting}} is surprisingly difficult to polynomially simulate in another proof system. Using the ideas of Raz-Shpilka’s polynomial identity testing for noncommutative circuits [Raz and Shpilka, 2005] we show that {{rmHitting}} is p-simulated by {{rmExtended {{rmFrege}}}}, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time. We consider multiple extensions of {{rmHitting}}, and in particular a proof system {{{rmHitting}}(⊕)} related to the {{{rmRes}}(⊕)} proof system for which no superpolynomial-size lower bounds are known. {{{rmHitting}}(⊕)} p-simulates the tree-like version of {{{rmRes}}(⊕)} and is at least quasi-polynomially stronger. We show that formulas expressing the non-existence of perfect matchings in the graphs K_{n,n+2} are exponentially hard for {{{rmHitting}}(⊕)} via a reduction to the partition bound for communication complexity. See the full version of the paper for the proofs. They are omitted in this Extended Abstract.

Cite as

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.ITCS.2024.48,
  author =	{Filmus, Yuval and Hirsch, Edward A. and Riazanov, Artur and Smal, Alexander and Vinyals, Marc},
  title =	{{Proving Unsatisfiability with Hitting Formulas}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{48:1--48:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.48},
  URN =		{urn:nbn:de:0030-drops-195762},
  doi =		{10.4230/LIPIcs.ITCS.2024.48},
  annote =	{Keywords: hitting formulas, polynomial identity testing, query complexity}
}
Document
Microservice-Aware Static Analysis: Opportunities, Gaps, and Advancements

Authors: Tomas Cerny and Davide Taibi

Published in: OASIcs, Volume 111, Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)


Abstract
Microservice architecture is the mainstream to fuel cloud-native systems with small service sets developed and deployed independently. The independent nature of this modular architecture also leads to challenges and gaps practitioners did not face in system monoliths. One of the major challenges with decentralization and its independent microservices that are managed by separate teams is that the evolving system architecture easily deviates far from the original plans, and it becomes difficult to maintain. Literature often refers to this process as system architecture degradation. Especially in the context of microservices, available tools are limited. This article challenges the audience on how static analysis could contribute to microservice system development and management, particularly managing architectural degradation. It elaborates on challenges and needed changes in the traditional code analysis to better fit these systems. Consequently, it discusses implications for practitioners once robust static analysis tools become available.

Cite as

Tomas Cerny and Davide Taibi. Microservice-Aware Static Analysis: Opportunities, Gaps, and Advancements. In Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022). Open Access Series in Informatics (OASIcs), Volume 111, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{cerny_et_al:OASIcs.Microservices.2020-2022.2,
  author =	{Cerny, Tomas and Taibi, Davide},
  title =	{{Microservice-Aware Static Analysis: Opportunities, Gaps, and Advancements}},
  booktitle =	{Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
  pages =	{2:1--2:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-306-5},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{111},
  editor =	{Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022.2},
  URN =		{urn:nbn:de:0030-drops-194647},
  doi =		{10.4230/OASIcs.Microservices.2020-2022.2},
  annote =	{Keywords: Microservice Architecture, Static Analysis, Reasoning, Decentralization}
}
Document
A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture

Authors: Markus Kirchweger, Tomáš Peitl, and Stefan Szeider

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


Abstract
In 1972, Paul Erdős, Vance Faber, and Lászlo Lovász asked whether every linear hypergraph with n vertices can be edge-colored with n colors, a statement that has come to be known as the EFL conjecture. Erdős himself considered the conjecture as one of his three favorite open problems, and offered increasing money prizes for its solution on several occasions. A proof of the conjecture was recently announced, for all but a finite number of hypergraphs. In this paper we look at some of the cases not covered by this proof. We use SAT solvers, and in particular the SAT Modulo Symmetries (SMS) framework, to generate non-colorable linear hypergraphs with a fixed number of vertices and hyperedges modulo isomorphisms. Since hypergraph colorability is NP-hard, we cannot directly express in a propositional formula that we want only non-colorable hypergraphs. Instead, we use one SAT (SMS) solver to generate candidate hypergraphs modulo isomorphisms, and another to reject them by finding a coloring. Each successive candidate is required to defeat all previous colorings, whereby we avoid having to generate and test all linear hypergraphs. Computational methods have previously been used to verify the EFL conjecture for small hypergraphs. We verify and extend these results to larger values and discuss challenges and directions. Ours is the first computational approach to the EFL conjecture that allows producing independently verifiable, DRAT proofs.

Cite as

Markus Kirchweger, Tomáš Peitl, and Stefan Szeider. A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.13,
  author =	{Kirchweger, Markus and Peitl, Tom\'{a}\v{s} and Szeider, Stefan},
  title =	{{A SAT Solver’s Opinion on the Erd\H{o}s-Faber-Lov\'{a}sz Conjecture}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{13:1--13:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.13},
  URN =		{urn:nbn:de:0030-drops-184752},
  doi =		{10.4230/LIPIcs.SAT.2023.13},
  annote =	{Keywords: hypergraphs, graph coloring, SAT modulo symmetries}
}
Document
Should Decisions in QCDCL Follow Prefix Order?

Authors: Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff

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


Abstract
Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the differences between QCDCL and propositional CDCL is that QCDCL typically follows the prefix order of the QBF for making decisions. We investigate an alternative model for QCDCL solving where decisions can be made in arbitrary order. The resulting system QCDCL^ANY is still sound and terminating, but does not necessarily allow to always learn asserting clauses or cubes. To address this potential drawback, we additionally introduce two subsystems that guarantee to always learn asserting clauses (QCDCL^UNI-ANI) and asserting cubes (QCDCL^EXI-ANY), respectively. We model all four approaches by formal proof systems and show that QCDCL^UNI-ANY is exponentially better than QCDCL on false formulas, whereas QCDCL^EXI-ANY is exponentially better than QCDCL on true QBFs. Technically, this involves constructing specific QBF families and showing lower and upper bounds in the respective proof systems. We complement our theoretical study with some initial experiments that confirm our theoretical findings.

Cite as

Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff. Should Decisions in QCDCL Follow Prefix Order?. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bohm_et_al:LIPIcs.SAT.2022.11,
  author =	{B\"{o}hm, Benjamin and Peitl, Tom\'{a}\v{s} and Beyersdorff, Olaf},
  title =	{{Should Decisions in QCDCL Follow Prefix Order?}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.11},
  URN =		{urn:nbn:de:0030-drops-166850},
  doi =		{10.4230/LIPIcs.SAT.2022.11},
  annote =	{Keywords: QBF, CDCL, proof complexity, lower bounds}
}
Document
Track A: Algorithms, Complexity and Games
Max Weight Independent Set in Graphs with No Long Claws: An Analog of the Gyárfás' Path Argument

Authors: Konrad Majewski, Tomáš Masařík, Jana Novotná, Karolina Okrasa, Marcin Pilipczuk, Paweł Rzążewski, and Marek Sokołowski

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


Abstract
We revisit recent developments for the Maximum Weight Independent Set problem in graphs excluding a subdivided claw S_{t,t,t} as an induced subgraph [Chudnovsky, Pilipczuk, Pilipczuk, Thomassé, SODA 2020] and provide a subexponential-time algorithm with improved running time 2^𝒪(√nlog n) and a quasipolynomial-time approximation scheme with improved running time 2^𝒪(ε^{-1} log⁵ n). The Gyárfás' path argument, a powerful tool that is the main building block for many algorithms in P_t-free graphs, ensures that given an n-vertex P_t-free graph, in polynomial time we can find a set P of at most t-1 vertices, such that every connected component of G-N[P] has at most n/2 vertices. Our main technical contribution is an analog of this result for S_{t,t,t}-free graphs: given an n-vertex S_{t,t,t}-free graph, in polynomial time we can find a set P of 𝒪(t log n) vertices and an extended strip decomposition (an appropriate analog of the decomposition into connected components) of G-N[P] such that every particle (an appropriate analog of a connected component to recurse on) of the said extended strip decomposition has at most n/2 vertices.

Cite as

Konrad Majewski, Tomáš Masařík, Jana Novotná, Karolina Okrasa, Marcin Pilipczuk, Paweł Rzążewski, and Marek Sokołowski. Max Weight Independent Set in Graphs with No Long Claws: An Analog of the Gyárfás' Path Argument. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 93:1-93:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{majewski_et_al:LIPIcs.ICALP.2022.93,
  author =	{Majewski, Konrad and Masa\v{r}{\'\i}k, Tom\'{a}\v{s} and Novotn\'{a}, Jana and Okrasa, Karolina and Pilipczuk, Marcin and Rz\k{a}\.{z}ewski, Pawe{\l} and Soko{\l}owski, Marek},
  title =	{{Max Weight Independent Set in Graphs with No Long Claws: An Analog of the Gy\'{a}rf\'{a}s' Path Argument}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{93:1--93:19},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.93},
  URN =		{urn:nbn:de:0030-drops-164343},
  doi =		{10.4230/LIPIcs.ICALP.2022.93},
  annote =	{Keywords: Max Independent Set, subdivided claw, QPTAS, subexponential-time algorithm}
}
Document
FPT and FPT-Approximation Algorithms for Unsplittable Flow on Trees

Authors: Tomás Martínez-Muñoz and Andreas Wiese

Published in: LIPIcs, Volume 204, 29th Annual European Symposium on Algorithms (ESA 2021)


Abstract
We study the unsplittable flow on trees (UFT) problem in which we are given a tree with capacities on its edges and a set of tasks, where each task is described by a path and a demand. Our goal is to select a subset of the given tasks of maximum size such that the demands of the selected tasks respect the edge capacities. The problem models throughput maximization in tree networks. The best known approximation ratio for (unweighted) UFT is O(log n). We study the problem under the angle of FPT and FPT-approximation algorithms. We prove that - UFT is FPT if the parameters are the cardinality k of the desired solution and the number of different task demands in the input, - UFT is FPT under (1+δ)-resource augmentation of the edge capacities for parameters k and 1/δ, and - UFT admits an FPT-5-approximation algorithm for parameter k. One key to our results is to compute structured hitting sets of the input edges which partition the given tree into O(k) clean components. This allows us to guess important properties of the optimal solution. Also, in some settings we can compute core sets of subsets of tasks out of which at least one task i is contained in the optimal solution. These sets have bounded size, and hence we can guess this task i easily. A consequence of our results is that the integral multicommodity flow problem on trees is FPT if the parameter is the desired amount of sent flow. Also, even under (1+δ)-resource augmentation UFT is APX-hard, and hence our FPT-approximation algorithm for this setting breaks this boundary.

Cite as

Tomás Martínez-Muñoz and Andreas Wiese. FPT and FPT-Approximation Algorithms for Unsplittable Flow on Trees. In 29th Annual European Symposium on Algorithms (ESA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 204, pp. 67:1-67:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{martinezmunoz_et_al:LIPIcs.ESA.2021.67,
  author =	{Mart{\'\i}nez-Mu\~{n}oz, Tom\'{a}s and Wiese, Andreas},
  title =	{{FPT and FPT-Approximation Algorithms for Unsplittable Flow on Trees}},
  booktitle =	{29th Annual European Symposium on Algorithms (ESA 2021)},
  pages =	{67:1--67:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-204-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{204},
  editor =	{Mutzel, Petra and Pagh, Rasmus and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2021.67},
  URN =		{urn:nbn:de:0030-drops-146486},
  doi =		{10.4230/LIPIcs.ESA.2021.67},
  annote =	{Keywords: FPT algorithms, FPT-approximation algorithms, packing problems, unsplittable flow, trees}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Arboreal Categories and Resources

Authors: Samson Abramsky and Luca Reggio

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
We introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a very general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fraïssé and modal bisimulation games recently introduced in [Abramsky et al., 2017; S. Abramsky and N. Shah, 2018; Abramsky and Shah, 2021] are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.

Cite as

Samson Abramsky and Luca Reggio. Arboreal Categories and Resources. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.ICALP.2021.115,
  author =	{Abramsky, Samson and Reggio, Luca},
  title =	{{Arboreal Categories and Resources}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{115:1--115:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.115},
  URN =		{urn:nbn:de:0030-drops-141845},
  doi =		{10.4230/LIPIcs.ICALP.2021.115},
  annote =	{Keywords: factorisation system, embedding, comonad, coalgebra, open maps, bisimulation, game, resources, relational structures, finite model theory}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Smooth Approximations and Relational Width Collapses

Authors: Antoine Mottet, Tomáš Nagy, Michael Pinsker, and Michał Wrona

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
We prove that relational structures admitting specific polymorphisms (namely, canonical pseudo-WNU operations of all arities n ≥ 3) have low relational width. This implies a collapse of the bounded width hierarchy for numerous classes of infinite-domain CSPs studied in the literature. Moreover, we obtain a characterization of bounded width for first-order reducts of unary structures and a characterization of MMSNP sentences that are equivalent to a Datalog program, answering a question posed by Bienvenu et al.. In particular, the bounded width hierarchy collapses in those cases as well.

Cite as

Antoine Mottet, Tomáš Nagy, Michael Pinsker, and Michał Wrona. Smooth Approximations and Relational Width Collapses. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 138:1-138:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{mottet_et_al:LIPIcs.ICALP.2021.138,
  author =	{Mottet, Antoine and Nagy, Tom\'{a}\v{s} and Pinsker, Michael and Wrona, Micha{\l}},
  title =	{{Smooth Approximations and Relational Width Collapses}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{138:1--138:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.138},
  URN =		{urn:nbn:de:0030-drops-142075},
  doi =		{10.4230/LIPIcs.ICALP.2021.138},
  annote =	{Keywords: local consistency, bounded width, constraint satisfaction problems, polymorphisms, smooth approximations}
}
Document
Integer Programming in Parameterized Complexity: Three Miniatures

Authors: Tomás Gavenciak, Dusan Knop, and Martin Koutecký

Published in: LIPIcs, Volume 115, 13th International Symposium on Parameterized and Exact Computation (IPEC 2018)


Abstract
Powerful results from the theory of integer programming have recently led to substantial advances in parameterized complexity. However, our perception is that, except for Lenstra's algorithm for solving integer linear programming in fixed dimension, there is still little understanding in the parameterized complexity community of the strengths and limitations of the available tools. This is understandable: it is often difficult to infer exact runtimes or even the distinction between FPT and XP algorithms, and some knowledge is simply unwritten folklore in a different community. We wish to make a step in remedying this situation. To that end, we first provide an easy to navigate quick reference guide of integer programming algorithms from the perspective of parameterized complexity. Then, we show their applications in three case studies, obtaining FPT algorithms with runtime f(k) poly(n). We focus on: - Modeling: since the algorithmic results follow by applying existing algorithms to new models, we shift the focus from the complexity result to the modeling result, highlighting common patterns and tricks which are used. - Optimality program: after giving an FPT algorithm, we are interested in reducing the dependence on the parameter; we show which algorithms and tricks are often useful for speed-ups. - Minding the poly(n): reducing f(k) often has the unintended consequence of increasing poly(n); so we highlight the common trade-offs and show how to get the best of both worlds. Specifically, we consider graphs of bounded neighborhood diversity which are in a sense the simplest of dense graphs, and we show several FPT algorithms for Capacitated Dominating Set, Sum Coloring, and Max-q-Cut by modeling them as convex programs in fixed dimension, n-fold integer programs, bounded dual treewidth programs, and indefinite quadratic programs in fixed dimension.

Cite as

Tomás Gavenciak, Dusan Knop, and Martin Koutecký. Integer Programming in Parameterized Complexity: Three Miniatures. In 13th International Symposium on Parameterized and Exact Computation (IPEC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 115, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gavenciak_et_al:LIPIcs.IPEC.2018.21,
  author =	{Gavenciak, Tom\'{a}s and Knop, Dusan and Kouteck\'{y}, Martin},
  title =	{{Integer Programming in Parameterized Complexity: Three Miniatures}},
  booktitle =	{13th International Symposium on Parameterized and Exact Computation (IPEC 2018)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-084-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{115},
  editor =	{Paul, Christophe and Pilipczuk, Michal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2018.21},
  URN =		{urn:nbn:de:0030-drops-102225},
  doi =		{10.4230/LIPIcs.IPEC.2018.21},
  annote =	{Keywords: graph coloring, parameterized complexity, integer linear programming, integer convex programming}
}
Document
Target Set Selection in Dense Graph Classes

Authors: Pavel Dvorák, Dusan Knop, and Tomás Toufar

Published in: LIPIcs, Volume 123, 29th International Symposium on Algorithms and Computation (ISAAC 2018)


Abstract
In this paper we study the Target Set Selection problem from a parameterized complexity perspective. Here for a given graph and a threshold for each vertex the task is to find a set of vertices (called a target set) to activate at the beginning which activates the whole graph during the following iterative process. A vertex outside the active set becomes active if the number of so far activated vertices in its neighborhood is at least its threshold. We give two parameterized algorithms for a special case where each vertex has the threshold set to the half of its neighbors (the so called Majority Target Set Selection problem) for parameterizations by the neighborhood diversity and the twin cover number of the input graph. We complement these results from the negative side. We give a hardness proof for the Majority Target Set Selection problem when parameterized by (a restriction of) the modular-width - a natural generalization of both previous structural parameters. We show that the Target Set Selection problem parameterized by the neighborhood diversity when there is no restriction on the thresholds is W[1]-hard.

Cite as

Pavel Dvorák, Dusan Knop, and Tomás Toufar. Target Set Selection in Dense Graph Classes. In 29th International Symposium on Algorithms and Computation (ISAAC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 123, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{dvorak_et_al:LIPIcs.ISAAC.2018.18,
  author =	{Dvor\'{a}k, Pavel and Knop, Dusan and Toufar, Tom\'{a}s},
  title =	{{Target Set Selection in Dense Graph Classes}},
  booktitle =	{29th International Symposium on Algorithms and Computation (ISAAC 2018)},
  pages =	{18:1--18:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-094-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{123},
  editor =	{Hsu, Wen-Lian and Lee, Der-Tsai and Liao, Chung-Shou},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2018.18},
  URN =		{urn:nbn:de:0030-drops-99666},
  doi =		{10.4230/LIPIcs.ISAAC.2018.18},
  annote =	{Keywords: parameterized complexity, target set selection, dense graphs}
}
Document
Reformulations for Integrated Planning of Railway Traffic and Network Maintenance

Authors: Tomas Lidén

Published in: OASIcs, Volume 65, 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)


Abstract
This paper addresses the capacity planning problem of coordinating train services and network maintenance windows for a railway system. We present model reformulations, for a mixed integer linear optimization model, which give a mathematically stronger model and substantial improvements in solving performance - as demonstrated with computational experiments on a set of synthetic test instances. As a consequence, more instances can be solved to optimality within a given time limit and the optimality gap can be reduced quicker.

Cite as

Tomas Lidén. Reformulations for Integrated Planning of Railway Traffic and Network Maintenance. In 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018). Open Access Series in Informatics (OASIcs), Volume 65, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{liden:OASIcs.ATMOS.2018.1,
  author =	{Lid\'{e}n, Tomas},
  title =	{{Reformulations for Integrated Planning of Railway Traffic and Network Maintenance}},
  booktitle =	{18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)},
  pages =	{1:1--1:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-096-5},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{65},
  editor =	{Bornd\"{o}rfer, Ralf and Storandt, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2018.1},
  URN =		{urn:nbn:de:0030-drops-97065},
  doi =		{10.4230/OASIcs.ATMOS.2018.1},
  annote =	{Keywords: Railway scheduling, Maintenance planning, Optimization}
}
Document
Piecewise Testable Languages and Nondeterministic Automata

Authors: Tomás Masopust

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)


Abstract
A regular language is k-piecewise testable if it is a finite boolean combination of languages of the form Sigma^* a_1 Sigma^* ... Sigma^* a_n Sigma^*, where a_i in Sigma and 0 <= n <= k. Given a DFA A and k >= 0, it is an NL-complete problem to decide whether the language L(A) is piecewise testable and, for k >= 4, it is coNP-complete to decide whether the language L(A) is k-piecewise testable. It is known that the depth of the minimal DFA serves as an upper bound on k. Namely, if L(A) is piecewise testable, then it is k-piecewise testable for k equal to the depth of A. In this paper, we show that some form of nondeterminism does not violate this upper bound result. Specifically, we define a class of NFAs, called ptNFAs, that recognize piecewise testable languages and show that the depth of a ptNFA provides an (up to exponentially better) upper bound on k than the minimal DFA. We provide an application of our result, discuss the relationship between k-piecewise testability and the depth of NFAs, and study the complexity of k-piecewise testability for ptNFAs.

Cite as

Tomás Masopust. Piecewise Testable Languages and Nondeterministic Automata. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 67:1-67:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{masopust:LIPIcs.MFCS.2016.67,
  author =	{Masopust, Tom\'{a}s},
  title =	{{Piecewise Testable Languages and Nondeterministic Automata}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{67:1--67:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.67},
  URN =		{urn:nbn:de:0030-drops-64799},
  doi =		{10.4230/LIPIcs.MFCS.2016.67},
  annote =	{Keywords: automata, logics, languages, k-piecewise testability, nondeterminism}
}
Document
On the Robustness of Bucket Brigade Quantum RAM

Authors: Srinivasan Arunachalam, Vlad Gheorghiu, Tomas Jochym-O'Connor, Michele Mosca, and Priyaa Varshinee Srinivasan

Published in: LIPIcs, Volume 44, 10th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2015)


Abstract
We study the robustness of the bucket brigade quantum random access memory model introduced by Giovannetti, Lloyd, and Maccone [Phys. Rev. Lett., 2008]. Due to a result of Regev and Schiff [ICALP, 2008], we show that for a class of error models the error rate per gate in the bucket brigade quantum memory has to be of order o(2^{-n/2}) (where N=2^n is the size of the memory) whenever the memory is used as an oracle for the quantum searching problem. We conjecture that this is the case for any realistic error model that will be encountered in practice, and that for algorithms with super-polynomially many oracle queries the error rate must be super-polynomially small, which further motivates the need for quantum error correction. We introduce a circuit model for the quantum bucket brigade architecture and argue that quantum error correction for the circuit causes the quantum bucket brigade architecture to lose its primary advantage of a small number of "active" gates, since all components have to be actively error corrected.

Cite as

Srinivasan Arunachalam, Vlad Gheorghiu, Tomas Jochym-O'Connor, Michele Mosca, and Priyaa Varshinee Srinivasan. On the Robustness of Bucket Brigade Quantum RAM. In 10th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 44, pp. 226-244, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{arunachalam_et_al:LIPIcs.TQC.2015.226,
  author =	{Arunachalam, Srinivasan and Gheorghiu, Vlad and Jochym-O'Connor, Tomas and Mosca, Michele and Srinivasan, Priyaa Varshinee},
  title =	{{On the Robustness of Bucket Brigade Quantum RAM}},
  booktitle =	{10th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2015)},
  pages =	{226--244},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-96-5},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{44},
  editor =	{Beigi, Salman and K\"{o}nig, Robert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2015.226},
  URN =		{urn:nbn:de:0030-drops-55594},
  doi =		{10.4230/LIPIcs.TQC.2015.226},
  annote =	{Keywords: Quantum Mechanics, Quantum Memories, Quantum Error Correction}
}
  • Refine by Author
  • 2 Knop, Dusan
  • 2 Peitl, Tomáš
  • 1 Abramsky, Samson
  • 1 Arunachalam, Srinivasan
  • 1 Beyersdorff, Olaf
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Graph algorithms analysis
  • 2 Theory of computation → Parameterized complexity and exact algorithms
  • 2 Theory of computation → Proof complexity
  • 1 Applied computing → Transportation
  • 1 Computer systems organization → Cloud computing
  • Show More...

  • Refine by Keyword
  • 2 graph coloring
  • 2 parameterized complexity
  • 1 CDCL
  • 1 Decentralization
  • 1 FPT algorithms
  • Show More...

  • Refine by Type
  • 13 document

  • Refine by Publication Year
  • 3 2021
  • 2 2018
  • 2 2022
  • 2 2023
  • 1 2015
  • 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