NP Decision Procedure for Monomial and Linear Integer Constraints

Rodrigo Raya, Jad Hamza, Viktor Kunčak

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 li…