Object Packing and Scheduling for Sequential 3D Printing: A Linear Arithmetic Model and a CEGAR-Inspired Optimal Solver (Extended Abstract)

Authors

  • Pavel Surynek Czech Technical University in Prague, Faculty of Information Technology
  • Vojtěch Bubník Prusa Research
  • Lukáš Matěna Prusa Research
  • Petr Kubiš Prusa Research

DOI:

https://doi.org/10.1609/socs.v18i1.36014

Abstract

We address the problem of object arrangement and scheduling for sequential 3D printing. Unlike the standard 3D printing, where all objects are printed slice by slice, in sequential 3D printing, objects are completed one after another. In the sequential case, it is necessary to ensure that the moving parts of the printer do not collide with previously printed objects. We propose to express the problem of sequential printing as a linear arithmetic formula, which is then solved using a solver for satisfiability modulo theories (SMT) combined with counterexample guided abstraction refinement (CEGAR).

Downloads

Published

2025-07-20

How to Cite

Surynek, P., Bubník, V., Matěna, L., & Kubiš, P. (2025). Object Packing and Scheduling for Sequential 3D Printing: A Linear Arithmetic Model and a CEGAR-Inspired Optimal Solver (Extended Abstract). Proceedings of the International Symposium on Combinatorial Search, 18(1), 271–272. https://doi.org/10.1609/socs.v18i1.36014