Z3py SMT编码跟随变量及公式 [英] Z3py SMT coding following variables and the formulas

问题描述

我对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)，如果Oi是第一个生成的输出，并且Oj是第二个生成的输出，则G k是在生成Oi之后和生成Oj之前调度的节点集合，但是如果Oj是在生成O之前生成的，则G k包含在生成之前调度的所有块。 节点的调度由另一个程序给出。 例如，在上面的框图中，节点的调度以及输出的生成如下所示：

• 计划的第一个节点=节点1
• 计划的第二个节点=节点2
• 计划的第三个节点=节点5
• 生成的输出=O₁
• 计划的第四个节点=节点3
• 计划的第五个节点=节点6
• 生成的输出=O₂
• 计划的第六个节点=节点4
• 计划的第五个节点=节点7
• 生成的输出=O₃

因此，从上面我们可以说(O¹，O²)的G¹>是={节点3，节点6}

但(O₂，O₁)的G₂为={Node1，Node2，Node5}

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

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

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

• f_{节点r，i任务r，M表示是否 节点r，i映射到任务r，m}
• Dn_{Noder，iNodes，j}表示 节点_s，j取决于节点_r，i，即是否存在从节点_r，i到节点_s，j的路径
• DT_{TASKr，mTASKs，N}表示 任务_%s，n取决于任务_r，m
• M_{任务r，m表示是否有节点映射到任务R，M}

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

1. 最小化(&Sigma；_r，m M_任务r，M)
2. M_任务r，M= F_{节点r，I任务r，M}(适用于所有I)
3. &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(一次只能将一个节点映射到一个任务，但一个任务一次可以映射到几个节点)
4. f_{节点r，i任务%s，m}=0(对于所有r！=)
5. f_{节点r，i任务r，m}=1(对于所有r=I，O和m=I)
6. f_{节点r，i任务r，m}=0(对于所有r=I，O和m！=I)
7. DT任务r，m任务s，n=f节点r，i任务r，m+f节点s，j任务_s，n+Dn_节点r，i节点<子>，j-2
8. dt_r，m任务_s，n>=dt_{任务r，m任务t，l}+dt_{任务t，l任务s，n}-1
9. 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())

而不是函数应用程序。

这篇关于Z3py SMT编码跟随变量及公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！