Optimization solvers based on methods from constraint programming (OR-Tools, Chuffed, Gecode), optimization modulo theory (Z3), and mathematical programming (CPLEX) are successfully applied nowadays to solve many non-trivial examples. However, for solving the problem of automated deployment in the Cloud of component-based applications, their computational requirements are huge making automatic optimization practically impossible with the current general optimization techniques. To overcome the difficulty, we exploited the sweet spots of the underlying problem in order to identify search space reduction methods. We came up with 15 symmetry breaking strategies which we tested in a static symmetry breaking setting on the solvers enumerated above and on 4 classes of problems. As a result, all symmetry breaking strategies led to significant improvement of the computational time of all solvers, most notably, Z3 performed the best compared to the others. As an observation, the symmetry breaking strategies confirmed that, when applied in a static setting, they may interact badly with the underlying techniques implemented by the solvers.

翻译：基于约束规划（OR-Tools、Chuffed、Gecode）、优化模理论（Z3）及数学规划（CPLEX）等方法的优化求解器，如今已成功应用于解决众多非平凡问题。然而，在解决基于组件的应用在云环境中的自动化部署问题时，这些求解器的计算需求极为庞大，使得当前通用优化技术几乎无法实现自动化优化。为克服这一困难，我们利用底层问题的"甜蜜点"来识别搜索空间缩减方法。我们提出了15种对称性打破策略，并在静态对称性打破设置下，对上述列举的求解器以及4类问题进行了测试。结果表明，所有对称性打破策略均显著提升了所有求解器的计算时间，其中Z3的表现最为突出。此外，观察发现，这些对称性打破策略在静态设置下应用时，可能与求解器内部实现的基础技术产生不良交互。