基于最大约束可满足性的过载实时系统最优调度算法研究

Real-time systems play an important role in a variety of modern applications. Studying the optimal scheduling strategy in overloaded real-time systems is of great significance to enhance the system stability and market competitiveness. Considering the challenge issues in existing works, such as the difficulty, low efficiency, and the lack of flexibility in solving the optimum solution, this work is concerned with the Maximum Satisfiability (MaxSAT) formulation for optimal scheduling in overloaded real-time systems. Specifically, on the basis of the fundamental scheduling problem, various task properties and scheduling objectives are taken into account. A MaxSAT model will be constructed to formulate the fundamental scheduling problem, and extensive MaxSAT encoding techniques will be applied to task properties and scheduling objectives. The accomplishment of this scientific research will work out a series of MaxSAT-based optimal scheduling algorithms for overloaded real-time systems, which provide theoretical and technical support for flexible and efficient scheduling, and improve the operating efficiency of systems.

实时系统在当今的各应用领域占有重要地位。研究过载实时系统的最优调度策略在提升系统稳定性和市场竞争力层面产生着积极影响，具有非常重要理论意义和实用价值。针对现有算法普遍存在的求解最优方案困难、效率低下、灵活性不够等诸多问题，本项目以过载条件下的实时系统为研究对象，采用最大约束可满足性（MaxSAT: Maximum Satisfiability）理论，探索基于MaxSAT的过载实时系统最优调度算法。项目以实时系统中的基本调度问题为基础，以任务属性和调度目标为核心，系统研究将基本调度问题进行MaxSAT建模的形式化方法，以及对任务属性和调度目标的扩展编码技术等关键科学问题，面向过载条件下的实时系统提出一套基于MaxSAT的最优调度方案，为灵活高效的系统调度提供理论和技术支撑，最终达到全面提升实时系统运行效率的目的。

本项目探索基于最大约束可满足性（MaxSAT）理论的过载实时系统最优调度算法。项目按计划顺利完成了既定目标，取得了相关的研究成果，主要包括如下几个方面：一、从形式化理论方法角度，提出全新的最大约束可满足性理论方法为单处理器过载实时系统设计最优任务调度方案，相比已有的形式化方法，显著提高了问题求解效率。二、从调度问题模型研究角度，将单处理器调度模型扩展为多处理器、多任务属性和多目标的调度模型，进行了该领域的理论初探，为调度领域的近似算法评估提供理论依据。三、从MaxSAT编码技术角度，针对现有的布尔逻辑编码缺陷进行了重点研究，精简了原编码产生的冗余布尔变量和子句，提出了更加紧凑的布尔逻辑编码，进一步提高问题求解效率。.依托该项目支持，在项目执行期间发表SCI论文7篇，EI期刊论文1篇，EI检索会议论文1篇，授权国家发明专利2项，招收研究生5名，在国际学术会议做口头报告1次，出国学术访问1次。综上，本项目顺利完成预期目标。