We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the combinations of the most common model-theoretic properties in theory combination, namely stable infiniteness, smoothness, convexity, finite witnessability, and strong finite witnessability (and therefore politeness and strong politeness as well). All of our examples are sharp, in the sense that we also offer proofs that no theories are available within simpler signatures. This table significantly progresses the current understanding of the various properties and their interactions. The most remarkable example in this table is of a theory over a single sort that is polite but not strongly polite (the existence of such a theory was only known until now for two-sorted signatures). The second contribution is a new combination theorem showing that in order to apply polite theory combination, it is sufficient for one theory to be stably infinite and strongly finitely witnessable, thus showing that smoothness is not a critical property in this combination method. This result has the potential to greatly simplify the process of showing which theories can be used in polite combination, as showing stable infiniteness is considerably simpler than showing smoothness.

翻译：我们为可满足性模理论中的理论组合研究做出两项贡献。第一项是列出了理论组合中最常见模型论性质（即稳定无穷性、光滑性、凸性、有限可证性及强有限可证性，因此也涵盖礼貌性与强礼貌性）组合的示例表。所有示例均为紧致的，即我们还证明了不存在更简单签名下的理论。该表显著推进了当前对各种性质及其相互作用的理解。其中最突出的示例是一个单排序理论，它满足礼貌性但不满足强礼貌性（此前仅已知双排序签名中存在此类理论）。第二项贡献是一个新的组合定理，表明应用礼貌理论组合时，只需一个理论满足稳定无穷性与强有限可证性，从而证明光滑性在该组合方法中并非关键性质。该结果有望极大简化证明哪些理论可用于礼貌组合的过程，因为证明稳定无穷性比证明光滑性要容易得多。