reachability_solver

针对有向边的线性可达性求解器

警告：在这个意义上，它被称为“线性求解器”，因为它在底层使用了线性求解器。这旨在作为逻辑研究的示例。请不要在生产环境中使用，因为这个算法的运行时间和内存复杂度远非最佳。

此求解器接受一个数字对的列表，并生成一个新的数字对列表。

例如

[1, 2], [2, 3]  =>  [1, 3]

换句话说，它是一种算法，可以判断一个迷宫是否可解。它通过将迷宫简化为一个更容易解决的等效迷宫来实现这一点。

哈利·波特与高阶迷宫求解

剧透警告

这种转换后的迷宫很有趣，因为它们与更复杂的迷宫相比，在起点和终点位置方面具有“相同的信息”。

这种转换可以用于预处理高阶迷宫求解的迷宫。它被称为“预语言语义”，因为任何在原始迷宫上使用布尔代数进行的推理问题都可以使用转换后的迷宫上的布尔代数来解决。

这个想法最好通过《哈利·波特与火焰杯》一书中的一个例子来说明。

书中的迷宫非常复杂，并且随时间变化（从空间-时间来看，这是一个静态迷宫），所以我将使用一个更简单的例子。

在三强争霸赛的最后一轮中，哈利从 1 开始，Cedric 从 2 开始。哈利和 Cedric 都试图同时到达三强争霸杯 5。我们想知道哈利和 Cedric 是否能同时到达三强争霸杯。结果证明他们可以，因为对哈利和 Cedric 来说都是可达的。

[1, 4], [2, 3], [3, 4], [4, 5]  =>  [1, 5], [2, 5]

这对 [3, 4] 代表哈利帮助 Cedric 的时间点。在一个哈利没有帮助 Cedric 的替代时间线上，转换后的迷宫变为

[1, 4], [2, 3], [4, 5]  =>  [1, 5], [2, 3]

Cedric 就被困在了迷宫的死胡同中。

这是一个更高阶的迷宫问题，可以表示为以下

(Harry -> TriwizardCup) ∧ (Cedric -> TriwizardCup)

在这里，∧ 运算符表示逻辑与。

从任何迷宫问题中，可以通过对任何子问题使用布尔代数来构造一个“更高阶的迷宫问题”。这些类型的问题在没有了解更高阶问题的细节的情况下，直接在非变换的迷宫上解决是比较困难的。

假设某个操纵者（我不会告诉你是谁）想让哈利到达三强争霸杯，但不能是西德里克。可以这样表达这个目标

(Harry -> TriwizardCup) ∧ ¬(Cedric -> TriwizardCup)

可以确定这是否为真，而无需了解时空位置如何连接的内部配置。

然而，如果这个人在通往目标唯一路径上放置一个只能让第一个人通过的魔法之门，那么就难以确定哈利是否能到达三强争霸杯。必须使用原始迷宫和一些额外信息（例如，哪条路径花费时间更短以及每个巫师学校冠军的速度如何）来分析这个问题。这个问题的可解性取决于求解算法。

图论

这对数字表示图中的边。对于从起始节点可到达的每个终端节点，输出都会产生一对。所有其他边都被删除，包括环形边。

有关可达性的更多信息，请参阅维基百科文章。

这可以用来

• 了解迷宫解决算法
• 通过研究简单示例了解线性解决方法
• 通过研究简单示例了解范畴论
• 研究前语言语义（布尔代数解释上的不变推理）

范畴论和可达性简介

范畴可以被认为是一种具有节点和边的图/网络。

• 范畴理论中的节点被称为“对象”
• 范畴理论中的边是方向的，称为“态射”

范畴论是数学的一个分支，它抽象地处理具有相似结构的难题，使得可以以共同的语言对这些难题进行推理。

以下要求适用于所有范畴

• 每个对象（节点）至少有一个到自身的态射（箭头）
• 如果有态射（箭头）A -> B 和 B -> C，那么就有一个态射（箭头）A -> C

没有关于节点和边的本身的信息，只有节点和边如何连接。

边 [A, B] 可以被认为是一个证明，至少存在一个态射 A -> B