While Maximum Satisfiability (MaxSAT) has been successfully applied to a wide range of combinatorial optimization problems, the encoding of Nonlinear Integer Programming (NLIP) with polynomial functions into MaxSAT has so far only been studied at a theoretical level. In this paper, we introduce NLIPSat, the first tool capable of encoding bounded polynomial NLIP instances directly into Maximum Satisfiability. Building upon recent MaxSAT formulations for polynomial NLIP proposed in [Zhifei Zheng et al., 2025], NLIPSat enables the encoding of polynomial nonlinear objective functions as weighted soft clauses and also supports the encoding of hard non-linear polynomial constraints within a polynomial setting. Extensive experiments on different benchmarks show that NLIPSat outperforms the state-of-the-art SMT solver Z3 by a wide margin.

The Simple Assembly Line Balancing Problem with Power Peak Minimization (SALB3PM) is a relatively new problem that aims to assign tasks to workstations with a focus on minimizing power peaks. By integrating load balancing and task scheduling, this problem offers a comprehensive approach to enhancing energy efficiency in production systems, which can lead to significant cost savings alongside a positive environmental impact. This paper introduces novel models for SALB3PM based on Maximum Satisfiability (MaxSAT), the natural optimization extension of the Satisfiability problem, providing a new perspective to solve this optimization problem effectively. Experimental results demonstrate the efficiency and robustness of our approach with respect to the MaxSAT solvers applied. To the best of our knowledge, this is the first attempt to address the SALB3PM problem through the lens of Maximum Satisfiability.