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

Question

给定一组两个或多个逻辑条件，是否可以通过算法确定其中一个将评估为 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

最终更新

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

Answer 1

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

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

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

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

Answer 2

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

Answer 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。

Answer 4

你的构建块只是条件吗

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

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

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

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

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