问背包问题的时间公式是什么？

EN

它在“模型概述>行为规范是什么”下面。

​

​

TLA+规范可以指定不同的内容，而不仅仅是迭代算法。您所链接的knapsack.tla指定了问题和最优解决方案的定义，而没有描述用计算机真正找到它的好方法。

ValidKnapsacks(itemset) ==
  {sack \in [Items -> 0..4]: KnapsackSize(sack, itemset) <= Capacity}

[Items -> 0..4]是从Item到大小0..4的所有可能映射的集合。最优的解决方案是适合于大小为Capacity的背包的子集，因此表达式KnapsackSize(sack, itemset) <= Capacity。

另一个TLA+定义以令人印象深刻的高级方式定义了哪一个背包是最好的：

BestKnapsack(itemset) ==
  LET all == ValidKnapsacks(itemset)
  IN CHOOSE best \in all:
    \A worse \in all \ {best}:
      KnapsackValue(best, itemset) > KnapsackValue(worse, itemset)

它基本上是这样说的:在所有有效的背包中，最好的背包是比所有其他背包更好(更高的KnapsackValue)的背包。

您要寻找的是与此解决方案规范相匹配的迭代算法规范。该算法的规范将包含Init和Next公式，然后您可以检查它是否最终终止--通常称为Termination --然后存储背包的状态变量将包含BestKnapsack。

但是，您可以通过在“计算常量表达式”框中键入表达式来“运行”这些定义。

​

​

作者还对BestKnapsack - BestKnapsackOne和BestKnapsackTwo作了两个精化的定义.它们仍然是功能性的，我们称之为精化，因为它们越来越接近于在迭代算法中可实现的东西。

您可以像上面为BestKnapsack(HardcodedItemSet)所做的那样评估它们。如果它们与所有可能的输入的BestKnapsack输出相匹配，则它们是正确的改进。由于这是模型检查，“所有可能的输入”限定为“不超过某个大小”，我们假设(或证明)解决方案扩展到任何大小。