给定一组条件，通过算法确定只有一个条件为真

Posted 2023-05-08

【中文标题】给定一组条件，通过算法确定只有一个条件为真

【英文标题】：given a set of conditions, algorithmically determine only one can be True

【发布时间】：2011-04-01 17:23:17

【问题描述】：

给定一组两个或多个逻辑条件，是否可以通过算法确定其中一个将评估为 TRUE？例如：

# this should pass, since for every X, only one condition is taken
cond 1: (X >= 1.0) 
cond 2: (X < 1.0)

# this should fail
cond 1: (X < 1.0)
cond 2: (X > 2.0)

# this should also fail, since X=1.0 would meet both conditions
cond 1: (X < 2.0)
cond 2: (X > 0.0)

# there may be more than one variable involved
cond 1: (X >= 1.0 && Y >= 0)
cond 2: (X < 1.0 && Y <= -1)

这些条件由特定领域的语言生成，用于确定下一个执行路径。即当执行树分成多个路径时，用户为每个选项组成一个条件，并且评估为真的条件确定要采用的路径。为了使模拟有效，这些应该只是任何给定值可以采用的一种可能路径。

目前，我在运行时评估这些条件，如果其中一个以上（或一个都不）为真，我会发脾气。

我希望能够在解析阶段检查错误条件（域语言到可编译源代码）。可能吗？如何验证条件？

更新

关于条件中可以包含的内容，在实践中范围相当广泛。这些都是可能的条件：

X >= Y && Y < Z X.within_radius(0.4) X IN some_array X * Y < Z

最终更新

似乎不可能找到涵盖所有可能条件的解决方案（或者至少，鉴于我的知识有限，在为该问题分配的时间内不可能）。有一天会重新审视这个，但现在接受让我走得更远的答案。

【问题讨论】：

NULL 可能吗？以下可能是一个很好的起点：en.wikipedia.org/wiki/Formal_verification

最后一个也应该失败不是吗？如果 X = 0 且 Y = 0，则这两个条件都是错误的。

@Chris：你是对的。谢谢。会更新。

@Lucero：（除非我误解了你的问题）NULL 不是每个条件的可能结果。每个条件都应该评估为真或假。

由于决策是决策树的一部分，您是否也必须包括父条件？例如，当您沿着X > 2 的路径前进时，随后的两个条件X < 1 和X > 0 不会发生冲突，但您的静态检查工具可能会报告它们会发生冲突。跨度>

【参考方案1】：

编辑：我会重申，因为其他答案似乎假设了一堆已经被证实的事情：

如果您可以根据Presburger arithmetic 陈述您的条件（以及只有一个为真的约束），那么您可以编写一个决策过程来静态验证该属性。从上面的例子来看，这似乎完全可以实现。

“钝器”方法基本上是与自动定理证明器或 SMT 求解器之类的东西交互（您基本上会尝试证明“存在满足约束 1 XOR 约束 2 的某些值 x”这一陈述的否定）。我之前以编程方式与CVC3 交互，发现它很好用，但我的理解是它已被其他 SMT 求解器超越。

我认为，您为解决此问题所做的任何其他事情可能最终都会近似于我所建议的各种工具的一些实现。根据您的约束的具体指定方式，您可能能够为Presburger arithmetic 之类的东西实施某种决策程序。

【讨论】：

谢谢吉安。我会读一读，看看是否符合要求。

同意吉安。还要检查“代码合同”概念，例如在 Eiffel 中。在此处对代码合约进行静态验证的出色工作：research.microsoft.com/en-us/projects/contracts，此处：pexforfun.com/… 和此处：channel9.msdn.com/posts/Peli/…

【参考方案2】：

一般来说，不会。但是，如果您真正要问的是，是否有可能给定由一组有限独立整数变量和常数上的不等式的布尔逻辑组合组成的条件，那么就有希望了。您可以通过使用不等式中出现的常量（以及这些常量的 +1 和 -1）置换变量来彻底检查，并验证成立的条件数始终为 1。

【讨论】：

我是这么想的，但我希望 S.O.可以告诉我否则。谢谢。

【参考方案3】：

如果您想查找是否只有一个条件为真（在两个或多个可能的条件中），请参考 SO：xor-of-three-values 上的这个异或问题可能会有所帮助。 直接从它的答案中获取：

(a ^ b ^ c) && !(a && b && c)

在你的情况下：

(cond 1 ^ cond 2 ^ cond 3) && !(cond 1 && cond 2 && cond 3)

还有一个通用的解决方案，每次任何条件为真时增加一个计数，然后在测试所有条件后检查计数是否为 1。

【讨论】：

谢谢加里。我已经有了一个几乎可以做到这一点的解决方案。我现在想知道的是是否可以静态而不是在运行时检查它。 a、b、c 的值事先不知道。

好吧，我一开始没看懂这个问题。祝你好运。

【参考方案4】：

你的构建块只是条件吗

一个整数变量， （、>=）中的比较运算符， 数字（假设是整数）？

最后的条件是使用 && 和 ||?

我们可以假设所有整数变量都是独立的吗？

在这些条件下，我假设可以通过算法对其进行检查。我会将每个变量的所有有效范围放入数据结构中，并检查交叉点。

编辑：由于情况似乎并非如此，最好的解决方案可能是将不同类型的条件分组，以便可以对每个组中的条件进行静态评估。我从你的第一个描述中假设的条件类型只是这些组中的一个。

【讨论】：

（编辑）恐怕变量不限于数字，并且可以包含返回 True/False 的类似函数的构造（例如 x.within_radius(0.3) 或 (x IN somearray)）。这些条件不会合并为最终条件，而是每个条件相互独立，并由用户分配给一系列路径以确定模拟的路线（因此需要验证）。