3 Search Results for "Spieksma, Frits C.R."

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.ISAAC.2022.49

Package Delivery Using Drones with Restricted Movement Areas

Authors: Thomas Erlebach, Kelin Luo, and Frits C.R. Spieksma

Published in: LIPIcs, Volume 248, 33rd International Symposium on Algorithms and Computation (ISAAC 2022)

Abstract

For the problem of delivering a package from a source node to a destination node in a graph using a set of drones, we study the setting where the movements of each drone are restricted to a certain subgraph of the given graph. We consider the objectives of minimizing the delivery time (problem DDT) and of minimizing the total energy consumption (problem DDC). For general graphs, we show a strong inapproximability result and a matching approximation algorithm for DDT as well as NP-hardness and a 2-approximation algorithm for DDC. For the special case of a path, we show that DDT is NP-hard if the drones have different speeds. For trees, we give optimal algorithms under the assumption that all drones have the same speed or the same energy consumption rate. The results for trees extend to arbitrary graphs if the subgraph of each drone is isometric.

Cite as

Thomas Erlebach, Kelin Luo, and Frits C.R. Spieksma. Package Delivery Using Drones with Restricted Movement Areas. In 33rd International Symposium on Algorithms and Computation (ISAAC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 248, pp. 49:1-49:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{erlebach_et_al:LIPIcs.ISAAC.2022.49,
  author =	{Erlebach, Thomas and Luo, Kelin and Spieksma, Frits C.R.},
  title =	{{Package Delivery Using Drones with Restricted Movement Areas}},
  booktitle =	{33rd International Symposium on Algorithms and Computation (ISAAC 2022)},
  pages =	{49:1--49:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-258-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{248},
  editor =	{Bae, Sang Won and Park, Heejin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2022.49},
  URN =		{urn:nbn:de:0030-drops-173343},
  doi =		{10.4230/LIPIcs.ISAAC.2022.49},
  annote =	{Keywords: Mobile agents, approximation algorithm, inapproximability}
}

Document

DOI: 10.4230/OASIcs.ATMOS.2014.92

Mathematical programming models for scheduling locks in sequence

Authors: Ward Passchyn, Dirk Briskorn, and Frits C.R. Spieksma

Published in: OASIcs, Volume 42, 14th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (2014)

Abstract

We investigate the scheduling of series of consecutive locks. This setting occurs naturally along canals and waterways. We describe a problem that generalizes different models that have been studied in literature. Our contribution is to (i) provide two distinct mathematical programming formulations, and compare them empirically, (ii) show how these models allow for minimizing emission by having the speed of a ship as a decision variable, (iii) to compare, on realistic instances, the optimum solution found by solving the models with the outcome of a decentralized heuristic.

Cite as

Ward Passchyn, Dirk Briskorn, and Frits C.R. Spieksma. Mathematical programming models for scheduling locks in sequence. In 14th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems. Open Access Series in Informatics (OASIcs), Volume 42, pp. 92-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{passchyn_et_al:OASIcs.ATMOS.2014.92,
  author =	{Passchyn, Ward and Briskorn, Dirk and Spieksma, Frits C.R.},
  title =	{{Mathematical programming models for scheduling locks in sequence}},
  booktitle =	{14th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems},
  pages =	{92--106},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-75-0},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{42},
  editor =	{Funke, Stefan and Mihal\'{a}k, Mat\'{u}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2014.92},
  URN =		{urn:nbn:de:0030-drops-47553},
  doi =		{10.4230/OASIcs.ATMOS.2014.92},
  annote =	{Keywords: Mixed Integer Programming, Inland Waterways, Lock Scheduling}
}

Refine by Author
2 Spieksma, Frits C.R.
1 Briskorn, Dirk
1 Demirović, Emir
1 Erlebach, Thomas
1 Luo, Kelin
Show More...

Refine by Classification
1 Theory of computation → Design and analysis of algorithms
1 Theory of computation → Discrete optimization
1 Theory of computation → Logic and verification

Refine by Keyword
1 Inland Waterways
1 Lock Scheduling
1 Mixed Integer Programming
1 Mobile agents
1 Proof logging
Show More...

Refine by Type
3 document

Refine by Publication Year
1 2014
1 2022
1 2024