Motivated by satisfiability of constraints with function symbols, we consider numerical inequalities on non-negative integers. The constraints we consider are a conjunction of a linear system Ax = b and a conjunction of (non-)convex constraints of the form x_i >= x_j^n (x_i <= x_j^n). We show that the satisfiability of these constraints is NP-complete even if the solution to the linear part is given explicitly. As a consequence, we obtain NP completeness for an extension of certain quantifier-free constraints on sets with cardinalities (QFBAPA) with function images S = f[P^n].
翻译:受功能符号约束的相对性驱使,我们考虑了非负整数上的数字不平等,我们认为这些制约是线性系统Ax=b和表x_i ⁇ x_j ⁇ n (x_i ⁇ x_j ⁇ n (x_i ⁇ x_j ⁇ n) 的(非)convex限制的结合。我们表明,这些制约的相对性是NP-完整,即使对线性部分的解决方案明确给出了。因此,我们对具有功能图像S = f[P ⁇ n] 的某些无限定性限制的集体(QFBAPA)的延伸获得了NP完整性。