2 Search Results for "Gr��linger, Armin"

Document
DOI: 10.4230/DagRep.5.4.98
Theory and Practice of SAT Solving (Dagstuhl Seminar 15171)

Authors: Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams

Published in: Dagstuhl Reports, Volume 5, Issue 4 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15171 "Theory and Practice of SAT Solving". The purpose of this workshop was to explore one of the most significant problems in all of computer science, namely that of computing whether formulas in propositional logic are satisfiable or not. This problem is believed to be intractable in general (by the theory of NP-completeness). However, the last two decades have seen dramatic developments in algorithmic techniques, and today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas. A surprising aspect of this development is that the best current SAT solvers are still to a large extent based on methods from the early 1960s, which can often handle formulas with millions of variables but may also get hopelessly stuck on formulas with just a few hundred variables. The fundamental question of when SAT solvers perform well or badly, and what underlying mathematical properties of the formulas influence SAT solver performance, remains very poorly understood. Another intriguing aspect is that much stronger mathematical methods of reasoning about propositional logic formulas are known today, in particular methods based on algebra and geometry, and these methods would seem to have great potential based on theoretical studies. However, attempts at harnessing the power of such methods have conspicuously failed to deliver any significant improvements in practical performance. This workshop gathered leading researchers in applied and theoretical areas of SAT and computational complexity to stimulate an increased exchange of ideas between these two communities. We see great opportunities for fruitful interplay between theoretical and applied research in this area, and believe that this workshop showed beyond doubt that a more vigorous interaction between the two has potential for major long-term impact in computer science, as well for applications in industry.
Cite as

Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams. Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). In Dagstuhl Reports, Volume 5, Issue 4, pp. 98-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{biere_et_al:DagRep.5.4.98,
  author =	{Biere, Armin and Ganesh, Vijay and Grohe, Martin and Nordstr\"{o}m, Jakob and Williams, Ryan},
  title =	{{Theory and Practice of SAT Solving (Dagstuhl Seminar 15171)}},
  pages =	{98--122},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{4},
  editor =	{Biere, Armin and Ganesh, Vijay and Grohe, Martin and Nordstr\"{o}m, Jakob and Williams, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.4.98},
  URN =		{urn:nbn:de:0030-drops-53520},
  doi =		{10.4230/DagRep.5.4.98},
  annote =	{Keywords: SAT, Boolean SAT solvers, SAT solving, conflict-driven clause learning, Gr\"{o}bner bases, pseudo-Boolean solvers, proof complexity, computational complexity, parameterized complexity}
}
Document
DOI: 10.4230/DagSemProc.07361.5
Some Experiments on Tiling Loop Programs for Shared-Memory Multicore Architectures

Authors: Armin Größlinger

Published in: Dagstuhl Seminar Proceedings, Volume 7361, Programming Models for Ubiquitous Parallelism (2008)

Abstract
The model-based transformation of loop programs is a way of detecting fine-grained parallelism in sequential programs. One of the challenges is to agglomerate the parallelism to a coarser grain, in order to map the operations of the program to the available cores in a multicore architecture. We consider shared-memory multicores as target architecture for space-time mapped loop programs and make some observations concerning code generation, load balancing and cache effects.
Cite as

Armin Größlinger. Some Experiments on Tiling Loop Programs for Shared-Memory Multicore Architectures. In Programming Models for Ubiquitous Parallelism. Dagstuhl Seminar Proceedings, Volume 7361, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{grolinger:DagSemProc.07361.5,
  author =	{Gr\"{o}{\ss}linger, Armin},
  title =	{{Some Experiments on Tiling Loop Programs for Shared-Memory Multicore Architectures}},
  booktitle =	{Programming Models for Ubiquitous Parallelism},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7361},
  editor =	{Albert Cohen and Mar{\'\i}a J. Garzar\'{a}n and Christian Lengauer and Samuel P. Midkiff},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07361.5},
  URN =		{urn:nbn:de:0030-drops-13748},
  doi =		{10.4230/DagSemProc.07361.5},
  annote =	{Keywords: Multicore, automatic parallelization, loop transformations, polyhedron model}
}
  • Refine by Author
  • 1 Biere, Armin
  • 1 Ganesh, Vijay
  • 1 Grohe, Martin
  • 1 Größlinger, Armin
  • 1 Nordström, Jakob
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Boolean SAT solvers
  • 1 Gröbner bases
  • 1 Multicore
  • 1 SAT
  • 1 SAT solving
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2008
  • 1 2015

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