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 Minimum Dominating Set problem (MDS) is a challenging NP-Hard problem with many practical applications. In this paper, we focus on its generalization, the Minimum Weight Dominating Set problem (MWDS). We first propose a novel lower bound for MWDS and prove a condition in which the computed lower bound is tight, then present a new local search approach, called Dual Bounds Search (DBS), which searches for a lower bound and an upper bound simultaneously in an alternate and collaborative way. We implement the lower bound algorithm and integrate two state-of-the-art local search algorithms into our DBS approach to obtain two new DBS algorithms for MWDS. Extensive experiments show that DBS approach can improve the local search performance for MWDS significantly. Thanks to the lower bound, new DBS algorithms can also provide a quality measure of solutions, which is practical in applications and is a clear difference from existing local searches for MWDS.

The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCLOpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.

This article focuses on the issue of the quantization-based event-triggered integral sliding-mode controller design for networked multiagent systems (MASs) encountering interferences under limited network bandwidth. An integral sliding manifold (ISM) is designed to address the effect of disturbances and ensure the desired dynamic performance of the system. We establish an event-triggered mechanism (ETM) with an exponential decay rate to conserve the limited communication resources. Then, a uniform quantizer is added to quantify the triggered state signals to lessen the network transmission burden caused by the digital network. Combining the designed ETM with a static uniform quantizer, the quantized trigger state signals are sent to decoders through the digital network to construct a quantized ISM. Subsequently, an event-triggered integral sliding-mode controller under quantization technology is developed to ensure the asymptotic average consensus of networked MASs. By testifying that every network agent has a lower positive bound, the viability of the proposed ETM is demonstrated, thereby ensuring the absence of Zeno behavior. Eventually, two simulation examples are proffered to confirm the efficacy of the quantization feedback-based event-triggered sliding-mode control methodology.

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.

A k-plex of a graph G is an induced subgraph in which every vertex has at most k-1 nonadjacent vertices. The Maximum k-plex Problem (MKP) consists in finding a k-plex of the largest size, which is NP-hard and finds many applications. Existing exact algorithms mainly implement a branch-and-bound approach and improve performance by integrating effective upper bounds and graph reduction rules. In this paper, we propose a refined upper bound, which can derive a tighter upper bound than existing methods, and an inprocessing strategy, which performs graph reduction incrementally. We implement a new BnB algorithm for MKP that employs the two components to reduce the search space. Extensive experiments show that both the refined upper bound and the inprocessing strategy are very efficient in the reduction of search space. The new algorithm outperforms the state-of-the-art algorithms on the tested benchmarks significantly.

The Minimum Dominating Set (MDS) problem is a classic NP-hard combinatorial optimization problem with many practical applications. Solving MDS is extremely challenging in computation. Previous work on exact algorithms mainly focuses on improving the theoretical time complexity and existing practical algorithms for MDS are almost based on heuristic search. In this paper, we propose a novel lower bound and an exact algorithm for MDS. The algorithm implements a branch-and-bound (BnB) approach and employs the new lower bound to reduce search space. Extensive empirical results show that the new lower bound is efficient in reduction of the search space and the new algorithm is effective for the standard instances and real-world instances. To the best of our knowledge, this is the first effective BnB algorithm for MDS.