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

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)

这些条件是从领域特定语言生成的，并用于确定下一个执行路径。即当执行树分裂成多条路径时，用户为每个选项编写一个条件，计算结果为真的条件决定要采取的路径。为了使模拟有效，这些应该只是任何给定值都可以采取的一种可能路径。

目前，我在运行时评估这些条件，如果其中有多个（或没有）为真，我就会发脾气。

我希望能够在解析阶段检查错误条件（域语言到可编译源代码）。是否可以？人们将如何验证这些条件？

update

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

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

最终更新

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

Answer 1

编辑：我将重述，因为其他答案似乎假设了一堆已经得到证实的事情：

如果您可以根据 Presburger 算术，然后您可以编写一个决策过程来静态验证该属性。从上面的例子来看，这似乎是完全可以实现的。

“钝器”方法基本上是与自动定理证明器或 SMT 求解器等接口（您基本上会尝试证明语句“存在某个值 x 满足约束 1 异或约束 2”的否定）。我之前曾以编程方式与 CVC3 进行交互，并发现它非常好用，但我的理解是它已经被其他SMT求解器超越了。

我认为，您为解决这个问题所做的任何其他事情都可能最终会近似于我所建议的工具类型的某些实现。根据您的约束的具体指定方式，您可能能够对诸如

Answer 2

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

Answer 3

如果您想确定是否只有一个条件为真（在两个或多个可能的条件中），请参阅 SO 上的此异或问题可能会有所帮助：三值异或。
直接从它的答案中获取：

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

在您的情况下：

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

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

Answer 4

条件的构建块只是

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

最终条件是使用 && 构建的。和||？

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

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

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