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

0-1背包问题是经典的组合优化问题与NP完全问题,具有重要的应用价值与理论意义.本文使用PAR(Partition and Recurrence)方法形式化推导了0-1背包问题的高效动态规划箅法程序.通过类比分析.该问题的若干变形问题的算法也可推导得到.算法通过PAR平台的自动生成系统转换成可执行语言程序并运行通过,保证了该类0-1背包问题算法的正确性和可靠性.本文主要的贡献是将PAR方法推广到能处理带约束条件的组合优化类问题,大大扩展了PAR方法的应用范围,为形式化开发高效高可信组合优化类算法开辟了一条新途径.

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

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 system 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.