Maximum Satisfiability Formulations for Nonlinear Integer Programming.

This paper introduces novel Maximum Satisfiability (MaxSAT) formulations for the Nonlinear Integer Programming (NLIP) problems with discrete polynomial functions. We develop a generic framework based on three established integer encoding techniques from the literature. Our approach treats each polynomial term as an atomic unit and demonstrates how it can be efficiently encoded through compact representations of integer assignments. Additionally, we present two distinct decomposition methods based on the degrees of polynomial terms. This work lays a foundation for future research and has the potential to extend the applicability of modern MaxSAT solvers to a wider range of optimization problems.