3 Search Results for "Schürmann, Carsten"

Document

DOI: 10.4230/LIPIcs.SEA.2024.4

Separator Based Data Reduction for the Maximum Cut Problem

Authors: Jonas Charfreitag, Christine Dahn, Michael Kaibel, Philip Mayer, Petra Mutzel, and Lukas Schürmann

Published in: LIPIcs, Volume 301, 22nd International Symposium on Experimental Algorithms (SEA 2024)

Abstract

Preprocessing is an important ingredient for solving the maximum cut problem to optimality on real-world graphs. In our work, we derive a new framework for data reduction rules based on vertex separators. Vertex separators are sets of vertices, whose removal increases the number of connected components of a graph. Certain small separators can be found in linear time, allowing for an efficient combination of our framework with existing data reduction rules. Additionally, we complement known data reduction rules for triangles with a new one. In our computational experiments on established benchmark instances, we clearly show the effectiveness and efficiency of our proposed data reduction techniques. The resulting graphs are significantly smaller than in earlier studies and sometimes no vertex is left, so preprocessing has fully solved the instance to optimality. The introduced techniques are also shown to offer significant speedup potential for an exact state-of-the-art solver and to help a state-of-the-art heuristic to produce solutions of higher quality.

Cite as

Jonas Charfreitag, Christine Dahn, Michael Kaibel, Philip Mayer, Petra Mutzel, and Lukas Schürmann. Separator Based Data Reduction for the Maximum Cut Problem. In 22nd International Symposium on Experimental Algorithms (SEA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 301, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{charfreitag_et_al:LIPIcs.SEA.2024.4,
  author =	{Charfreitag, Jonas and Dahn, Christine and Kaibel, Michael and Mayer, Philip and Mutzel, Petra and Sch\"{u}rmann, Lukas},
  title =	{{Separator Based Data Reduction for the Maximum Cut Problem}},
  booktitle =	{22nd International Symposium on Experimental Algorithms (SEA 2024)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-325-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{301},
  editor =	{Liberti, Leo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2024.4},
  URN =		{urn:nbn:de:0030-drops-203698},
  doi =		{10.4230/LIPIcs.SEA.2024.4},
  annote =	{Keywords: Data Reduction, Maximum Cut, Vertex Separators}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2016.33

Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types

Authors: Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract

Wadler introduced Classical Processes (CP), a calculus based on a propositions-as-types correspondence between propositions of classical linear logic and session types. Carbone et al. introduced Multiparty Classical Processes, a calculus that generalises CP to multiparty session types, by replacing the duality of classical linear logic (relating two types) with a more general notion of coherence (relating an arbitrary number of types). This paper introduces variants of CP and MCP, plus a new intermediate calculus of Globally-governed Classical Processes (GCP). We show a tight relation between these three calculi, giving semantics-preserving translations from GCP to CP and from MCP to GCP. The translation from GCP to CP interprets a coherence proof as an arbiter process that mediates communications in a session, while MCP adds annotations that permit processes to communicate directly without centralised control.

Cite as

Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{carbone_et_al:LIPIcs.CONCUR.2016.33,
  author =	{Carbone, Marco and Lindley, Sam and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Wadler, Philip},
  title =	{{Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.33},
  URN =		{urn:nbn:de:0030-drops-61811},
  doi =		{10.4230/LIPIcs.CONCUR.2016.33},
  annote =	{Keywords: Multiparty Session Types, Linear Logic, Propositions as Types}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2015.412

Multiparty Session Types as Coherence Proofs

Authors: Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract

We propose a Curry-Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.

Cite as

Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty Session Types as Coherence Proofs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 412-426, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{carbone_et_al:LIPIcs.CONCUR.2015.412,
  author =	{Carbone, Marco and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Yoshida, Nobuko},
  title =	{{Multiparty Session Types as Coherence Proofs}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{412--426},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.412},
  URN =		{urn:nbn:de:0030-drops-53661},
  doi =		{10.4230/LIPIcs.CONCUR.2015.412},
  annote =	{Keywords: Programming languages, Type systems, Session Types, Linear Logic}
}

Refine by Author
2 Carbone, Marco
2 Montesi, Fabrizio
2 Schürmann, Carsten
1 Charfreitag, Jonas
1 Dahn, Christine
Show More...

Refine by Classification
1 Mathematics of computing → Combinatorial optimization
1 Mathematics of computing → Solvers
1 Theory of computation → Network optimization

Refine by Keyword
2 Linear Logic
1 Data Reduction
1 Maximum Cut
1 Multiparty Session Types
1 Programming languages
Show More...

Refine by Type
3 document

Refine by Publication Year
1 2015
1 2016
1 2024