The matroids have a wide range of applications in discrete mathematics, combinatorial mathematics, computer science and other fields. However, most of the researches about matroids focus on the mathematical level, and there is a lack of exploration on functional modelling and formal verification. In this paper, we propose a general functional modeling framework for matroids, which consists of the basic elements of matroids, the verification functions of basic properties, and the verification functions of matroids. Finally, the functional modeling framework of this paper is used to verify whether the 0-1 knapsack problem and the fractional knapsack problem conform to the matroid structure, thus exemplifying the correctness of the matroid functional modeling and the matroid verification function, and reflecting the validity and extensibility of this framework.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Functional Modelling of the Matroid and Application to the Knapsack Problem

  • Zikang Wan,
  • Zhen You,
  • Chen Zhang,
  • Zhengkang Zuo,
  • Changjing Wang,
  • Qimin Hu

摘要

The matroids have a wide range of applications in discrete mathematics, combinatorial mathematics, computer science and other fields. However, most of the researches about matroids focus on the mathematical level, and there is a lack of exploration on functional modelling and formal verification. In this paper, we propose a general functional modeling framework for matroids, which consists of the basic elements of matroids, the verification functions of basic properties, and the verification functions of matroids. Finally, the functional modeling framework of this paper is used to verify whether the 0-1 knapsack problem and the fractional knapsack problem conform to the matroid structure, thus exemplifying the correctness of the matroid functional modeling and the matroid verification function, and reflecting the validity and extensibility of this framework.