Functional Modelling of the Matroid and Application to the Knapsack Problem
摘要
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.