29 Search Results for "F�genschuh, Armin"

Document
DOI: 10.4230/LIPIcs.SAT.2023.3
CadiBack: Extracting Backbones with CaDiCaL

Authors: Armin Biere, Nils Froleyks, and Wenxi Wang

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

Abstract
The backbone of a satisfiable formula is the set of literals that are true in all its satisfying assignments. Backbone computation can improve a wide range of SAT-based applications, such as verification, fault localization and product configuration. In this tool paper, we introduce a new backbone extraction tool called CadiBack. It takes advantage of unique features available in our state-of-the-art SAT solver CaDiCaL including transparent inprocessing and single clause assumptions, which have not been evaluated in this context before. In addition, CaDiCaL is enhanced with an improved algorithm to support model rotation by utilizing watched literal data structures. In our comprehensive experiments with a large number of benchmarks, CadiBack solves 60% more instances than the state-of-the-art backbone extraction tool MiniBones. Our tool is thoroughly tested with fuzzing, internal correctness checking and cross-checking on a large benchmark set. It is publicly available as open source, well documented and easy to extend.
Cite as

Armin Biere, Nils Froleyks, and Wenxi Wang. CadiBack: Extracting Backbones with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{biere_et_al:LIPIcs.SAT.2023.3,
  author =	{Biere, Armin and Froleyks, Nils and Wang, Wenxi},
  title =	{{CadiBack: Extracting Backbones with CaDiCaL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{3:1--3:12},
  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.3},
  URN =		{urn:nbn:de:0030-drops-184655},
  doi =		{10.4230/LIPIcs.SAT.2023.3},
  annote =	{Keywords: Satisfiability, Backbone, Incremental Solving}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.8
IPASIR-UP: User Propagators for CDCL

Authors: Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere

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

Abstract
Modern SAT solvers are frequently embedded as sub-reasoning engines into more complex tools for addressing problems beyond the Boolean satisfiability problem. Examples include solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration and counting. In such use cases, the SAT solver is often able to provide relevant information beyond the satisfiability answer. Further, domain knowledge of the embedding system (e.g., symmetry properties or theory axioms) can be beneficial for the CDCL search, but cannot be efficiently represented in clausal form. In this paper, we propose a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. Our goal is to capture the most essential functionalities that are sufficient to simplify and improve use cases that require a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, we extend CaDiCaL with our interface and evaluate it on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.
Cite as

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User Propagators for CDCL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{fazekas_et_al:LIPIcs.SAT.2023.8,
  author =	{Fazekas, Katalin and Niemetz, Aina and Preiner, Mathias and Kirchweger, Markus and Szeider, Stefan and Biere, Armin},
  title =	{{IPASIR-UP: User Propagators for CDCL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{8:1--8:13},
  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.8},
  URN =		{urn:nbn:de:0030-drops-184709},
  doi =		{10.4230/LIPIcs.SAT.2023.8},
  annote =	{Keywords: SAT, CDCL, Satisfiability Modulo Theories, Satisfiability Modulo Symmetries}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.21
Faster LRAT Checking Than Solving with CaDiCaL

Authors: Florian Pollitt, Mathias Fleury, and Armin Biere

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

Abstract
DRAT is the standard proof format used in the SAT Competition. It is easy to generate but checking proofs often takes even more time than solving the problem. An alternative is to use the LRAT proof system. While LRAT is easier and way more efficient to check, it is more complex to generate directly. Due to this complexity LRAT is not supported natively by any state-of-the-art SAT solver. Therefore Carneiro and Heule proposed the mixed proof format FRAT which still suffers from costly intermediate translation. We present an extension to the state-of-the-art solver CaDiCaL which is able to generate LRAT natively for all procedures implemented in CaDiCaL. We further present Lrat-Trim, a tool which not only trims and checks LRAT proofs in both ASCII and binary format but also produces clausal cores and has been tested thoroughly. Our experiments on recent competition benchmarks show that our approach reduces time of proof generation and certification substantially compared to competing approaches using intermediate DRAT or FRAT proofs.
Cite as

Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT Checking Than Solving with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 21:1-21:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{pollitt_et_al:LIPIcs.SAT.2023.21,
  author =	{Pollitt, Florian and Fleury, Mathias and Biere, Armin},
  title =	{{Faster LRAT Checking Than Solving with CaDiCaL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{21:1--21:12},
  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.21},
  URN =		{urn:nbn:de:0030-drops-184837},
  doi =		{10.4230/LIPIcs.SAT.2023.21},
  annote =	{Keywords: SAT solving, Proof Checking, DRAT, LRAT, FRAT}
}
Document
DOI: 10.4230/DagRep.12.10.84
Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)

Authors: Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel

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

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22411 "Theory and Practice of SAT and Combinatorial Solving". The purpose of this workshop was to explore the Boolean satisfiability (SAT) problem, which plays a fascinating dual role in computer science. By the theory of NP-completeness, this problem captures thousands of important applications in different fields, and a rich mathematical theory has been developed showing that all these problems are likely to be infeasible to solve in the worst case. But real-world problems are typically not worst-case, and in recent decades exceedingly efficient algorithms based on so-called conflict-driven clause learning (CDCL) have turned SAT solvers into highly practical tools for solving large-scale real-world problems in a wide range of application areas. Analogous developments have taken place for problems beyond NP such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, satisfiability modulo theories (SMT) solving, quantified Boolean formula (QBF) solving, constraint programming, and mixed integer programming, where the conflict-driven paradigm has sometimes been added to other powerful techniques. The current state of the art in combinatorial solving presents a host of exciting challenges at the borderline between theory and practice. Can we gain a deeper scientific understanding of the techniques and heuristics used in modern combinatorial solvers and why they are so successful? Can we develop tools for rigorous analysis of the potential and limitations of these algorithms? Can computational complexity theory be extended to shed light on real-world settings that go beyond worst case? Can more powerful methods of reasoning developed in theoretical research be harnessed to yield improvements in practical performance? And can state-of-the-art combinatorial solvers be enhanced to not only solve problems, but also provide verifiable proofs of correctness for the solutions they produce? This workshop gathered leading applied and theoretical researchers working on SAT and combinatorial optimization more broadly in order to stimulate an exchange of ideas and techniques. We see great opportunities for fruitful interplay between theory and practice in these areas, as well as for technology transfer between different paradigms in combinatorial optimization, and our assessment is that this workshop demonstrated very convincingly that a more vigorous interaction has potential for major long-term impact in computer science, as well for applications in industry.
Cite as

Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel. Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). In Dagstuhl Reports, Volume 12, Issue 10, pp. 84-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.12.10.84,
  author =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  title =	{{Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)}},
  pages =	{84--105},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{10},
  editor =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.10.84},
  URN =		{urn:nbn:de:0030-drops-178212},
  doi =		{10.4230/DagRep.12.10.84},
  annote =	{Keywords: Boolean satisfiability (SAT), SAT solving, computational complexity, proof complexity, combinatorial solving, combinatorial optimization, constraint programming, mixed integer linear programming}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.27
Migrating Solver State

Authors: Armin Biere, Md Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, and Michael W. Whalen

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

Abstract
We present approaches to store and restore the state of a SAT solver, allowing us to migrate the state between different compute resources, or even between different solvers. This can be used in many ways, e.g., to improve the fault tolerance of solvers, to schedule SAT problems on a restricted number of cores, or to use dedicated preprocessing tools for inprocessing. We identify a minimum viable subset of the solver state to migrate such that the loss of performance is small. We then present and implement two different approaches to state migration: one approach stores the state at the end of a solver run whereas the other approach stores the state continuously as part of the proof trace. We show that our approaches enable the generation of correct models and valid unsatisfiability proofs. Experimental results confirm that the overhead is reasonable and that in several cases solver performance actually improves.
Cite as

Armin Biere, Md Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, and Michael W. Whalen. Migrating Solver State. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{biere_et_al:LIPIcs.SAT.2022.27,
  author =	{Biere, Armin and Chowdhury, Md Solimul and Heule, Marijn J. H. and Kiesl, Benjamin and Whalen, Michael W.},
  title =	{{Migrating Solver State}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{27:1--27:24},
  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.27},
  URN =		{urn:nbn:de:0030-drops-167015},
  doi =		{10.4230/LIPIcs.SAT.2022.27},
  annote =	{Keywords: SAT, SMT, Cloud Computing, Serverless Computing}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.127
Satisfiability Problems for Finite Groups

Authors: Paweł M. Idziak, Piotr Kawałek, Jacek Krzaczkowski, and Armin Weiß

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

Abstract
Over twenty years ago, Goldmann and Russell initiated the study of the complexity of the equation satisfiability problem (PolSat and the NUDFA program satisfiability problem (ProgramSat) in finite groups. They showed that these problems are in 𝖯 for nilpotent groups while they are NP-complete for non-solvable groups. In this work we completely characterize finite groups for which the problem ProgramSat can be solved in randomized polynomial time under the assumptions of the Randomized Exponential Time Hypothesis and the Constant Degree Hypothesis. We also determine the complexity of PolSat for a wide class of finite groups. As a by-product, we obtain a classification for ListPolSat, a version of PolSat where each variable can be restricted to an arbitrary subset. Finally, we also prove unconditional algorithms for these problems in certain cases.
Cite as

Paweł M. Idziak, Piotr Kawałek, Jacek Krzaczkowski, and Armin Weiß. Satisfiability Problems for Finite Groups. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 127:1-127:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{idziak_et_al:LIPIcs.ICALP.2022.127,
  author =	{Idziak, Pawe{\l} M. and Kawa{\l}ek, Piotr and Krzaczkowski, Jacek and Wei{\ss}, Armin},
  title =	{{Satisfiability Problems for Finite Groups}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{127:1--127: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.127},
  URN =		{urn:nbn:de:0030-drops-164685},
  doi =		{10.4230/LIPIcs.ICALP.2022.127},
  annote =	{Keywords: Satisifiability, Solvable groups, ProgramSat, PolSat, Exponential Time Hypothesis}
}
Document
DOI: 10.4230/LIPIcs.STACS.2022.26
The Isomorphism Problem for Plain Groups Is in Σ₃^{𝖯}

Authors: Heiko Dietrich, Murray Elder, Adam Piggott, Youming Qiao, and Armin Weiß

Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

Abstract
Testing isomorphism of infinite groups is a classical topic, but from the complexity theory viewpoint, few results are known. Sénizergues and the fifth author (ICALP2018) proved that the isomorphism problem for virtually free groups is decidable in PSPACE when the input is given in terms of so-called virtually free presentations. Here we consider the isomorphism problem for the class of plain groups, that is, groups that are isomorphic to a free product of finitely many finite groups and finitely many copies of the infinite cyclic group. Every plain group is naturally and efficiently presented via an inverse-closed finite convergent length-reducing rewriting system. We prove that the isomorphism problem for plain groups given in this form lies in the polynomial time hierarchy, more precisely, in Σ₃^𝖯. This result is achieved by combining new geometric and algebraic characterisations of groups presented by inverse-closed finite convergent length-reducing rewriting systems developed in recent work of the second and third authors (2021) with classical finite group isomorphism results of Babai and Szemerédi (1984).
Cite as

Heiko Dietrich, Murray Elder, Adam Piggott, Youming Qiao, and Armin Weiß. The Isomorphism Problem for Plain Groups Is in Σ₃^{𝖯}. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 26:1-26:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dietrich_et_al:LIPIcs.STACS.2022.26,
  author =	{Dietrich, Heiko and Elder, Murray and Piggott, Adam and Qiao, Youming and Wei{\ss}, Armin},
  title =	{{The Isomorphism Problem for Plain Groups Is in \Sigma₃^\{𝖯\}}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{26:1--26:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.26},
  URN =		{urn:nbn:de:0030-drops-158368},
  doi =		{10.4230/LIPIcs.STACS.2022.26},
  annote =	{Keywords: plain group, isomorphism problem, polynomial hierarchy, \Sigma₃^\{𝖯\} complexity class, inverse-closed finite convergent length-reducing rewriting system}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.74
Parallel Algorithms for Power Circuits and the Word Problem of the Baumslag Group

Authors: Caroline Mattes and Armin Weiß

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
Power circuits have been introduced in 2012 by Myasnikov, Ushakov and Won as a data structure for non-elementarily compressed integers supporting the arithmetic operations addition and (x,y) ↦ x⋅2^y. The same authors applied power circuits to give a polynomial-time solution to the word problem of the Baumslag group, which has a non-elementary Dehn function. In this work, we examine power circuits and the word problem of the Baumslag group under parallel complexity aspects. In particular, we establish that the word problem of the Baumslag group can be solved in NC - even though one of the essential steps is to compare two integers given by power circuits and this, in general, is shown to be 𝖯-complete. The key observation is that the depth of the occurring power circuits is logarithmic and such power circuits can be compared in NC.
Cite as

Caroline Mattes and Armin Weiß. Parallel Algorithms for Power Circuits and the Word Problem of the Baumslag Group. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 74:1-74:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{mattes_et_al:LIPIcs.MFCS.2021.74,
  author =	{Mattes, Caroline and Wei{\ss}, Armin},
  title =	{{Parallel Algorithms for Power Circuits and the Word Problem of the Baumslag Group}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{74:1--74:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.74},
  URN =		{urn:nbn:de:0030-drops-145148},
  doi =		{10.4230/LIPIcs.MFCS.2021.74},
  annote =	{Keywords: Word problem, Baumslag group, power circuit, parallel complexity}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2020.10
A Strategic Routing Framework and Algorithms for Computing Alternative Paths

Authors: Thomas Bläsius, Maximilian Böther, Philipp Fischbeck, Tobias Friedrich, Alina Gries, Falk Hüffner, Otto Kißig, Pascal Lenzner, Louise Molitor, Leon Schiller, Armin Wells, and Simon Wietheger

Published in: OASIcs, Volume 85, 20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020)

Abstract
Traditional navigation services find the fastest route for a single driver. Though always using the fastest route seems desirable for every individual, selfish behavior can have undesirable effects such as higher energy consumption and avoidable congestion, even leading to higher overall and individual travel times. In contrast, strategic routing aims at optimizing the traffic for all agents regarding a global optimization goal. We introduce a framework to formalize real-world strategic routing scenarios as algorithmic problems and study one of them, which we call Single Alternative Path (SAP), in detail. There, we are given an original route between a single origin-destination pair. The goal is to suggest an alternative route to all agents that optimizes the overall travel time under the assumption that the agents distribute among both routes according to a psychological model, for which we introduce the concept of Pareto-conformity. We show that the SAP problem is NP-complete, even for such models. Nonetheless, assuming Pareto-conformity, we give multiple algorithms for different variants of SAP, using multi-criteria shortest path algorithms as subroutines. Moreover, we prove that several natural models are in fact Pareto-conform. The implementation and evaluation of our algorithms serve as a proof of concept, showing that SAP can be solved in reasonable time even though the algorithms have exponential running time in the worst case.
Cite as

Thomas Bläsius, Maximilian Böther, Philipp Fischbeck, Tobias Friedrich, Alina Gries, Falk Hüffner, Otto Kißig, Pascal Lenzner, Louise Molitor, Leon Schiller, Armin Wells, and Simon Wietheger. A Strategic Routing Framework and Algorithms for Computing Alternative Paths. In 20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020). Open Access Series in Informatics (OASIcs), Volume 85, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{blasius_et_al:OASIcs.ATMOS.2020.10,
  author =	{Bl\"{a}sius, Thomas and B\"{o}ther, Maximilian and Fischbeck, Philipp and Friedrich, Tobias and Gries, Alina and H\"{u}ffner, Falk and Ki{\ss}ig, Otto and Lenzner, Pascal and Molitor, Louise and Schiller, Leon and Wells, Armin and Wietheger, Simon},
  title =	{{A Strategic Routing Framework and Algorithms for Computing Alternative Paths}},
  booktitle =	{20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020)},
  pages =	{10:1--10:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-170-2},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{85},
  editor =	{Huisman, Dennis and Zaroliagis, Christos D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2020.10},
  URN =		{urn:nbn:de:0030-drops-131469},
  doi =		{10.4230/OASIcs.ATMOS.2020.10},
  annote =	{Keywords: Routing, Strategic Routing, Selfish Routing, Route Planning, Network Flow, Algorithm Design}
}
Document
DOI: 10.4230/OASIcs.ASD.2020.4
Agile Requirement Engineering for a Cloud System for Automated and Networked Vehicles

Authors: Armin Mokhtarian, Alexandru Kampmann, Bassam Alrifaee, Stefan Kowalewski, Bastian Lampe, and Lutz Eckstein

Published in: OASIcs, Volume 79, 2nd International Workshop on Autonomous Systems Design (ASD 2020)

Abstract
This paper presents a methodology for the agile development of a cloud system in a multi-partner project centered around automated vehicles. Besides providing an external environment model as an additional input to the automation, the cloud system is also the main gateway for users to interact with automated vehicles through applications on mobile devices. Multiple factors are posing a challenge in our context. Coordination becomes especially challenging, as stakeholders are spread among different locations with backgrounds from various domains. Furthermore, automated vehicles for different applications, such as delivery or taxi services, give rise to a large number of use cases that our cloud system has to support. For our agile development process, we use standardized templates for the description of use-cases, which are initialized from storyboards and iteratively refined by stakeholders. These use-case templates are subsequently transformed into machine-readable specifications, which allows for generation of REST APIs for our cloud system.
Cite as

Armin Mokhtarian, Alexandru Kampmann, Bassam Alrifaee, Stefan Kowalewski, Bastian Lampe, and Lutz Eckstein. Agile Requirement Engineering for a Cloud System for Automated and Networked Vehicles. In 2nd International Workshop on Autonomous Systems Design (ASD 2020). Open Access Series in Informatics (OASIcs), Volume 79, pp. 4:1-4:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{mokhtarian_et_al:OASIcs.ASD.2020.4,
  author =	{Mokhtarian, Armin and Kampmann, Alexandru and Alrifaee, Bassam and Kowalewski, Stefan and Lampe, Bastian and Eckstein, Lutz},
  title =	{{Agile Requirement Engineering for a Cloud System for Automated and Networked Vehicles}},
  booktitle =	{2nd International Workshop on Autonomous Systems Design (ASD 2020)},
  pages =	{4:1--4:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-141-2},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{79},
  editor =	{Steinhorst, Sebastian and Deshmukh, Jyotirmoy V.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ASD.2020.4},
  URN =		{urn:nbn:de:0030-drops-125983},
  doi =		{10.4230/OASIcs.ASD.2020.4},
  annote =	{Keywords: agile requirements engineering, cloud architecture, automated vehicles}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.29
Groups with ALOGTIME-Hard Word Problems and PSPACE-Complete Circuit Value Problems

Authors: Laurent Bartholdi, Michael Figelius, Markus Lohrey, and Armin Weiß

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
We give lower bounds on the complexity of the word problem of certain non-solvable groups: for a large class of non-solvable infinite groups, including in particular free groups, Grigorchuk’s group and Thompson’s groups, we prove that their word problem is ALOGTIME-hard. For some of these groups (including Grigorchuk’s group and Thompson’s groups) we prove that the circuit value problem (which is equivalent to the circuit evaluation problem) is PSPACE-complete.
Cite as

Laurent Bartholdi, Michael Figelius, Markus Lohrey, and Armin Weiß. Groups with ALOGTIME-Hard Word Problems and PSPACE-Complete Circuit Value Problems. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 29:1-29:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bartholdi_et_al:LIPIcs.CCC.2020.29,
  author =	{Bartholdi, Laurent and Figelius, Michael and Lohrey, Markus and Wei{\ss}, Armin},
  title =	{{Groups with ALOGTIME-Hard Word Problems and PSPACE-Complete Circuit Value Problems}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{29:1--29:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.29},
  URN =		{urn:nbn:de:0030-drops-125814},
  doi =		{10.4230/LIPIcs.CCC.2020.29},
  annote =	{Keywords: NC^1-hardness, word problem, G-programs, straight-line programs, non-solvable groups, self-similar groups, Thompson’s groups, Grigorchuk’s group}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2020.102
Hardness of Equations over Finite Solvable Groups Under the Exponential Time Hypothesis

Authors: Armin Weiß

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

Abstract
Goldmann and Russell (2002) initiated the study of the complexity of the equation satisfiability problem in finite groups by showing that it is in 𝖯 for nilpotent groups while it is 𝖭𝖯-complete for non-solvable groups. Since then, several results have appeared showing that the problem can be solved in polynomial time in certain solvable groups of Fitting length two. In this work, we present the first lower bounds for the equation satisfiability problem in finite solvable groups: under the assumption of the exponential time hypothesis, we show that it cannot be in 𝖯 for any group of Fitting length at least four and for certain groups of Fitting length three. Moreover, the same hardness result applies to the equation identity problem.
Cite as

Armin Weiß. Hardness of Equations over Finite Solvable Groups Under the Exponential Time Hypothesis. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 102:1-102:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{wei:LIPIcs.ICALP.2020.102,
  author =	{Wei{\ss}, Armin},
  title =	{{Hardness of Equations over Finite Solvable Groups Under the Exponential Time Hypothesis}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{102:1--102:19},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.102},
  URN =		{urn:nbn:de:0030-drops-125093},
  doi =		{10.4230/LIPIcs.ICALP.2020.102},
  annote =	{Keywords: equations in groups, solvable groups, exponential time hypothesis}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.6
An Automaton Group with PSPACE-Complete Word Problem

Authors: Jan Philipp Wächter and Armin Weiß

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

Abstract
We construct an automaton group with a PSPACE-complete word problem, proving a conjecture due to Steinberg. Additionally, the constructed group has a provably more difficult, namely EXPSPACE-complete, compressed word problem. Our construction directly simulates the computation of a Turing machine in an automaton group and, therefore, seems to be quite versatile. It combines two ideas: the first one is a construction used by D'Angeli, Rodaro and the first author to obtain an inverse automaton semigroup with a PSPACE-complete word problem and the second one is to utilize a construction used by Barrington to simulate circuits of bounded degree and logarithmic depth in the group of even permutations over five elements.
Cite as

Jan Philipp Wächter and Armin Weiß. An Automaton Group with PSPACE-Complete Word Problem. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{wachter_et_al:LIPIcs.STACS.2020.6,
  author =	{W\"{a}chter, Jan Philipp and Wei{\ss}, Armin},
  title =	{{An Automaton Group with PSPACE-Complete Word Problem}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{6:1--6:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.6},
  URN =		{urn:nbn:de:0030-drops-118674},
  doi =		{10.4230/LIPIcs.STACS.2020.6},
  annote =	{Keywords: automaton group, word problem, PSPACE, compressed word problem}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.43
The Power Word Problem

Authors: Markus Lohrey and Armin Weiß

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

Abstract
In this work we introduce a new succinct variant of the word problem in a finitely generated group G, which we call the power word problem: the input word may contain powers p^x, where p is a finite word over generators of G and x is a binary encoded integer. The power word problem is a restriction of the compressed word problem, where the input word is represented by a straight-line program (i.e., an algebraic circuit over G). The main result of the paper states that the power word problem for a finitely generated free group F is AC^0-Turing-reducible to the word problem for F. Moreover, the following hardness result is shown: For a wreath product G Wr Z, where G is either free of rank at least two or finite non-solvable, the power word problem is complete for coNP. This contrasts with the situation where G is abelian: then the power word problem is shown to be in TC^0.
Cite as

Markus Lohrey and Armin Weiß. The Power Word Problem. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 43:1-43:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lohrey_et_al:LIPIcs.MFCS.2019.43,
  author =	{Lohrey, Markus and Wei{\ss}, Armin},
  title =	{{The Power Word Problem}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{43:1--43: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.43},
  URN =		{urn:nbn:de:0030-drops-109871},
  doi =		{10.4230/LIPIcs.MFCS.2019.43},
  annote =	{Keywords: word problem, compressed word problem, free groups}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.18
ThingsMigrate: Platform-Independent Migration of Stateful JavaScript IoT Applications

Authors: Julien Gascon-Samson, Kumseok Jung, Shivanshu Goyal, Armin Rezaiean-Asel, and Karthik Pattabiraman

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
The Internet of Things (IoT) has gained wide popularity both in academic and industrial contexts. As IoT devices become increasingly powerful, they can run more and more complex applications written in higher-level languages, such as JavaScript. However, by their nature, IoT devices are subject to resource constraints, which require applications to be dynamically migrated between devices (and the cloud). Further, IoT applications are also becoming more stateful, and hence we need to save their state during migration transparently to the programmer. In this paper, we present ThingsMigrate, a middleware providing VM-independent migration of stateful JavaScript applications across IoT devices. ThingsMigrate captures and reconstructs the internal JavaScript program state by instrumenting application code before run time, without modifying the underlying Virtual Machine (VM), thus providing platform and VM-independence. We evaluated ThingsMigrate against standard benchmarks, and over two IoT platforms and a cloud-like environment. We show that it can successfully migrate even highly CPU-intensive applications, with acceptable overheads (about 30%), and supports multiple migrations.
Cite as

Julien Gascon-Samson, Kumseok Jung, Shivanshu Goyal, Armin Rezaiean-Asel, and Karthik Pattabiraman. ThingsMigrate: Platform-Independent Migration of Stateful JavaScript IoT Applications. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 18:1-18:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gasconsamson_et_al:LIPIcs.ECOOP.2018.18,
  author =	{Gascon-Samson, Julien and Jung, Kumseok and Goyal, Shivanshu and Rezaiean-Asel, Armin and Pattabiraman, Karthik},
  title =	{{ThingsMigrate: Platform-Independent Migration of Stateful JavaScript IoT Applications}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{18:1--18:33},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.18},
  URN =		{urn:nbn:de:0030-drops-92236},
  doi =		{10.4230/LIPIcs.ECOOP.2018.18},
  annote =	{Keywords: JavaScript, Code Migration, Closures, IoT, Node.js}
}
  • Refine by Author
  • 9 Weiß, Armin
  • 7 Biere, Armin
  • 3 Fügenschuh, Armin
  • 2 Friedrich, Tobias
  • 2 Ganesh, Vijay
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Automated reasoning
  • 4 Theory of computation → Problems, reductions and completeness
  • 2 Mathematics of computing → Combinatorics
  • 2 Theory of computation → Circuit complexity
  • 2 Theory of computation → Complexity classes
  • Show More...

  • Refine by Keyword
  • 4 word problem
  • 3 SAT
  • 3 SAT solving
  • 2 compressed word problem
  • 2 computational complexity
  • Show More...

  • Refine by Type
  • 29 document

  • Refine by Publication Year
  • 5 2020
  • 4 2023
  • 3 2018
  • 3 2022
  • 2 2006
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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