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.

使用对称性压缩结构来解决满足性问题，通过将句子转化为能够进行领域压缩的句子，检查满足性并找到满足条件的结构，其适用于生成配置问题。