We analyze how symmetries can be used to compress structures (also known as interpretations) onto a smaller domain without loss of information. This analysis suggests the possibility to solve satisfiability problems in the compressed domain for better performance. Thus, we propose a 2-step novel method: (i) the sentence to be satisfied is automatically translated into an equisatisfiable sentence over a ``lifted'' vocabulary that allows domain compression; (ii) satisfiability of the lifted sentence is checked by growing the (initially unknown) compressed domain until a satisfying structure is found. The key issue is to ensure that this satisfying structure can always be expanded into an uncompressed structure that satisfies the original sentence to be satisfied. We present an adequate translation for sentences in typed first-order logic extended with aggregates. Our experimental evaluation shows large speedups for generative configuration problems. The method also has applications in the verification of software operating on complex data structures. Our results justify further research in automatic translation of sentences for symmetry reduction.

翻译：我们分析了如何利用对称性将结构（亦称解释）无损压缩到更小的论域上。这一分析表明，在压缩论域中求解可满足性问题可能获得更优性能。为此，我们提出一种新颖的两步法：(i) 将被满足的语句自动翻译成在允许论域压缩的"提升"词汇表上的等可满足语句；(ii) 通过逐步扩展（初始未知的）压缩论域直至找到满足结构，来检验提升语句的可满足性。关键问题在于确保该满足结构始终能够扩展为满足原始语句的非压缩结构。我们为扩展了聚合运算的类型一阶逻辑中的语句给出了恰当的翻译方案。实验评估显示，该方法在生成式配置问题上获得了大幅加速，同时也可应用于操作复杂数据结构的软件验证。研究结果证明，面向对称约减的自动语句翻译值得进一步探索。