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.

翻译：本文研究顺序3D打印中的物体排布与调度问题。与传统3D打印一次性逐层打印所有物体不同，顺序3D打印需逐个完成物体打印。在此模式下，必须确保打印机的运动部件不会与已打印物体发生碰撞。我们从组合优化角度审视该顺序打印问题，提出将其表述为线性算术公式，并采用可满足性模理论（SMT）求解器进行求解。然而，我们并未直接求解表述物体排布与调度问题的原始公式，而是提出了一种受反例引导抽象精化（CEGAR）启发的技术，该技术被证明是提升求解效率的关键创新。