NP Decision Procedure for Monomial and Linear Integer Constraints

2022/08/04 by Raya, Rodrigo, Hamza, Jad, Kunčak, Viktor
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2208.02713

Abstract

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ⁿ (x_i <= x_jⁿ). 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ⁿ].

Related

• A polynomial-time algorithm for median-closed semilinear constraints
• Certificates and relaxations for integer programming and the semi-group membership problem
• NP Satisfiability for Arrays as Powers
• Constraint Propagation as Information Maximization
• NP-Completeness of deciding the feasibility of Linear Equations over binary-variables with coefficients and constants that are 0, 1, or -1