扣除算法

Question

这就是问题所在。

如果我们有两个语句 p=>q 和q=>r，也暗示p=>r。

给定一组语句，我需要找出给定语句是true 还是false，或者不能从给定语句中得出结论。

示例：
给定语句p=>q, p=>r, q=>s

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

• 如果输入是p=>t，我应该得到输出Cannot be concluded

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

我的问题是实现这一点的最佳数据结构是什么以及使用什么算法。

谢谢。

Answer 1

所以，我仍然不完全清楚您要做什么。冒着被否决的风险，我将把它踢出去，看看人们的想法。

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

我还没有进一步审查这个想法，但这似乎是一个有趣的前景。特别是因为图论很酷，而且很多人都对它感兴趣（即 Facebook 高管）。并且 Python 中有很好的模块用于分析图形。 （我认为 C++ 也是如此。您始终可以使用 Gephi 手动指定它：https://gephi.org/）

Answer 2

很多人多年来一直研究这个问题。您需要的是SAT Solver。查找 Chaff 或 zChaff 或任何其他常用的 SAT 求解器。您想使用 (p->q && q->r) -> (p -> r) 之类的子句并否定它们并确定是否可以满足。如果否定不能满足，那么你就有一个定理，它总是正确的。如果原分句可满足，而分句的否定可满足，则应返回“不能成立”。如果原始条款不能满足，那么你就有了错误的东西。

这实际上是一个经过充分研究的问题。有很好的算法，但是你可以处理多少命题变量是有硬性限制的。 SAT 是 NP 难题的核心。一类未知有效算法的问题。

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>;

您以下列方式使用映射：当给定p => q 时，您将{ "q", true } 插入到与{ "p", true } 关联的谓词集中。

请注意，这实际上是对有向图进行编码，因此探索图的典型方法适用于证明陈述。