We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional ``global cardinality constraints'': restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.

翻译：我们提出了关于带计数与算术的逻辑有限可满足性的新结果。第一个结果是对具有所谓局部普雷斯伯格量词的逻辑可满足性复杂度的紧致界，该量词对图中节点的邻域进行求和。第二个贡献涉及计算扩展了计数量词的双变量逻辑公式所关联基数的半线性表示。这种表示不仅允许获取这些逻辑的可满足性界，还能处理附加“全局基数约束”下的可满足性问题：即通过任意可判定算术逻辑表达的对一元公式基数的限制。在此过程中，我们为这些逻辑的有限可满足性及谱半线性的一些关键已有结果提供了更简洁的证明。