扣除算法

Question

这里有个问题。

如果我们有两个陈述：p=>q 和 q=>r，那么这也意味着 p=>r 是成立的。

给定一组陈述，我需要判断一个特定的陈述是 true（真的）、false（假的），还是无法从给定的陈述中得出结论。

举个例子：
给定的陈述是 p=>q, p=>r, q=>s

• 如果输入是 p=>s，我应该得到的输出是 true

• 如果输入是 p=>t，我应该得到的输出是 无法得出结论

• 如果输入是 p=> ~p，我应该得到的输出是 false

我的问题是，什么是实现这个的最佳数据结构，以及应该使用什么算法。

谢谢。

Answer 1

很多人研究这个问题已经很多年了。你需要一个叫做 SAT求解器 的工具。可以看看 Chaff 或者 zChaff，这些都是常用的SAT求解器。你需要把你的条件，比如 (p->q && q->r) 转换成 (p -> r)，然后对它们取反，看看这个反转后的条件是否可以满足。如果反转后的条件无法满足，那就说明你有一个定理，也就是总是成立的东西。如果原来的条件可以满足，而反转后的条件也可以满足，那就应该返回“无法得出结论”。如果原来的条件无法满足，那就说明你有一个错误的情况。

这个问题其实研究得很透彻了。有一些不错的算法，但处理的命题变量数量是有限制的。SAT问题是NP困难问题的核心，属于一类目前还没有找到高效算法的问题。

Answer 2

所以，我对你想做的事情还不是很清楚。冒着被投反对票的风险，我想把这个想法抛出来，看看大家的看法。

我可能会从构建一个图开始。每个实体（比如 p、q 等）都有自己的节点。“蕴含”意味着你在两个节点之间画一条线。那么，任何输入其实就是看看你能否找到一种方法来遍历这个图——在你的例子中，a => b，b => c，这个图有三个节点，a 连接到 b，b 连接到 c。a 和 c 之间存在路径，意味着 a 蕴含 c。

我还没有进一步验证这个想法，但这似乎是一个有趣的前景。特别是因为图论很酷，很多人对此感兴趣（比如 Facebook 的高管）。而且在 Python 中有很好的模块可以用来分析图。（我想 C++ 也有类似的情况。你也可以使用 Gephi 手动进行分析：https://gephi.org/）

Answer 3

我觉得考虑到你的问题比较简单，你可以用一个简单的 map 来解决。它比 vector 的主要优点是查找速度更快。

// For "p":  { name: "p", positive: "true" }
// For "~q": { name: "q", positive: "false" }
struct Predicate {
    std::string _name;
    bool _positive;
};

using PredicateSetType = std::unordered_set<Predicate>;
using PredicateMapType = std::unordered_map<Predicate, PredicateSetType>;

你可以这样使用这个 map：当你有 p => q 这样的关系时，你就把 { "q", true } 插入到与 { "p", true } 相关联的集合里。

需要注意的是，这实际上是在编码一个有向图，所以在证明某个说法时，可以用探索图的常规方法。