Z3py SMT coding following variables and the formul

问题:

I am really new to Z3 and SMT solvers. I have the following problem which I don't know how to code in Z3py.

In the above diagram N is set of nodes, thus N = {Node1, Node2, Node3, Node4, Node5, Node6, Node7}

I is set of Inputs, I = {I₁, I₂, I₃, I₄}

O is set of Outputs, O = {O₁, O₂, O₃}

G is a group where for any consecutive 2 outputs (O_i, O_j), if O_i is first output generated and O_j is second output generated then, G_k is set of nodes that were scheduled after the generation of O_i and before the generation of O_j, but if O_j was generated before O_i then G_k contains all the blocks that were scheduled before O_j was generated. The scheduling of the nodes is given by another program. For example in the above block diagram the scheduling of nodes along with generation of output is as follows:

• First node scheduled = Node1
• Second node scheduled = Node2
• Third node scheduled = Node5
• Output generated = O₁
• Fourth node scheduled = Node3
• Fifth node scheduled = Node6
• Output generated = O₂
• Sixth node scheduled = Node4
• Fifth node scheduled = Node7
• Output generated = O₃

Thus from above we can say that G₁ for (O₁, O₂) is = {Node3, Node6}

But G₂ for (O₂, O₁) is = {Node1, Node2, Node5}

To execute each node we need a task, a task can implement 1 node or a set of nodes at a time.

Node_r,i denotes i^th node in group G_r. Task_r,m denotes m^th task in group G_r.

The boolean variables (can either be 0 or 1) :

• f_{Noder,iTaskr,m} represents if Node_r,i is mapped to Task_r,m
• DN_{Noder,iNodes,j} represents if Node_s,j depends on Node_r,i i.e. if there is a path from Node_r,i to Node_s,j
• DT_{Taskr,mTasks,n} represents if Task_s,n depends on Task_r,m
• M_Taskr,m represents if there is any node mapped on to Task_r,m

Based on the above information I have to formulate the following equations in SMT.

1. Minimize ( Σ_r,m M_Taskr,m )
2. M_Taskr,m >= f_{Noder,iTaskr,m} (for all i)
3. Σ_m f_{Noder,iTaskr,m} = 1 (for all r != I,O) example: f_{Noder,iTaskr,m} + f_{Noder,iTaskr,m+1} + f_{Noder,iTaskr,m+2} = 1 + 0 + 0 = This tells us that Node_r,i is mapped to Task_r,m since f_{Noder,iTaskr,m} = 1 (only one node can be mapped to 1 task at a time but a task can be mapped to several nodes at a time)
4. f_{Noder,iTasks,m} = 0 (for all r != s)
5. f_{Noder,iTaskr,m} = 1 (for all r = I,O and m = i)
6. f_{Noder,iTaskr,m} = 0 (for all r = I,O and m != i)
7. DT_{Taskr,mTasks,n} >= f_{Noder,iTaskr,m} + f_{Nodes,jTasks,n} + DN_{Noder,iNodes,j} - 2
8. DT_{Taskr,mTasks,n} >= DT_{Taskr,mTaskt,l} + DT_{Taskt,lTasks,n} - 1
9. DT_{Taskr,mTasks,n} + DT_{Tasks,nTaskr,m} <= 1

I don't understand how to represent the variables and these formulas in SMT format.

回答1:

I am not sure how to best answer because the question contains a lot of references to specifics that are not fully specified. For example, what is I, and O? You probably are asking how to add a system of linear inequalities. Or how to specify problems with integer variables that can be either 0 or 1.

One approach is to introduce functions as follows:

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

Then 'a' is a function that maps pairs of integers to an integer. You can declare function 'n' in a similar way (but I guess your example actually has some typos and you use n both as a function and as an index variable). You can declare functions f, h, q in similar ways too.

Then in python you can write:

     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)

This adds the equality constraints on f that you specified. The other equality and inequality constraints can be added in similar ways. In the end you ask whether the resulting state is satisfiable.

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

Other approaches are that you declare distinct constants for the different versions of f. After all your suggested problem indicates that you are just writing down a large system of inequalities over variables created in different ways.

E.g., you can create and the constant v:

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

instead of the function application.