给定一组条件,通过算法确定只有一个可以为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)

这些条件是从域特定语言生成的,用于确定下一个执行路径.即,当执行树分成多个路径时,用户为每个选项组成一个条件,并且计算结果为true的条件确定要采用的路径.为了使模拟有效,这些应该只是可以对任何给定值采用的一种可能路径.

目前,我在运行时评估这些条件,如果它们中的多个(或没有)为True,则会发脾气.

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

更新

关于条件中可包括的内容,范围在实践中相当广泛.所有这些都是可能的条件:

• 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 求解器超越。

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