An E?cient Approach for Solving Optimization over Linear Arithmetic Constraints

来源 :计算机科学技术学报(英文版) | 被引量 : 0次 | 上传用户:skb09
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
Satisfiability Modulo Theories (SMT) have been widely investigated over the last decade. Recently researchers have extended SMT to the optimization problem over linear arithmetic constraints. To the best of our knowledge, Symba and OPT-MathSAT are two most e?cient solvers available for this problem. The key algorithms used by Symba and OPT-MathSAT consist of the loop of two procedures: 1) critical finding for detecting a critical point, which is very likely to be globally optimal, and 2) global checking for confirming the critical point is really globally optimal. In this paper, we propose a new approach based on the Simplex method widely used in operation research. Our fundamental idea is to find several critical points by constructing and solving a series of linear problems with the Simplex method. Our approach replaces the algorithms of critical finding in Symba and OPT-MathSAT, and reduces the runtime of critical finding and decreases the number of executions of global checking. The correctness of our approach is proved. The experiment evaluates our implementation against Symba and OPT-MathSAT on a critical class of problems in real-time systems. Our approach outperforms Symba on 99.6% of benchmarks and is superior to OPT-MathSAT in large-scale cases where the number of tasks is more than 24. The experimental results demonstrate that our approach has great potential and competitiveness for the optimization problem.
其他文献
Software product line (SPL) is an approach used to develop a range of software products with a high degree of similarity. In this approach, a feature model is u
多年以来,我们国家的疾病防治模式,实际上一直是以“治病救人”为中心,忽视了预防为主。究其根源来说,我国医学教育采用前苏联的医学模式,将公共卫生中的预防医学独立出来,其
该文从挂篮荷载计算、施工流程、支座及临时固结施工、挂篮安装及试验、合拢段施工、模板制作安装、钢筋安装、混凝土的浇筑及养生、测量监控等方面人手,介绍了S226海滨大桥
期刊
时下,走进镇赉县莫莫格蒙古族乡元宝吐村,你会看到干净的水泥路、崭新的砖瓦房、成群的牛羊,偶尔还会听到悠扬的马头琴声……这里,处处展示着繁荣富庶的社会主义新农村的新气
 一、鱼粉  1.看:纯鱼粉粒度不太均匀,能看到鱼肉纤维。假鱼粉磨得很细,呈粉末状,无鱼肉纤维。色泽:纯鱼粉为棕黄色或棕褐色,颜色一致。若呈灰白色、淡黄色,呈丝条状,说明掺有制革
我科应用双水平气道内正压无创通气(BiPAP)呼吸机治疗慢性阻塞性肺疾病(COPD)合并Ⅱ型呼吸衰竭患者82例,取得了满意效果.现根据实践经验对BiPAP呼吸机的使用和护理体会总结如
期刊
水产品消费具有很强的季节性,与此同时,淡水鱼的养殖也具有很强的季节性,每年的 3月份往往是我国淡水鱼主产区集中干塘起捕阶段。所以每年的 3、 4月份往往是我国主要淡水鱼价格
期刊
新生儿硬肿症的复温护理非常重要,它与患儿生命安危紧密联系.在护理新生儿硬肿症中我们有较深的体会,现介绍如下.
江苏苏北去年渔用饲料价格较低,淡水鱼类价格平稳,养鱼利润相对于养蟹高。由于盲目扩大养蟹面积,加上蟹病较为严重,养蟹的效益随着规模的扩大而严重下降,出现了不少养蟹亏损户。在
期刊