扣除算法

Algorithm for Deductions

本文关键字：算法      更新时间：2023-10-16

这就是问题所在。

如果我们有两个语句 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

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

谢谢。

所以，我仍然_entirely不清楚你想做什么。冒着被否决的风险，我要把它踢出去，看看人们怎么想。

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

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

很多人研究这个问题很多年了。您需要的是 SAT 求解器。查找箔条或z箔条或任何其他常用的SAT求解器。你想把像(p->q && q->r(这样的子句>(p -> r(否定它们，并确定这是否满足。如果否定不能满足，那么你有一个定理，一个总是正确的定理。如果原始子句是可以满足的，并且满足了对子句的否定，则应返回"无法结束"。如果原始条款不满足，那么你就有了错误的东西。

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

我认为

鉴于您的问题的简单性，您可以使用简单的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时，在与{ "p", true }关联的谓词集中插入{ "q", true }。

请注意，这实际上编码了一个有向图，因此在证明语句时，探索图的典型方法适用。

相关文章：