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. Further refinements of the translation are left for future work.

翻译：本文分析了如何利用对称性将结构（亦称作解释）无损压缩到更小的论域上。该分析表明，在压缩域中求解可满足性问题可能获得更好的性能。为此，我们提出一种新颖的两步法：（i）将待满足的语句自动翻译为在允许域压缩的“提升”词汇表上的等可满足语句；（ii）通过逐步扩展（初始未知的）压缩域直至找到满足结构，来判定提升语句的可满足性。关键在于确保此满足结构总能展开为满足原始待满足语句的非压缩结构。我们给出了针对带聚合的带类型一阶逻辑语句的充分翻译方案。实验评估表明，该方法在生成式配置问题上实现了显著加速。该方法还可应用于对操作复杂数据结构的软件的验证。翻译的进一步优化留待未来工作。