3

这是问题所在。

如果我们有两个陈述 p=>qand q=>r，它也暗示着p=>r。

给定一组陈述，我需要找出给定陈述是否true可以false从给定陈述中得出。

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

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

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

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

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

谢谢。

4

3 回答 3

1

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

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

于 2013-02-14T04:15:20.960 回答
1

我认为鉴于您的问题很简单，您可以使用简单的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 }。

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

于 2013-02-14T08:00:14.237 回答
1

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

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

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

于 2013-02-14T03:31:48.590 回答