算法用于扣款

Question

算法用于扣款

3

这里有一个问题，如果我们有两个语句p=>q 和 q=>r，那么它也意味着p=>r。

给定一组语句，我需要找出一个给定语句是true还是

false或不能从给定的语句中得出结论。
例如：

给定语句p=>q, p=>r, q=>s


如果输入是p=>s，我应该得到输出true
如果输入是p=>t，我应该得到输出无法得出结论
如果输入是p=> ~p，我应该得到输出false


这里我的问题是实现这个最好的数据结构是什么，并且使用什么算法。
谢谢。

- Anil

你只是在担心原子元素之间的 "implies" 运算符吗？或者你有更奇特的东西，像 ~p 或 ~s and r？ - BenDundee

2

@Deamonpog 这个问题实际上并没有漏洞。它要求一个例程，判断在给定理论（公理集）的情况下是否可以正式证明一个句子。请参阅http://en.wikipedia.org/wiki/Propositional_calculus#Proofs_in_propositional_calculus。 - us2012

@us2012 我已经使用一对向量实现了。但我正在做的是生成所有可能的推论，然后查看是否存在给定的语句。但是这需要很长时间，因为我的输入可能有10000个基本语句。 - Anil

1

@Anil YACAS 实现了这个功能，你可以查看他们的源代码以获取灵感：http://yacas.sourceforge.net/refchapter14.html。如果你找到了一个*高效的*算法，你将获得博士学位并受邀参加世界各地的会议。命题逻辑的可决定性是co-NP完全问题：http://en.wikipedia.org/wiki/Automated_theorem_proving#Decidability_of_the_problem。 - us2012

我并不是在追求任何博士学位。我需要解决这个问题以解决另一个问题。http://code.google.com/codejam/contest/438101/dashboard#s=p3 - Anil

显示剩余7条评论

3个回答

1

所以，我还不是完全清楚你想做什么。冒着被踩的风险，我想先建立一个图表来看看人们的想法。

我可能会先建立一个图表。每个实体（p、q等）都有自己的节点。"意味着"意味着在两个节点之间画一条线。任何输入，只要看看是否能找到遍历图的方法--所以在你的例子中，a => b，b => c，图形有三个节点，a连接到b，b连接到c。存在一条路径从a到c，这意味着a意味着c。

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

- BenDundee

只要您的编程语言允许仅变量名称和蕴含运算符，这就可以工作。但是，一旦像OP一样引入了NOT ~，它就会变得更加复杂！ - us2012

如果只是检查两个事物之间是否存在连接，那就没问题了，但我想我的问题不仅仅是这个。 - Anil

1

@Anil 如果您只对您提供的一个推导规则感兴趣，那么上面概述的简单基于图形的方法就足够了。原因是您没有任何结构扩展或缩减的规则，例如您没有像 p=>r，因此 p and q => r 对于任何 q 的规则。因此，您可以将所有的 p、q 甚至复杂的子句如 p and q 或 p=>q 视为 _原子_。但是，一旦您在演算法中引入了能够修改这些原子结构的规则，简单的图形就无法工作，因为结构修改规则会动态添加图形节点。 - jogojapan

1

@jogojapan 和 us2012：最近我一直在玩图论，这只是脑力激荡的结果。但这个想法如此美妙，以至于我确信数百年前就有人想到过它。话虽如此，我还是有点惊讶，居然没有一种方法可以使你的图表更加复杂。从与数学家打交道中，我知道他们为了保留一个美丽的想法而不惜代价 :) - BenDundee

1

很多人已经研究了这个问题多年。你需要的是一个SAT求解器。查找Chaff或zChaff或其他常用的SAT求解器。你需要取出类似(p->q && q->r) -> (p -> r) 的子句，对它们进行否定，并确定是否可满足。如果否定不可满足，则你有一个定理，即总是成立的东西。如果原始子句可满足且子句的否定也可满足，则应返回“无法得出结论”。如果原始子句不可满足，则你有一个错误的东西。

实际上，这是一个经过深入研究的问题。有好的算法，但是你可以处理的命题变量数量存在一个硬性限制。SAT是NP难问题的核心。这是一类没有有效算法的问题。

- carlosdc

谢谢，看起来好像有点多余，但我只需要解决这个问题。http://code.google.com/codejam/contest/438101/dashboard#s=p3 因为比赛只有两个小时，我没有时间写那么多代码。 :) - Anil

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Matthieu M. · Accepted Answer

考虑到你的问题比较简单，我建议使用一个简单的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}相关的谓词集合中。

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