基于混合搜索的含逻辑“与”“或”的RM优化算法

来源：软件学报杂志2017年第10期北京时间：

作者：吕荫润,陈力,王翀,吴敬征,王永吉

单位：吕荫润，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院 软件研究所 基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 10019011,陈力，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院 软件研究所 基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 10019002,王翀，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院 软件研究所 基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 10019003,吴敬征，中国科学院 软件研究所 基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 10019004,王永吉，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院 软件研究所 基础软件国家工程研究中心, 北京 100190;中国科学院 软件研究所 互联网软件技术实验室, 北京 100190;中国科学院大学, 北京 10019005

摘要：相对于标准约束优化问题，广义约束优化问题（或称析取优化问题）的等式或不等式约束条件中不仅包含逻辑“与”关系，还含有逻辑“或”关系.单调速率（RM）优化问题是广义约束优化问题的一个重要应用.目前RM优化问题已有的解法包括函数变换、混合整数规划、线性规划搜索等算法.随着任务数的增多，这些算法的求解时间较长.提出一种基于线性规划的深度广度混合搜索算法（LPHS），将广义约束优化问题拆分成若干子问题，建立线性规划搜索树，合理选择搜索顺序，利用动态剪枝算法减小子问题的规模，最终求得最优解.实验结果表明，LPHS算法比其他方法有明显的效率提升.研究成果与计算机基础理论中的可满足性模理论的研究相结合，有助于提高可满足性模理论问题的求解效率，促进该理论在程序验证、符号执行等领域的进一步应用.

关键词：约束优化问题;实时系统;单调速率;线性规划;搜索算法

基金资助：中国科学院-国家外国专家局创新团队国际合作伙伴计划；国家自然科学基金（61170072）；青年科学基金（61303057）