Z3在变量决策过程中可以调用python函数吗？答案

【问题标题】：Can Z3 call python function during decision making of variables?Z3在变量决策过程中可以调用python函数吗？
【发布时间】：2013-07-24 20:17:41
【问题描述】：

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

这是我的代码：我有一个函数def getVal(n1,n2):，其中n1, n2 是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 求解器对此类问题进行编码以找到最佳路径点序列吗？

【问题讨论】：

标签： z3 z3py

【解决方案1】：

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

【讨论】：

您好，感谢您的回复。我的问题是：我有一个包含大量节点的全连接图。每条边都有成本。给出了开始和结束节点。我想应用增量 Sat 求解来找到从开始到结束节点的最短路径。这几乎就像一个带有其他约束的 TSP 问题。

【解决方案2】：

我认为您不能在 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，最后一个整数代表权重。

【讨论】：