在 Mozart/Oz 中检查变量元组是不是不能被进一步约束

Posted 2023-03-31

【中文标题】在 Mozart/Oz 中检查变量元组是不是不能被进一步约束

【英文标题】：Check whether a tuple of variables cannot be constrained any further, in Mozart/Oz在 Mozart/Oz 中检查变量元组是否不能被进一步约束

【发布时间】：2011-08-21 04:29:11

【问题描述】：

你好，

这个想法最好用一个例子来说明：

假设我们有一个向量vec(a:FD.int 1#100 b:FD.int 1#100 c:FD.int 1#100)。 我希望能够向这个向量添加约束，直到我添加的每个额外约束 它不会添加任何更多信息，例如不再限制vec.a、vec.b 和vec.c。

是否可以在 Mozart/Oz 中做到这一点？

我愿意这样想。

在循环中：

访问约束存储， 检查是否改变 如果没有变化则终止。

【参考方案1】：

您可以使用FD.reflect 模块中的函数检查有限域变量的状态。 FD.reflect.dom 函数在这种情况下似乎特别有用。

要获取记录中每个字段的当前域，您可以将此函数映射到记录：

declare

fun GetDomains Vec
   Record.map Vec FD.reflect.dom
end

您的示例中的初始结果是：

vec(a:[1#100] b:[1#100] c:[1#100])

现在你可以比较这个函数在添加约束之前和之后的结果，看看有没有发生什么。

两个限制：

这仅适用于实际改变至少一个变量的域的约束。某些约束会更改约束存储但不会更改任何域，例如具有未绑定变量的等式约束。 像这样使用反射不适用于并发，即如果从多个线程添加约束，则会引入竞争条件。

如果您需要有关如何在循环中使用 GetDomains 函数的示例，请告诉我...

编辑：在old mailing list message 的提示下，我想出了这个适用于所有类型约束的通用解决方案。它通过在从属计算空间中推测性地执行约束来工作。

declare

Vec = vec(a:FD.int 1#100 b:FD.int 1#100 c:FD.int 1#100)

%% A number of constraints as a list of procedures
Constraints =
[proc $ Vec.a <: 50 end
 proc $ Vec.b =: Vec.a end
 proc $ Vec.b <: 50 end
 proc $ Vec.a =: Vec.b end
]


%% Tentatively executes a constraint C (represented as a procedure).
%% If it is already entailed by the current constraint store, returns false.
%% Otherwise merges the space (and thereby finally executes the constraint)
%% and returns true.
fun ExecuteConstraint C
   %% create a compuation space which tentatively executes C
   S = Space.new
        proc $ Root
           C
           Root = unit
        end
       
in
   %% check whether the computation space is entailed
   case Space.askVerbose S
   of succeeded(entailed) then false
   else
      Wait Space.merge S
      true
   end
end


for C in Constraints I in 1..4 break:Break do
   System.showInfo "Trying constraint "#I#" ..."
   if Not ExecuteConstraint C then
      System.showInfo "Constraint "#I#" is already entailed. Stopping."
      Break
   end
   Show Vec
end

Show Vec

【讨论】：

感谢您的回答。不幸的是，我需要整个约束存储，而不仅仅是域。例如，如果我有两个约束 a=:b 和 b=:c，则能够知道新约束 a=:c 甚至约束 a=:b 是否不会进一步约束我的变量。并发不是问题。

非常感谢。这正是我所要求的。