5 Search Results for "Berg, Christoph"


Document
Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization

Authors: Christoph Jabs, Jeremias Berg, Hannes Ihalainen, and Matti Järvisalo

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)


Abstract
Building on Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT) solving algorithms, several approaches to computing Pareto-optimal MaxSAT solutions under multiple objectives have been recently proposed. However, preprocessing in (Max)SAT-based multi-objective optimization remains so-far unexplored. Generalizing clause redundancy to the multi-objective setting, we establish provably-correct liftings of MaxSAT preprocessing techniques for multi-objective MaxSAT in terms of computing Pareto-optimal solutions. We also establish preservation of Pareto-MCSes - the multi-objective lifting of minimal correction sets tightly connected to optimal MaxSAT solutions - as a distinguishing feature between different redundancy notions in the multi-objective setting. Furthermore, we provide a first empirical evaluation of the effect of preprocessing on instance sizes and multi-objective MaxSAT solvers.

Cite as

Christoph Jabs, Jeremias Berg, Hannes Ihalainen, and Matti Järvisalo. Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{jabs_et_al:LIPIcs.CP.2023.18,
  author =	{Jabs, Christoph and Berg, Jeremias and Ihalainen, Hannes and J\"{a}rvisalo, Matti},
  title =	{{Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.18},
  URN =		{urn:nbn:de:0030-drops-190553},
  doi =		{10.4230/LIPIcs.CP.2023.18},
  annote =	{Keywords: maximum satisfiability, multi-objective combinatorial optimization, preprocessing, redundancy}
}
Document
MaxSAT-Based Bi-Objective Boolean Optimization

Authors: Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo

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


Abstract
We explore a maximum satisfiability (MaxSAT) based approach to bi-objective optimization. Bi-objective optimization refers to the task of finding so-called Pareto-optimal solutions in terms of two objective functions. Bi-objective optimization problems naturally arise in various real-world settings. For example, in the context of learning interpretable representations, such as decision rules, from data, one wishes to balance between two objectives, the classification error and the size of the representation. Our approach is generally applicable to bi-objective optimizations which allow for propositional encodings. The approach makes heavy use of incremental Boolean satisfiability (SAT) solving and draws inspiration from modern MaxSAT solving approaches. In particular, we describe several variants of the approach which arise from different approaches to MaxSAT solving. In addition to computing a single representative solution per each point of the Pareto front, the approach allows for enumerating all Pareto-optimal solutions. We empirically compare the efficiency of the approach to recent competing approaches, showing practical benefits of our approach in the contexts of learning interpretable classification rules and bi-objective set covering.

Cite as

Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. MaxSAT-Based Bi-Objective Boolean Optimization. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{jabs_et_al:LIPIcs.SAT.2022.12,
  author =	{Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J\"{a}rvisalo, Matti},
  title =	{{MaxSAT-Based Bi-Objective Boolean Optimization}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{12:1--12:23},
  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.12},
  URN =		{urn:nbn:de:0030-drops-166863},
  doi =		{10.4230/LIPIcs.SAT.2022.12},
  annote =	{Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT}
}
Document
A Domain Specific Language for Performance Evaluation of Medical Imaging Systems

Authors: Freek van den Berg, Anne Remke, and Boudewijn R. Haverkort

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)


Abstract
We propose iDSL, a domain specific language and toolbox for performance evaluation of Medical Imaging Systems. iDSL provides transformations to MoDeST models, which are in turn converted into UPPAAL and discrete-event MODES models. This enables automated performance evaluation by means of model checking and simulations. iDSL presents its results visually. We have tested iDSL on two example image processing systems. iDSL has successfully returned differentiated delays, resource utilizations and delay bounds. Hence, iDSL helps in evaluating and choosing between design alternatives, such as the effects of merging subsystems onto one platform or moving functionality from one platform to another.

Cite as

Freek van den Berg, Anne Remke, and Boudewijn R. Haverkort. A Domain Specific Language for Performance Evaluation of Medical Imaging Systems. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 80-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{vandenberg_et_al:OASIcs.MCPS.2014.80,
  author =	{van den Berg, Freek and Remke, Anne and Haverkort, Boudewijn R.},
  title =	{{A Domain Specific Language for Performance Evaluation of Medical Imaging Systems}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{80--93},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.80},
  URN =		{urn:nbn:de:0030-drops-45257},
  doi =		{10.4230/OASIcs.MCPS.2014.80},
  annote =	{Keywords: Domain Specific Language, Performance Evaluation, Simulation, Model Checking, Medical Systems}
}
Document
PLRU Cache Domino Effects

Authors: Christoph Berg

Published in: OASIcs, Volume 4, 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06) (2006)


Abstract
Domino effects have been shown to hinder a tight prediction of worst case execution times (WCET) on real-time hardware. First investigated by Lundqvist and Stenström, domino effects caused by pipeline stalls were shows to exist in the PowerPC by Schneider. This paper extends the list of causes of domino effects by showing that the pseudo LRU (PLRU) cache replacement policy can cause unbounded effects on the WCET. PLRU is used in the PowerPC PPC755, which is widely used in embedded systems, and some x86 models.

Cite as

Christoph Berg. PLRU Cache Domino Effects. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Open Access Series in Informatics (OASIcs), Volume 4, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{berg:OASIcs.WCET.2006.672,
  author =	{Berg, Christoph},
  title =	{{PLRU Cache Domino Effects}},
  booktitle =	{6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)},
  pages =	{1--3},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-03-3},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{4},
  editor =	{Mueller, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2006.672},
  URN =		{urn:nbn:de:0030-drops-6723},
  doi =		{10.4230/OASIcs.WCET.2006.672},
  annote =	{Keywords: Embedded systems, predictability, cache memory, PLRU, domino effects, timing anomalies}
}
Document
Requirements for and Design of a Processor with Predictable Timing

