我对Z3和SMT解算器真的很陌生。 我有以下问题，我不知道如何在Z3py中编码。

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

i是输入集合，i={i1，i2，i3，i4}

O是输出集合，O={O1，O2，O3}

G是这样一个组，其中对于任何连续的2个输出(O i、O j)，如果Oi是第一个生成的输出，并且Oj是第二个生成的输出，则G k是在生成Oi之后和生成Oj之前调度的节点集合，但是如果Oj是在生成O之前生成的，则G k包含在生成之前调度的所有块。 节点的调度由另一个程序给出。 例如，在上面的框图中，节点的调度以及输出的生成如下所示：

计划的第一个节点=节点1 计划的第二个节点=节点2 计划的第三个节点=节点5 生成的输出=O1 计划的第四个节点=节点3 计划的第五个节点=节点6 生成的输出=O2 计划的第六个节点=节点4 计划的第五个节点=节点7 生成的输出=O3 因此，从上面我们可以说(O1，O2)的G1>是={节点3，节点6}

但(O2，O1)的G2为={Node1，Node2，Node5}

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

节点r，i表示组G中的第i个r节点。 任务表示G组中第m个任务。

布尔变量(可以是0或1)：

f节点r，i任务r，M表示是否 节点r，i映射到任务r，m DnNoder，iNodes，j表示 节点s，j取决于节点r，i，即是否存在从节点r，i到节点s，j的路径 DTTASKr，mTASKs，N表示 任务%s，n取决于任务r，m M任务r，m表示是否有节点映射到任务R，M

基于以上信息，我必须在SMT中表达以下公式。

最小化(&Sigma；r，m M任务r，M) M任务r，M= F节点r，I任务r，M(适用于所有I) &Sigma；m F节点r，I任务r，m=1(对于所有r！=I，O) 示例：f节点r，i任务r，m+f节点r，i任务r，m+1+f节点r，i任务r，m+2任务r，m+2任务r，m+2映射到任务r，这告诉我们，节点r，i映射到任务r，m映射到任务r，因为f节点r，i任务r，m=1(一次只能将一个节点映射到一个任务，但一个任务一次可以映射到几个节点) f节点r，i任务%s，m=0(对于所有r！=) f节点r，i任务r，m=1(对于所有r=I，O和m=I) f节点r，i任务r，m=0(对于所有r=I，O和m！=I) DT任务r，m任务s，n=f节点r，i任务r，m+f节点s，j任务s，n+Dn节点r，i节点，j-2 dtr，m任务s，n>=dt任务r，m任务t，l+dt任务t，l任务s，n-1 DT任务r，m任务%s，n+Dt任务%s，n任务r，m<；=1

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

推荐答案

我不确定如何获得最佳答案，因为该问题包含许多未完全指定的细节引用。 例如，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.

其他方法是为不同的 毕竟，你提出的问题表明你只是 写下一个关于不同变量的大的不等式系统 方式。

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

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

而不是函数应用程序。