7 Search Results for "Anders, Markus"

Document
DOI: 10.4230/LIPIcs.SAT.2023.1
Algorithms Transcending the SAT-Symmetry Interface

Authors: Markus Anders, Pascal Schweitzer, and Mate Soos

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

Abstract
Dedicated treatment of symmetries in satisfiability problems (SAT) is indispensable for solving various classes of instances arising in practice. However, the exploitation of symmetries usually takes a black box approach. Typically, off-the-shelf external, general-purpose symmetry detection tools are invoked to compute symmetry groups of a formula. The groups thus generated are a set of permutations passed to a separate tool to perform further analyzes to understand the structure of the groups. The result of this second computation is in turn used for tasks such as static symmetry breaking or dynamic pruning of the search space. Within this pipeline of tools, the detection and analysis of symmetries typically incurs the majority of the time overhead for symmetry exploitation. In this paper we advocate for a more holistic view of what we call the SAT-symmetry interface. We formulate a computational setting, centered around a new concept of joint graph/group pairs, to analyze and improve the detection and analysis of symmetries. Using our methods, no information is lost performing computational tasks lying on the SAT-symmetry interface. Having access to the entire input allows for simpler, yet efficient algorithms. Specifically, we devise algorithms and heuristics for computing finest direct disjoint decompositions, finding equivalent orbits, and finding natural symmetric group actions. Our algorithms run in what we call instance-quasi-linear time, i.e., almost linear time in terms of the input size of the original formula and the description length of the symmetry group returned by symmetry detection tools. Our algorithms improve over both heuristics used in state-of-the-art symmetry exploitation tools, as well as theoretical general-purpose algorithms.
Cite as

Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms Transcending the SAT-Symmetry Interface. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1:1-1:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SAT.2023.1,
  author =	{Anders, Markus and Schweitzer, Pascal and Soos, Mate},
  title =	{{Algorithms Transcending the SAT-Symmetry Interface}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{1:1--1:21},
  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.1},
  URN =		{urn:nbn:de:0030-drops-184635},
  doi =		{10.4230/LIPIcs.SAT.2023.1},
  annote =	{Keywords: boolean satisfiability, symmetry exploitation, computational group theory}
}
Document
DOI: 10.4230/LIPIcs.SEA.2023.1
Engineering a Preprocessor for Symmetry Detection

Authors: Markus Anders, Pascal Schweitzer, and Julian Stieß

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
State-of-the-art solvers for symmetry detection in combinatorial objects are becoming increasingly sophisticated software libraries. Most of the solvers were initially designed with inputs from combinatorics in mind (nauty, bliss, Traces, dejavu). They excel at dealing with a complicated core of the input. Others focus on practical instances that exhibit sparsity. They excel at dealing with comparatively easy but extremely large substructures of the input (saucy). In practice, these differences manifest in significantly diverging performances on different types of graph classes. We engineer a preprocessor for symmetry detection. The result is a tool designed to shrink sparse, large substructures of the input graph. On most of the practical instances, the preprocessor improves the overall running time significantly for many of the state-of-the-art solvers. At the same time, our benchmarks show that the additional overhead is negligible. Overall we obtain single algorithms with competitive performance across all benchmark graphs. As such, the preprocessor bridges the disparity between solvers that focus on combinatorial graphs and large practical graphs. In fact, on most of the practical instances the combined setup significantly outperforms previous state-of-the-art.
Cite as

Markus Anders, Pascal Schweitzer, and Julian Stieß. Engineering a Preprocessor for Symmetry Detection. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 1:1-1:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SEA.2023.1,
  author =	{Anders, Markus and Schweitzer, Pascal and Stie{\ss}, Julian},
  title =	{{Engineering a Preprocessor for Symmetry Detection}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.1},
  URN =		{urn:nbn:de:0030-drops-183511},
  doi =		{10.4230/LIPIcs.SEA.2023.1},
  annote =	{Keywords: graph isomorphism, automorphism groups, symmetry detection, preprocessors}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.1
SAT Preprocessors and Symmetry

Authors: Markus Anders

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

