1

我正在尝试解决一个问题，例如我有4 点，每两点之间都有成本。现在我想找到总成本小于界限的节点序列。我写了一个代码，但它似乎不起作用。主要问题是我已经定义了一个 python 函数并试图在约束中调用它。

这是我的代码：我有一个函数def getVal(n1,n2): where n1, n2are Int Sort。该行将Nodes = [ Int("n_%s" % (i)) for i in range(totalNodeNumber) ]4 个点定义为 Int 排序，当我添加约束时s.add(getVal(Nodes[0], Nodes[1]) + getVal(Nodes[1], Nodes[2]) < 100)，它会立即调用getVal函数。但我想要的是，当 Z3 将决定 Nodes[0]、Nodes[1]、Nodes[2]、Nodes[3] 的值时，应该调用该函数来获取点之间的成本。

from z3 import *
import random

totalNodeNumber = 4
Nodes = [ Int("n_%s" % (i)) for i in range(totalNodeNumber) ]
def getVal(n1,n2):
    # I need n1 and n2 values those assigned by Z3
    cost = random.randint(1,20)
    print cost
    return IntVal(cost)

s = Solver()

#constraint: Each Nodes value should be distinct
nodes_index_distinct_constraint  = Distinct(Nodes)
s.add(nodes_index_distinct_constraint)

#constraint: Each Nodes value should be between 0 and totalNodeNumber
def get_node_index_value_constraint(i):
    return And(Nodes[i] >= 0, Nodes[i] < totalNodeNumber)
nodes_index_constraint  = [ get_node_index_value_constraint(i) for i in range(totalNodeNumber)]
s.add(nodes_index_constraint)

#constraint: Problem with this constraint
# Here is the problem it's just called python getVal function twice without assiging Nodes[0],Nodes[1],Nodes[2] values
# But I want to implement that - Z3 will call python function during his decission making of variables
s.add(getVal(Nodes[0], Nodes[1]) + getVal(Nodes[1], Nodes[2]) + getVal(Nodes[2], Nodes[3]) < 100)

if s.check() == sat:
    print "SAT"
    print "Model: "
    m = s.model()
    nodeIndex = [ m.evaluate(Nodes[i]) for i in range(totalNodeNumber) ]
    print nodeIndex
else:
    print "UNSAT"
    print "No solution found !!"

如果这不是解决问题的正确方法，那么您能否告诉我其他解决问题的方法。我可以使用 Z3 求解器对此类问题进行编码以找到最佳的航点序列吗？

4

2 回答 2

0

我不明白你需要解决什么问题。毫无疑问，制定 getVal 的方式没有意义。它不使用参数 n1、n2。如果要检查模型产生的值，则在 Z3 从对 check() 的调用中返回后执行此操作。

于 2013-08-01T20:00:58.263 回答
0

我认为您不能在 SMT 逻辑中使用 python 函数。您可以选择将 getVal 定义为这样的函数

getVal = Function('getVal',IntSort(),IntSort(),IntSort())

并将边缘权重约束为

s.add(And(getVal(0,1)==1,getVal(1,2)==2,getVal(0,2)==3))

getVal 的前两个输入参数代表节点 ID，最后一个整数代表权重。

于 2015-11-10T20:30:55.003 回答