30 Search Results for "Schweitzer, Pascal"

Document
DOI: 10.4230/LIPIcs.CP.2024.3
The Complexity of Symmetry Breaking Beyond Lex-Leader

Authors: Markus Anders, Sofia Brenner, and Gaurav Rattan

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Symmetry breaking is a widely popular approach to enhance solvers in constraint programming, such as those for SAT or MIP. Symmetry breaking predicates (SBPs) typically impose an order on variables and single out the lexicographic leader (lex-leader) in each orbit of assignments. Although it is NP-hard to find complete lex-leader SBPs, incomplete lex-leader SBPs are widely used in practice. In this paper, we investigate the complexity of computing complete SBPs, lex-leader or otherwise, for SAT. Our main result proves a natural barrier for efficiently computing SBPs: efficient certification of graph non-isomorphism. Our results explain the difficulty of obtaining short SBPs for important CP problems, such as matrix-models with row-column symmetries and graph generation problems. Our results hold even when SBPs are allowed to introduce additional variables. We show polynomial upper bounds for breaking certain symmetry groups, namely automorphism groups of trees and wreath products of groups with efficient SBPs.
Cite as

Markus Anders, Sofia Brenner, and Gaurav Rattan. The Complexity of Symmetry Breaking Beyond Lex-Leader. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.CP.2024.3,
  author =	{Anders, Markus and Brenner, Sofia and Rattan, Gaurav},
  title =	{{The Complexity of Symmetry Breaking Beyond Lex-Leader}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{3:1--3:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.3},
  URN =		{urn:nbn:de:0030-drops-206881},
  doi =		{10.4230/LIPIcs.CP.2024.3},
  annote =	{Keywords: symmetry breaking, boolean satisfiability, matrix models, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.4
Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability

Authors: Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.
Cite as

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berg_et_al:LIPIcs.CP.2024.4,
  author =	{Berg, Jeremias and Bogaerts, Bart and Nordstr\"{o}m, Jakob and Oertel, Andy and Paxian, Tobias and Vandesande, Dieter},
  title =	{{Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{4:1--4:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.4},
  URN =		{urn:nbn:de:0030-drops-206895},
  doi =		{10.4230/LIPIcs.CP.2024.4},
  annote =	{Keywords: proof logging, certifying algorithms, MaxSAT, solution-improving search, SAT-UNSAT, maximum satisfiability, combinatorial optimization, certification, pseudo-Boolean}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.9
Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms

Authors: Emir Demirović, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordström, Andy Oertel, and Konstantin Sidorov

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Pseudo-Boolean proof logging has been used successfully to provide certificates of optimality from a variety of constraint- and satisifability-style solvers that combine reasoning with a backtracking or clause-learning search. Another paradigm, occurring in dynamic programming and decision diagram solving, instead reasons about partial states and possible transitions between them. We describe a framework for generating clean and efficient pseudo-Boolean proofs for these kinds of algorithm, and use it to produce certifying algorithms for knapsack, longest path, and interval scheduling. Because we use a common proof system, we can also reason about hybrid solving algorithms: we demonstrate this by providing proof logging for a dynamic programming based knapsack propagator inside a constraint programming solver.
Cite as

Emir Demirović, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordström, Andy Oertel, and Konstantin Sidorov. Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{demirovic_et_al:LIPIcs.CP.2024.9,
  author =	{Demirovi\'{c}, Emir and McCreesh, Ciaran and McIlree, Matthew J. and Nordstr\"{o}m, Jakob and Oertel, Andy and Sidorov, Konstantin},
  title =	{{Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.9},
  URN =		{urn:nbn:de:0030-drops-206948},
  doi =		{10.4230/LIPIcs.CP.2024.9},
  annote =	{Keywords: Proof logging, dynamic programming, decision diagrams}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.55
Minimal Obstructions to C₅-Coloring in Hereditary Graph Classes

Authors: Jan Goedgebeur, Jorik Jooken, Karolina Okrasa, Paweł Rzążewski, and Oliver Schaudt

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

Abstract
For graphs G and H, an H-coloring of G is an edge-preserving mapping from V(G) to V(H). Note that if H is the triangle, then H-colorings are equivalent to 3-colorings. In this paper we are interested in the case that H is the five-vertex cycle C₅. A minimal obstruction to C₅-coloring is a graph that does not have a C₅-coloring, but every proper induced subgraph thereof has a C₅-coloring. In this paper we are interested in minimal obstructions to C₅-coloring in F-free graphs, i.e., graphs that exclude some fixed graph F as an induced subgraph. Let P_t denote the path on t vertices, and let S_{a,b,c} denote the graph obtained from paths P_{a+1},P_{b+1},P_{c+1} by identifying one of their endvertices. We show that there is only a finite number of minimal obstructions to C₅-coloring among F-free graphs, where F ∈ {P₈, S_{2,2,1}, S_{3,1,1}} and explicitly determine all such obstructions. This extends the results of Kamiński and Pstrucha [Discr. Appl. Math. 261, 2019] who proved that there is only a finite number of P₇-free minimal obstructions to C₅-coloring, and of Dębski et al. [ISAAC 2022 Proc.] who showed that the triangle is the unique S_{2,1,1}-free minimal obstruction to C₅-coloring. We complement our results with a construction of an infinite family of minimal obstructions to C₅-coloring, which are simultaneously P_{13}-free and S_{2,2,2}-free. We also discuss infinite families of F-free minimal obstructions to H-coloring for other graphs H.
Cite as

Jan Goedgebeur, Jorik Jooken, Karolina Okrasa, Paweł Rzążewski, and Oliver Schaudt. Minimal Obstructions to C₅-Coloring in Hereditary Graph Classes. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 55:1-55:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{goedgebeur_et_al:LIPIcs.MFCS.2024.55,
  author =	{Goedgebeur, Jan and Jooken, Jorik and Okrasa, Karolina and Rz\k{a}\.{z}ewski, Pawe{\l} and Schaudt, Oliver},
  title =	{{Minimal Obstructions to C₅-Coloring in Hereditary Graph Classes}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{55:1--55:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.55},
  URN =		{urn:nbn:de:0030-drops-206110},
  doi =		{10.4230/LIPIcs.MFCS.2024.55},
  annote =	{Keywords: graph homomorphism, critical graphs, hereditary graph classes}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.82
An Algorithmic Meta Theorem for Homomorphism Indistinguishability

Authors: Tim Seppelt

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

Abstract
Two graphs G and H are homomorphism indistinguishable over a family of graphs ℱ if for all graphs F ∈ ℱ the number of homomorphisms from F to G is equal to the number of homomorphism from F to H. Many natural equivalence relations comparing graphs such as (quantum) isomorphism, cospectrality, and logical equivalences can be characterised as homomorphism indistinguishability relations over various graph classes. The wealth of such results motivates a more fundamental study of homomorphism indistinguishability. From a computational perspective, the central object of interest is the decision problem HomInd(ℱ) which asks to determine whether two input graphs G and H are homomorphism indistinguishable over a fixed graph class ℱ. The problem HomInd(ℱ) is known to be decidable only for few graph classes ℱ. Due to a conjecture by Roberson (2022) and results by Seppelt (MFCS 2023), homomorphism indistinguishability relations over minor-closed graph classes are of special interest. We show that HomInd(ℱ) admits a randomised polynomial-time algorithm for every minor-closed graph class ℱ of bounded treewidth. This result extends to a version of HomInd where the graph class ℱ is specified by a sentence in counting monadic second-order logic and a bound k on the treewidth, which are given as input. For fixed k, this problem is randomised fixed-parameter tractable. If k is part of the input, then it is coNP- and coW[1]-hard. Addressing a problem posed by Berkholz (2012), we show coNP-hardness by establishing that deciding indistinguishability under the k-dimensional Weisfeiler-Leman algorithm is coNP-hard when k is part of the input.
Cite as

Tim Seppelt. An Algorithmic Meta Theorem for Homomorphism Indistinguishability. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 82:1-82:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{seppelt:LIPIcs.MFCS.2024.82,
  author =	{Seppelt, Tim},
  title =	{{An Algorithmic Meta Theorem for Homomorphism Indistinguishability}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{82:1--82:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.82},
  URN =		{urn:nbn:de:0030-drops-206387},
  doi =		{10.4230/LIPIcs.MFCS.2024.82},
  annote =	{Keywords: homomorphism indistinguishability, graph homomorphism, graph minor, recognisability, randomised algorithm, Courcelle’s Theorem}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.4
Satsuma: Structure-Based Symmetry Breaking in SAT

Authors: Markus Anders, Sofia Brenner, and Gaurav Rattan

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Symmetry reduction is crucial for solving many interesting SAT instances in practice. Numerous approaches have been proposed, which try to strike a balance between symmetry reduction and computational overhead. Arguably the most readily applicable method is the computation of static symmetry breaking constraints: a constraint restricting the search-space to non-symmetrical solutions is added to a given SAT instance. A distinct advantage of static symmetry breaking is that the SAT solver itself is not modified. A disadvantage is that the strength of symmetry reduction is usually limited. In order to boost symmetry reduction, the state-of-the-art tool BreakID [Devriendt et. al] pioneered the identification and tailored breaking of a particular substructure of symmetries, the so-called row interchangeability groups. In this paper, we propose a new symmetry breaking tool called satsuma. The core principle of our tool is to exploit more diverse but frequently occurring symmetry structures. This is enabled by new practical detection algorithms for row interchangeability, row-column symmetry, Johnson symmetry, and various combinations. Based on the resulting structural description, we then produce symmetry breaking constraints. We compare this new approach to BreakID on a range of instance families exhibiting symmetry. Our benchmarks suggest improved symmetry reduction in the presence of Johnson symmetry and comparable performance in the presence of row-column symmetry. Moreover, our implementation runs significantly faster, even though it identifies more diverse structures.
Cite as

Markus Anders, Sofia Brenner, and Gaurav Rattan. Satsuma: Structure-Based Symmetry Breaking in SAT. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SAT.2024.4,
  author =	{Anders, Markus and Brenner, Sofia and Rattan, Gaurav},
  title =	{{Satsuma: Structure-Based Symmetry Breaking in SAT}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.4},
  URN =		{urn:nbn:de:0030-drops-205269},
  doi =		{10.4230/LIPIcs.SAT.2024.4},
  annote =	{Keywords: symmetry breaking, boolean satisfiability, graph isomorphism}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.78
Isomorphism for Tournaments of Small Twin Width

Authors: Martin Grohe and Daniel Neuen

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We prove that isomorphism of tournaments of twin width at most k can be decided in time k^O(log k) n^O(1). This implies that the isomorphism problem for classes of tournaments of bounded or moderately growing twin width is in polynomial time. By comparison, there are classes of undirected graphs of bounded twin width that are isomorphism complete, that is, the isomorphism problem for the classes is as hard as the general graph isomorphism problem. Twin width is a graph parameter that has been introduced only recently (Bonnet et al., FOCS 2020), but has received a lot of attention in structural graph theory since then. On directed graphs, it is functionally smaller than clique width. We prove that on tournaments (but not on general directed graphs) it is also functionally smaller than directed tree width (and thus, the same also holds for cut width and directed path width). Hence, our result implies that tournament isomorphism testing is also fixed-parameter tractable when parameterized by any of these parameters. Our isomorphism algorithm heavily employs group-theoretic techniques. This seems to be necessary: as a second main result, we show that the combinatorial Weisfeiler-Leman algorithm does not decide isomorphism of tournaments of twin width at most 35 if its dimension is o(n). (Throughout this abstract, n is the order of the input graphs.)
Cite as

Martin Grohe and Daniel Neuen. Isomorphism for Tournaments of Small Twin Width. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 78:1-78:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{grohe_et_al:LIPIcs.ICALP.2024.78,
  author =	{Grohe, Martin and Neuen, Daniel},
  title =	{{Isomorphism for Tournaments of Small Twin Width}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{78:1--78:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.78},
  URN =		{urn:nbn:de:0030-drops-202216},
  doi =		{10.4230/LIPIcs.ICALP.2024.78},
  annote =	{Keywords: tournament isomorphism, twin width, fixed-parameter tractability, Weisfeiler-Leman algorithm}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.152
On Homomorphism Indistinguishability and Hypertree Depth

Authors: Benjamin Scheidt

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
GC^k is a logic introduced by Scheidt and Schweikardt (2023) to express properties of hypergraphs. It is similar to first-order logic with counting quantifiers (C) adapted to the hypergraph setting. It has distinct sets of variables for vertices and for hyperedges and requires vertex variables to be guarded by hyperedge variables on every quantification. We prove that two hypergraphs G, H satisfy the same sentences in the logic GC^k with guard depth at most k if, and only if, they are homomorphism indistinguishable over the class of hypergraphs of strict hypertree depth at most k. This lifts the analogous result for tree depth ≤ k and sentences of first-order logic with counting quantifiers of quantifier rank at most k due to Grohe (2020) from graphs to hypergraphs. The guard depth of a formula is the quantifier rank with respect to hyperedge variables, and strict hypertree depth is a restriction of hypertree depth as defined by Adler, Gavenčiak and Klimošová (2012). To justify this restriction, we show that for every H, the strict hypertree depth of H is at most 1 larger than its hypertree depth, and we give additional evidence that strict hypertree depth can be viewed as a reasonable generalisation of tree depth for hypergraphs.
Cite as

Benjamin Scheidt. On Homomorphism Indistinguishability and Hypertree Depth. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 152:1-152:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{scheidt:LIPIcs.ICALP.2024.152,
  author =	{Scheidt, Benjamin},
  title =	{{On Homomorphism Indistinguishability and Hypertree Depth}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{152:1--152:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.152},
  URN =		{urn:nbn:de:0030-drops-202958},
  doi =		{10.4230/LIPIcs.ICALP.2024.152},
  annote =	{Keywords: homomorphism indistinguishability, counting logics, guarded logics, hypergraphs, incidence graphs, tree depth, elimination forest, hypertree width}
}
Document
DOI: 10.4230/LIPIcs.ESA.2023.11
Exploration of Graphs with Excluded Minors

Authors: Júlia Baligács, Yann Disser, Irene Heinrich, and Pascal Schweitzer

Published in: LIPIcs, Volume 274, 31st Annual European Symposium on Algorithms (ESA 2023)

Abstract
We study the online graph exploration problem proposed by Kalyanasundaram and Pruhs (1994) and prove a constant competitive ratio on minor-free graphs. This result encompasses and significantly extends the graph classes that were previously known to admit a constant competitive ratio. The main ingredient of our proof is that we find a connection between the performance of the particular exploration algorithm Blocking and the existence of light spanners. Conversely, we exploit this connection to construct light spanners of bounded genus graphs. In particular, we achieve a lightness that improves on the best known upper bound for genus g ≥ 1 and recovers the known tight bound for the planar case (g = 0).
Cite as

Júlia Baligács, Yann Disser, Irene Heinrich, and Pascal Schweitzer. Exploration of Graphs with Excluded Minors. In 31st Annual European Symposium on Algorithms (ESA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 274, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baligacs_et_al:LIPIcs.ESA.2023.11,
  author =	{Balig\'{a}cs, J\'{u}lia and Disser, Yann and Heinrich, Irene and Schweitzer, Pascal},
  title =	{{Exploration of Graphs with Excluded Minors}},
  booktitle =	{31st Annual European Symposium on Algorithms (ESA 2023)},
  pages =	{11:1--11:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-295-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{274},
  editor =	{G{\o}rtz, Inge Li and Farach-Colton, Martin and Puglisi, Simon J. 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.2023.11},
  URN =		{urn:nbn:de:0030-drops-186644},
  doi =		{10.4230/LIPIcs.ESA.2023.11},
  annote =	{Keywords: online algorithms, competitive analysis, graph exploration, graph spanners, minor-free graphs, bounded genus graphs}
}
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.ESA.2022.27
A Systematic Study of Isomorphism Invariants of Finite Groups via the Weisfeiler-Leman Dimension

Authors: Jendrik Brachter and Pascal Schweitzer

Published in: LIPIcs, Volume 244, 30th Annual European Symposium on Algorithms (ESA 2022)

Abstract
We investigate the relationship between various isomorphism invariants for finite groups. Specifically, we use the Weisfeiler-Leman dimension (WL) to characterize, compare and quantify the effectiveness and complexity of invariants for group isomorphism. It turns out that a surprising number of invariants and characteristic subgroups that are classic to group theory can be detected and identified by a low dimensional Weisfeiler-Leman algorithm. These include the center, the inner automorphism group, the commutator subgroup and the derived series, the abelian radical, the solvable radical, the Fitting group and π-radicals. A low dimensional WL-algorithm additionally determines the isomorphism type of the socle as well as the factors in the derives series and the upper and lower central series. We also analyze the behavior of the WL-algorithm for group extensions and prove that a low dimensional WL-algorithm determines the isomorphism types of the composition factors of a group. Finally we develop a new tool to define a canonical maximal central decomposition for groups. This allows us to show that the Weisfeiler-Leman dimension of a group is at most one larger than the dimensions of its direct indecomposable factors. In other words the Weisfeiler-Leman dimension increases by at most 1 when taking direct products.
Cite as

Jendrik Brachter and Pascal Schweitzer. A Systematic Study of Isomorphism Invariants of Finite Groups via the Weisfeiler-Leman Dimension. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brachter_et_al:LIPIcs.ESA.2022.27,
  author =	{Brachter, Jendrik and Schweitzer, Pascal},
  title =	{{A Systematic Study of Isomorphism Invariants of Finite Groups via the Weisfeiler-Leman Dimension}},
  booktitle =	{30th Annual European Symposium on Algorithms (ESA 2022)},
  pages =	{27:1--27:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-247-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{244},
  editor =	{Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva 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.2022.27},
  URN =		{urn:nbn:de:0030-drops-169653},
  doi =		{10.4230/LIPIcs.ESA.2022.27},
  annote =	{Keywords: group isomorphism problem, Weisfeiler-Leman algorithms, group invariants, direct product decompositions}
}
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.CSL.2022.36
Number of Variables for Graph Differentiation and the Resolution of GI Formulas

Authors: Jacobo Torán and Florian Wörz

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

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

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

Copy BibTex To Clipboard

@InProceedings{toran_et_al:LIPIcs.CSL.2022.36,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Number of Variables for Graph Differentiation and the Resolution of GI Formulas}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.36},
  URN =		{urn:nbn:de:0030-drops-157564},
  doi =		{10.4230/LIPIcs.CSL.2022.36},
  annote =	{Keywords: Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, k-variable fragment first-order logic 𝔏\underlinek, Immerman’s Pebble Game, Symmetry Rule, SRC-1}
}
Document
DOI: 10.4230/LIPIcs.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}
}
  • Refine by Author
  • 17 Schweitzer, Pascal
  • 9 Anders, Markus
  • 3 Neuen, Daniel
  • 2 Brachter, Jendrik
  • 2 Brenner, Sofia
  • Show More...

  • Refine by Classification
  • 8 Mathematics of computing → Graph algorithms
  • 4 Theory of computation → Complexity theory and logic
  • 4 Theory of computation → Design and analysis of algorithms
  • 4 Theory of computation → Graph algorithms analysis
  • 4 Theory of computation → Online algorithms
  • Show More...

  • Refine by Keyword
  • 12 graph isomorphism
  • 4 boolean satisfiability
  • 2 Graph Isomorphism
  • 2 Graph isomorphism
  • 2 Lower bounds
  • Show More...

  • Refine by Type
  • 30 document

  • Refine by Publication Year
  • 8 2024
  • 6 2021
  • 3 2022
  • 3 2023
  • 2 2016
  • 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