Abstract
Exploitation of symmetries is an indispensable approach to solve certain classes of difficult SAT instances. Numerous techniques for the use of symmetry in SAT have evolved over the past few decades. But no matter how symmetries are used precisely, they have to be detected first. We investigate how to detect more symmetry, faster. The initial idea is to reap the benefits of SAT preprocessing for symmetry detection. As it turns out, applying an off-the-shelf preprocessor before handling symmetry runs into problems: the preprocessor can haphazardly remove symmetry from formulas, severely impeding symmetry exploitation. Our main contribution is a theoretical framework that captures the relationship of SAT preprocessing techniques and symmetry. Based on this, we create a symmetry-aware preprocessor that can be applied safely before handling symmetry. We then demonstrate that applying the preprocessor does not only substantially decrease symmetry detection and breaking times, but also uncovers hidden symmetry not detectable in the original instances. Overall, we depart the conventional view of treating symmetry detection as a black-box, presenting a new application-specific approach to symmetry detection in SAT.
Cite as

Markus Anders. SAT Preprocessors and Symmetry. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 1:1-1:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{anders:LIPIcs.SAT.2022.1,
  author =	{Anders, Markus},
  title =	{{SAT Preprocessors and Symmetry}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{1:1--1:20},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.1},
  URN =		{urn:nbn:de:0030-drops-166752},
  doi =		{10.4230/LIPIcs.SAT.2022.1},
  annote =	{Keywords: boolean satisfiability, symmetry exploitation, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2021.24
A Characterization of Individualization-Refinement Trees

Authors: Markus Anders, Jendrik Brachter, and Pascal Schweitzer

Published in: LIPIcs, Volume 212, 32nd International Symposium on Algorithms and Computation (ISAAC 2021)

Abstract
Individualization-Refinement (IR) algorithms form the standard method and currently the only practical method for symmetry computations of graphs and combinatorial objects in general. Through backtracking, on each graph an IR-algorithm implicitly creates an IR-tree whose order is the determining factor of the running time of the algorithm. We give a precise and constructive characterization which trees are IR-trees. This characterization is applicable both when the tree is regarded as an uncolored object but also when regarded as a colored object where vertex colors stem from a node invariant. We also provide a construction that given a tree produces a corresponding graph whenever possible. This provides a constructive proof that our necessary conditions are also sufficient for the characterization.
Cite as

Markus Anders, Jendrik Brachter, and Pascal Schweitzer. A Characterization of Individualization-Refinement Trees. In 32nd International Symposium on Algorithms and Computation (ISAAC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 212, pp. 24:1-24:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.ISAAC.2021.24,
  author =	{Anders, Markus and Brachter, Jendrik and Schweitzer, Pascal},
  title =	{{A Characterization of Individualization-Refinement Trees}},
  booktitle =	{32nd International Symposium on Algorithms and Computation (ISAAC 2021)},
  pages =	{24:1--24:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-214-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{212},
  editor =	{Ahn, Hee-Kap and Sadakane, Kunihiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2021.24},
  URN =		{urn:nbn:de:0030-drops-154578},
  doi =		{10.4230/LIPIcs.ISAAC.2021.24},
  annote =	{Keywords: individualization refinement algorithms, backtracking trees, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.ESA.2021.6
Parallel Computation of Combinatorial Symmetries

Authors: Markus Anders and Pascal Schweitzer

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

Abstract
In practice symmetries of combinatorial structures are computed by transforming the structure into an annotated graph whose automorphisms correspond exactly to the desired symmetries. An automorphism solver is then employed to compute the automorphism group of the constructed graph. Such solvers have been developed for over 50 years, and highly efficient sequential, single core tools are available. However no competitive parallel tools are available for the task. We introduce a new parallel randomized algorithm that is based on a modification of the individualization-refinement paradigm used by sequential solvers. The use of randomization crucially enables parallelization. We report extensive benchmark results that show that our solver is competitive to state-of-the-art solvers on a single thread, while scaling remarkably well with the use of more threads. This results in order-of-magnitude improvements on many graph classes over state-of-the-art solvers. In fact, our tool is the first parallel graph automorphism tool that outperforms current sequential tools.
Cite as

Markus Anders and Pascal Schweitzer. Parallel Computation of Combinatorial Symmetries. In 29th Annual European Symposium on Algorithms (ESA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 204, pp. 6:1-6:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.ESA.2021.6,
  author =	{Anders, Markus and Schweitzer, Pascal},
  title =	{{Parallel Computation of Combinatorial Symmetries}},
  booktitle =	{29th Annual European Symposium on Algorithms (ESA 2021)},
  pages =	{6:1--6:18},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2021.6},
  URN =		{urn:nbn:de:0030-drops-145875},
  doi =		{10.4230/LIPIcs.ESA.2021.6},
  annote =	{Keywords: graph isomorphism, automorphism groups, algorithm engineering, parallel algorithms}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2021.15
Comparative Design-Choice Analysis of Color Refinement Algorithms Beyond the Worst Case

Authors: Markus Anders, Pascal Schweitzer, and Florian Wetzels

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

Abstract
Color refinement is a crucial subroutine in symmetry detection in theory as well as practice. It has further applications in machine learning and in computational problems from linear algebra. While tight lower bounds for the worst case complexity are known [Berkholz, Bonsma, Grohe, ESA2013] no comparative analysis of design choices for color refinement algorithms is available. We devise two models within which we can compare color refinement algorithms using formal methods, an online model and an approximation model. We use these to show that no online algorithm is competitive beyond a logarithmic factor and no algorithm can approximate the optimal color refinement splitting scheme beyond a logarithmic factor. We also directly compare strategies used in practice showing that, on some graphs, queue based strategies outperform stack based ones by a logarithmic factor and vice versa. Similar results hold for strategies based on priority queues.
Cite as

Markus Anders, Pascal Schweitzer, and Florian Wetzels. Comparative Design-Choice Analysis of Color Refinement Algorithms Beyond the Worst Case. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 15:1-15:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.ICALP.2021.15,
  author =	{Anders, Markus and Schweitzer, Pascal and Wetzels, Florian},
  title =	{{Comparative Design-Choice Analysis of Color Refinement Algorithms Beyond the Worst Case}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{15:1--15:15},
  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.15},
  URN =		{urn:nbn:de:0030-drops-140846},
  doi =		{10.4230/LIPIcs.ICALP.2021.15},
  annote =	{Keywords: Color refinement, Online algorithms, Graph isomorphism, Lower bounds}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2021.16
Search Problems in Trees with Symmetries: Near Optimal Traversal Strategies for Individualization-Refinement Algorithms

Authors: Markus Anders and Pascal Schweitzer

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

Abstract
We define a search problem on trees that closely captures the backtracking behavior of all current practical graph isomorphism algorithms. Given two trees with colored leaves, the goal is to find two leaves of matching color, one in each of the trees. The trees are subject to an invariance property which promises that for every pair of leaves of equal color there must be a symmetry (or an isomorphism) that maps one leaf to the other. We describe a randomized algorithm with errors for which the number of visited nodes is quasilinear in the square root of the size of the smaller of the two trees. For inputs of bounded degree, we develop a Las Vegas algorithm with a similar running time. We prove that these results are optimal up to logarithmic factors. For this, we show a lower bound for randomized algorithms on inputs of bounded degree that is the square root of the tree sizes. For inputs of unbounded degree, we show a linear lower bound for Las Vegas algorithms. For deterministic algorithms we can prove a linear bound even for inputs of bounded degree. This shows why randomized algorithms outperform deterministic ones. Our results explain why the randomized "breadth-first with intermixed experimental path" search strategy of the isomorphism tool Traces (Piperno 2008) is often superior to the depth-first search strategy of other tools such as nauty (McKay 1977) or bliss (Junttila, Kaski 2007). However, our algorithm also provides a new traversal strategy, which is theoretically near optimal and which has better worst case behavior than traversal strategies that have previously been used.
Cite as

Markus Anders and Pascal Schweitzer. Search Problems in Trees with Symmetries: Near Optimal Traversal Strategies for Individualization-Refinement Algorithms. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 16:1-16:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.ICALP.2021.16,
  author =	{Anders, Markus and Schweitzer, Pascal},
  title =	{{Search Problems in Trees with Symmetries: Near Optimal Traversal Strategies for Individualization-Refinement Algorithms}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{16:1--16:21},
  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.16},
  URN =		{urn:nbn:de:0030-drops-140853},
  doi =		{10.4230/LIPIcs.ICALP.2021.16},
  annote =	{Keywords: Online algorithms, Graph isomorphism, Lower bounds}
}
  • Refine by Author
  • 7 Anders, Markus
  • 6 Schweitzer, Pascal
  • 1 Brachter, Jendrik
  • 1 Soos, Mate
  • 1 Stieß, Julian
  • Show More...

  • Refine by Classification
  • 4 Mathematics of computing → Graph algorithms
  • 3 Theory of computation → Design and analysis of algorithms
  • 2 Theory of computation → Graph algorithms analysis
  • 2 Theory of computation → Online algorithms
  • 1 Mathematics of computing → Trees
  • Show More...

  • Refine by Keyword
  • 4 graph isomorphism
  • 2 Graph isomorphism
  • 2 Lower bounds
  • 2 Online algorithms
  • 2 automorphism groups
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 4 2021
  • 2 2023
  • 1 2022

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact