1

我实际上使用 Z3py 来调度解决问题，并且我试图代表一个 2 处理器系统，其中必须完成 4 个不同执行时间的进程。

我的实际数据是： 进程 1：到达 0 和执行时间 4 进程 2：到达 1 和执行时间 3 进程 3：到达 3 和执行时间 5 进程 4：到达 1 和执行时间 2

我实际上是在尝试表示每个进程，同时在相同时间的子进程中分解每个进程，所以我的数据类型是这样的：

Pn = Datatype('Pn')
Pn.declare('1')
Pn.declare('2')
Pn.declare('3')
Pn.declare('4')
Pt = Datatype('Pt')
Pt.declare('1')
Pt.declare('2')
Pt.declare('3')
Pt.declare('4')
Pt.declare('5')
Process = Datatype('Process')
Process.declare('cons' , ('name',Pn) , ('time', Pt))
Process.declare('idle')

其中 pn 和 pt 是进程名称和进程的一部分（进程 1 分为 4 个部分，...）

但是现在我不知道如何代表我的处理器来添加我需要的 3 条规则：唯一性（每个子进程必须由 1 个处理器完成 1 次，并且只有 1 次）检查到达（进程的第一部分不能在到达之前处理）和顺序（流程的每个部分都必须在先例之后处理）所以我正在考虑使用数组来表示我的 2 个处理器与这种声明：

P = Array('P', IntSort() , Process)

但是当我尝试执行它时，我收到一条错误消息：

Traceback (most recent call last):
  File "C:\Users\Alexis\Desktop\test.py", line 16, in <module>
    P = Array('P', IntSort() , Process)
  File "src/api/python\z3.py", line 3887, in Array
  File "src/api/python\z3.py", line 3873, in ArraySort
  File "src/api/python\z3.py", line 56, in _z3_assert
Z3Exception: 'Z3 sort expected'

并且知道我不知道如何处理它......我必须创建一个新的数据类型并想办法添加我的规则吗？或者有没有办法将数据类型添加到数组中，让我创建这样的规则：

unicity = ForAll([x,y] , (Implies(x!=y,P[x]!=P[y])))

提前致谢

4

1 回答 1

2

There is a tutorial on using Datatypes from the Python API. A link to the tutorial is: http://rise4fun.com/Z3Py/tutorialcontent/advanced#h22 It shows how to create a list data-type and use the "create()" method to instantiate a Sort object from the object used when declaring the data-type. For your example, it suffices to add calls to "create()" in the places where you want to use the declared type as a sort. See: http://rise4fun.com/Z3Py/rQ7t

Regarding the rest of the case study you are looking at: it is certainly possible to express the constrsaints you describe using quantifiers and arrays. You could also consider somewhat more efficient encodings:

  • Instead of using an array, use a function declaration. So P would be declared as a unary function: P = Function('P', IntSort(), Process.create()).
  • Using quantifiers for small finite domain problems may be more of an overhead than a benefit. Writing down the constraints directly as a finite conjunction saves the overhead of instantiating quantifiers possibly repeatedly. That said, some quantified axioms can also be optimized. Z3 automatically compiles axioms of the form: ForAll([x,y], Implies(x != y, P(x) != P(y))) into an axioms of the form Forall([x], Pinv(P(x)) == x), where "Pinv" is a fresh function. The new axiom still enforces that P is injective but requires only a linear number of instantiations, linear in the number of occurrences of P(t) for some term 't'.

Have fun!

于 2013-05-16T16:26:51.027 回答