Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Object Packing and Scheduling for Sequential 3D Printing: a Linear Arithmetic Model and a CEGAR-inspired Optimal Solver

Pavel Surynek, Vojtěch Bubník, Lukáš Matěna, Petr Kubiš

TL;DR

The paper tackles arranging and scheduling objects for sequential 3D printing, where objects are produced one after another and the extruder must avoid collisions with prior prints. It introduces SEQ-PACK+S, a linear arithmetic formulation, and a CEGAR-inspired solver NRICLSolve-CEGAR-SEQ that iterative refines feasibility by checking geometric collisions. Experimental results show SMT-based solving (with Z3) outperforming CSP approaches, and demonstrate substantial efficiency gains from the CEGAR refinements when solving the sequential packing problem. This approach enables more robust and faster sequential 3D printing planning, with practical impact for improving print reliability and throughput.

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 at once, in sequential 3D printing, objects are completed one after other. In the sequential case, it is necessary to ensure that the moving parts of the printer do not collide with previously printed objects. We look at the sequential printing problem from the perspective of combinatorial optimization. We propose to express the problem as a linear arithmetic formula, which is then solved using a solver for satisfiability modulo theories (SMT). However, we do not solve the formula expressing the problem of object arrangement and scheduling directly, but we have proposed a technique inspired by counterexample guided abstraction refinement (CEGAR), which turned out to be a key innovation to efficiency.

Object Packing and Scheduling for Sequential 3D Printing: a Linear Arithmetic Model and a CEGAR-inspired Optimal Solver

TL;DR

The paper tackles arranging and scheduling objects for sequential 3D printing, where objects are produced one after another and the extruder must avoid collisions with prior prints. It introduces SEQ-PACK+S, a linear arithmetic formulation, and a CEGAR-inspired solver NRICLSolve-CEGAR-SEQ that iterative refines feasibility by checking geometric collisions. Experimental results show SMT-based solving (with Z3) outperforming CSP approaches, and demonstrate substantial efficiency gains from the CEGAR refinements when solving the sequential packing problem. This approach enables more robust and faster sequential 3D printing planning, with practical impact for improving print reliability and throughput.

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 at once, in sequential 3D printing, objects are completed one after other. In the sequential case, it is necessary to ensure that the moving parts of the printer do not collide with previously printed objects. We look at the sequential printing problem from the perspective of combinatorial optimization. We propose to express the problem as a linear arithmetic formula, which is then solved using a solver for satisfiability modulo theories (SMT). However, we do not solve the formula expressing the problem of object arrangement and scheduling directly, but we have proposed a technique inspired by counterexample guided abstraction refinement (CEGAR), which turned out to be a key innovation to efficiency.

Paper Structure

This paper contains 10 sections, 4 theorems, 13 equations, 6 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Contribution
  4. Background
  5. A Linear Arithmetic Model
  6. A CEGAR Inspired Algorithm
  7. Experimental Evaluation
  8. Comparison of Solvers
  9. Benefit of CEGAR-style Refinements
  10. Conclusion

Key Result

Proposition 1

Minkowski sum of convex polygons $P_A=(A_1,A_2,...A_{\alpha}) \subseteq \mathbb{R}^2$ and $P_B=(B_1,B_2,...,B_{\beta}) \subseteq \mathbb{R}^2$ is convex polygon $P_C=(C_1,C_2,...,C_{\gamma}) \subseteq \mathbb{R}^2$.

Figures (6)

  • Figure 1: Standard 3D printing slice by slice and sequential 3D printing where objects are completed one by one shown in Prusa Slicer prusa-slicer-2025. The ordering of objects for sequential printing is shown by numbers. Printer extruder and gantry must avoid peviously printed objects in the sequential case (printing of the last object is shown).
  • Figure 2: Two overlapping convex polygons $P_A=(A_1,A_2,A_3,A_4)$ and $P_B=(B_1,B_2,B_3,B_4)$. Left: Condition (i) is violated while requirement (ii) is satisfied, Right: Although requirement (i) is met, the polygons overlap. Condition (ii) is violated.
  • Figure 3: Illustration of object simplification used in modeling the requirements for sequential printing (SEQ-PACK+S) as a linear arithmetic formula.
  • Figure 4: Illustration of the idea behind linear arithmetic formula modeling SEQ-PACK+S. In the setting where $O_1$ is printed after $O_2$ (right), the $xy$-projection of extruder $E$ and other moving parts of the printer moves only within $\mathcal{C}(\mathcal{E}(O_1)^{xy})$, hence ensuring non-overlapping between $\mathcal{C}(O_2^{xy})$ and $\mathcal{C}(\mathcal{E}(O_1)^{xy})$ as required by constraint (\ref{['eq:seq-constraint']}) ensures correct sequential printing.
  • Figure 5: Comparison of solving SEQ-PACK+S by the Gecode solver and the z3 solver on random cuboids. The right part shows cactus plots of runtimes (lower plot is better).
  • ...and 1 more figures

Theorems & Definitions (5)

  • Proposition 1
  • Proposition 2
  • proof
  • Proposition 3
  • Proposition 4