Pseudo-Boolean optimization (PBO) problem involves optimizing a linear objective function under linear inequality constraints defined over Boolean variables. PBO is widely used for modeling many combinational optimization problems, particularly in some real-world scenarios. In core-guided CDCL-based exact solvers, the way branching variables are assigned, known as phase selection, significantly affects the solving efficiency. This paper introduces two strategies to enhance solver performance by improving phase selection. Firstly, we design a new phase selection strategy that actively guides variables in the objective function toward assignments closer to the optimal solution. Secondly, to prevent the solver from becoming trapped in local solutions, we propose a reinforcement learning-based rephase mechanism that dynamically updates and resets variable phases. We integrate two phase selection strategies into two state-of-the-art PBO solvers and compare them against top-performing solvers from the PB competitions, using benchmarks from these competitions for assessment. The experimental results show that our solvers outperform the winning solver from the competitions.

Pseudo-Boolean optimization (PBO) is usually used to model combinatorial optimization problems, especially for some real-world applications. Despite its significant importance in both theory and applications, the performance of current PBO solvers is still limited. This paper develops a novel local search algorithm for PBO, which has four main ideas. First, we design a new primary scoring function and a two-level selection strategy to evaluate all candidate variables. Second, we introduce a new weighting scheme to accurately guide the search process toward more promising directions. Third, we propose a novel deep optimization strategy to disturb some search processes. Fourth, an efficient solution space exploration mechanism is applied to help the algorithm jump out of local optimum. We conduct experiments on a broad range of public benchmarks, including three large-scale practical application benchmarks, two benchmarks from PB competitions, an integer linear programming optimization benchmark, a crafted combinatorial benchmark, and a combinatorial optimization knapsack benchmark to compare our proposed algorithm against twelve state-of-the-art competitors, including seven recently-proposed pure stochastic local search PBO solvers, a non-traditional stochastic local search combined with complete oracle, two complete PB solvers, and two mixed integer programming (MIP) solvers. Our proposed algorithm has been shown to perform best on these three real-world benchmarks. On the other five benchmarks, our algorithm shows competitive performance compared to state-of-the-art competitors, and it significantly outperforms all other local search algorithms, indicating that our algorithm greatly advances the state of the art in local search for solving PBO.

Abstract UPPAAL is a formal modeling and verification tool based on timed automata, capable of effectively analyzing real‐time software and hardware systems. In this article, we investigate research on UPPAAL‐assisted formal modeling and verification. First, we propose four research questions considering tool characteristics, modeling methods, verification means and application domains. Then, the state‐of‐the‐art methods for model specification and verification in UPPAAL are discussed, involving model transformation, model repair, property specification, as well as verification and testing methods. Next, typical application cases of formal modeling and verification assisted by UPPAAL are analyzed, spanning across domains such as network protocol, multi‐agent system, cyber‐physical system, rail traffic and aerospace systems, cloud and edge computing systems, as well as biological and medical systems. Finally, we address the four proposed questions based on our survey and outline future research directions. By responding to these questions, we aim to provide summaries and insights into potential avenues for further exploration in this field.