一类0-1背包问题算法程序的形式化推导  

Formal Derivation of a Kind of 0-1 Knapsack Problems Algorithmic Programs

作　　者：王昌晶[1,2,3] 薛锦云[1,2] 

机构地区：[1]江西师范大学江西省高性能计算技术重点实验室,江西南昌330022 [2]中国科学院软件研究所,北京100190 [3]中国科学院研究生院,北京100049

出　　处：《武汉大学学报（理学版）》2009年第6期674-680,共7页Journal of Wuhan University:Natural Science Edition

基　　金：科技部国际合作项目(2008DFA11940);国家自然科学基金资助项目(60773054);江西省教育厅青年科学基金资助项目(GJJ09461)

摘　　要：0-1背包问题是经典的组合优化问题与NP完全问题,具有重要的应用价值与理论意义.本文使用PAR(Partition and Recurrence)方法形式化推导了0-1背包问题的高效动态规划算法程序.通过类比分析,该问题的若干变形问题的算法也可推导得到,算法通过PAR平台的自动生成系统转换成可执行语言程序并运行通过,保证了该类0-1背包问题算法的正确性和可靠性.本文主要的贡献是将PAR方法推广到能处理带约束条件的组合优化类问题,大大扩展了PAR方法的应用范围,为形式化开发高效高可信组合优化类算法开辟了一条新途径.0-1 knapsack problem is a classical Combinatorial optimization problem and NP complete problem. It has important application value and theoretical significance. In this paper, we formally derive the efficient dynamic programming algorithmic program for solving 0 1 knapsack problem by using PAR （Partition and Recurrence） method. Some of its variable algorithms can also be derived by analogy. The algorithm can be transformed into executive program and run normally using the automatic generation sys- tem in PAR platform. It guarantees the correctness and reliability of this kind of 0-1 knapsack problems algorithms. The main contribution of this paper is to extend PAR method to dealing with the combinatorial optimization problems with constraints, which greatly expand the scope of application of PAR method. The approach in this paper pioneers a new avenue to formally develop combination and optimization algorithms with high efficiency and trustworthiness.

关 键 词：形式化推导 高可信 组合优化 0-1背包问题 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]