Z3py SMT 编码以下变量和公式

Question

我对 Z3 和 SMT 求解器非常陌生。 我有以下问题，我不知道如何在 Z3py 中编写代码。

在上图中 N 是节点的集合，因此 N = {Node1, Node2, Node3, Node4, Node5, Node6, Node7}

I 是一组输入，I = {I₁, I₂, I₃, I₄}

O 是一组输出，O = {O₁, O₂, O₃}

G 是一个组，其中对于任何连续的 2 个输出（O_i，O_j），如果 O_i 是第一个输出，并且O_j 是生成的第二个输出，G_k 是在 O_i 生成之后和 O 生成之前调度的节点集_j, but 如果 O_j 在 O_i 之前生成，则 G_k 包含在生成 O_j 之前调度的所有块。 节点的调度由另一个程序给出。 例如在上面的框图中，节点的调度以及输出的生成如下：

• 计划的第一个节点 = 节点 1
• 计划的第二个节点 = Node2
• 计划的第三个节点 = Node5
• 生成的输出 = O₁
• 计划的第四个节点 = Node3
• 计划的第五个节点 = 节点 6
• 生成的输出 = O₂
• 计划的第六个节点 = Node4
• 计划的第五个节点 = Node7
• 生成的输出 = O₃

因此从上面我们可以说 G₁ for (O₁, O₂) 是 = {Node3, Node6}

但是 (O₂, O₁) 的 G₂ 是 = {Node1, Node2, Node5}

要执行每个节点，我们需要一个任务，一个任务一次可以实现一个节点或一组节点。

Node_r,i 表示组 G_r 中的第 i^th 个节点。 Task_r,m 表示 G_r 组中的第 m^th 个任务。

布尔变量（可以是 0 或 1）：

• f_{Noder,iTaskr,m} 表示如果 Node_r,i 映射到 Task_r,m
• DN_{Noder,iNodes,j} 表示如果 Node_s,j 取决于 Node_r,i 即是否存在从 Node_r,i 到 Node_{s,j 的路径}
• DT_{Taskr,mTasks,n} 表示如果 Task_s,n 依赖于 Task_r,m
• M_Taskr,m表示是否有节点映射到Task_r,m

基于以上信息，我必须在 SMT 中制定以下方程式。

1. 最小化（Σ_r,m M_任务r,m)
2. M_任务r,m >= f_{Noder,iTaskr,m}（对于所有i）
3. Σ_m f_{Noder,iTaskr,m} = 1（对于所有 r != I,O） 例子： f_{Noder,iTaskr,m} + f_{节点r,i任务r,m+1} + f_{节点r,i任务r ,m+2} = 1 + 0 + 0 = 这告诉我们 Node_r,i 映射到 Task_r,m 因为 f _{Noder,iTaskr,m} = 1（一次只能将一个节点映射到1个任务，但可以映射一个任务一次连接到多个节点）
4. f_{Noder,iTasks,m} = 0（对于所有 r != s）
5. f_{Noder,iTaskr,m} = 1（对于所有 r = I,O 和 m = i）李>
6. f_{Noder,iTaskr,m} = 0（对于所有 r = I,O 和 m != i）
7. DT_{Taskr,mTasks,n} >= f_{Noder,i任务r,m} + f_{节点s,j任务s,n} + DN_{节点r,i节点s,j} - 2
8. DT_{Taskr,mTasks,n} >= DT_{Taskr,m任务t,l} + DT_{任务t,l任务s,n} - 1李>
9. DT_{Taskr,mTasks,n} + DT_{Tasks,nTask r,m}

我不明白如何用 SMT 格式表示变量和这些公式。

Answer 1

我不确定如何最好地回答，因为该问题包含很多未完全指定的细节参考。 例如，什么是 I 和 O？ 您可能在问如何添加线性不等式系统。或者如何指定可以为 0 或 1 的整数变量的问题。

一种方法是引入如下函数：

       a = Function('a', IntSort(), IntSort(), IntSort())

那么'a'是一个将整数对映射到整数的函数。 您可以以类似的方式声明函数“n”（但我猜您的示例实际上有一些拼写错误，并且您将 n 用作函数和索引变量）。 您也可以用类似的方式声明函数 f、h、q。

然后在python中你可以写：

     N = 5
     s = Solver()  # create a solver context
     for r in range(N):
         for i in range(N):
             for m in range(N):
                 if m != i:
                     s.add(f(n(r,i),a(r,m)) == 0)

这会在您指定的 f 上添加等式约束。 可以以类似的方式添加其他等式和不等式约束。 最后你问结果状态是否可以满足。

    print s.check()
    print s.model()   # print model for satisfiable outcome.

其他方法是为不同的变量声明不同的常量 f的版本。毕竟你建议的问题表明你只是 写下一个庞大的不等式系统 方式。

例如，您可以创建常量 v：

    v = Const('f(a[%d][%d],a[%d][%d])' % (r,m,r,i), IntSort())

而不是函数应用程序。