Authors: Christoph Berg, Jakob Engblom, and Reinhard Wilhelm

Published in: Dagstuhl Seminar Proceedings, Volume 3471, Perspectives Workshop: Design of Systems with Predictable Behaviour (2004)


Abstract
This paper introduces a set of design principles that aim to make processor architectures amenable to static timing analysis. Based on these principles, we give a design of a hard real-time processor with predictable timing, which is simultaneously capable of reaching respectable performance levels. The design principles we identify are recoverability from information loss in the analysis, minimal variation of the instruction timing, non-interference between processor components, deterministic processor behavior, and comprehensive documentation. The principles are based on our experience and that of other researchers in building timing analysis tools for existing processors.

Cite as

Christoph Berg, Jakob Engblom, and Reinhard Wilhelm. Requirements for and Design of a Processor with Predictable Timing. In Perspectives Workshop: Design of Systems with Predictable Behaviour. Dagstuhl Seminar Proceedings, Volume 3471, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2004)


Copy BibTex To Clipboard

@InProceedings{berg_et_al:DagSemProc.03471.4,
  author =	{Berg, Christoph and Engblom, Jakob and Wilhelm, Reinhard},
  title =	{{Requirements for and Design of a Processor with Predictable Timing}},
  booktitle =	{Perspectives Workshop: Design of Systems with Predictable Behaviour},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2004},
  volume =	{3471},
  editor =	{Lothar Thiele and Reinhard Wilhelm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.03471.4},
  URN =		{urn:nbn:de:0030-drops-57},
  doi =		{10.4230/DagSemProc.03471.4},
  annote =	{Keywords: WCET, hard real-time, embedded systems, computer architecture}
}
  • Refine by Author
  • 2 Berg, Christoph
  • 2 Berg, Jeremias
  • 2 Jabs, Christoph
  • 2 Järvisalo, Matti
  • 1 Engblom, Jakob
  • Show More...

  • Refine by Classification
  • 2 Mathematics of computing → Combinatorial optimization
  • 2 Theory of computation → Constraint and logic programming

  • Refine by Keyword
  • 2 maximum satisfiability
  • 1 Domain Specific Language
  • 1 Embedded systems
  • 1 Medical Systems
  • 1 Model Checking
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 1 2004
  • 1 2006
  • 1 2014
  • 1 2022
  • 1 2023

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