z3 - 使用 z3py 获取 unsat 核心以实现非线性约束
问题描述
我有一组简单但非线性的约束,例如:
v0= Real('v0')
v1= Real('v1')
v2= Real('v2')
v3= Real('v3')
v4= Real('v4')
v5= Real('v5')
v6= Real('v6')
v7= Real('v7')
v8= Real('v8')
v9= Real('v9')
v10= Real('v10')
v11= Real('v11')
v12= Real('v12')
v13= Real('v13')
v14= Real('v14')
v15= Real('v15')
v16= Real('v16')
v17= Real('v17')
v18= Real('v18')
v19= Real('v19')
s = Solver()
s.set(unsat_core=True)
s.add(v0>=0, v0<=1)
s.add(v1>=0, v1<=1)
s.add(v2>=0, v2<=1)
s.add(v3>=0, v3<=1)
s.add(v4>=0, v4<=1)
s.add(v5>=0, v5<=1)
s.add(v6>=0, v6<=1)
s.add(v7>=0, v7<=1)
s.add(v8>=0, v8<=1)
s.add(v9>=0, v9<=1)
s.add(v10>=0, v10<=1)
s.add(v11>=0, v11<=1)
s.add(v12>=0, v12<=1)
s.add(v13>=0, v13<=1)
s.add(v14>=0, v14<=1)
s.add(v15>=0, v15<=1)
s.add(v16>=0, v16<=1)
s.add(v17>=0, v17<=1)
s.add(v18>=0, v18<=1)
s.add(v19>=0, v19<=1)
s.add(v0==v1*v4)
s.add(v4==(v5+v6+v19)-(v5*v6+v5*v19+v6*v19)+(v5*v6*v19))
s.add(v6==v7*v11)
s.add(v11==(v12+v15+v18)-(v12*v15+v12*v18+v15*v18)+(v12*v15*v18))
s.add(v15==(v16+v17)-(v16*v17))
s.add(v12==v13*v14)
s.add(v7==(v8+v9+v10)-(v8*v9+v8*v10+v9*v10)+(v8*v9*v10))
s.add(v1==(v2+v3)-(v2*v3))
(这基本上是概率计算)
我想添加一组约束,例如
v0_pred = Bool('v0_pred')
s.add(Implies(v0_pred, v0==0.0046))
v19_pred = Bool('v19_pred')
s.add(Implies(v19_pred, v19==0.015))
v16_pred = Bool('v16_pred')
s.add(Implies(v16_pred, v16==0.0094))
v12_pred = Bool('v12_pred')
s.add(Implies(v12_pred, v12==0.0172))
v5_pred = Bool('v5_pred')
s.add(Implies(v5_pred, v5==0.0038))
result = s.check(v0_pred,v19_pred,v16_pred,v12_pred,v5_pred)
并将这 5 个约束跟踪到 unsat 核心。但是,通常情况下,求解器报告它找不到解决方案(未知)。如果我只是这样做s.add(v0==0.0046, v19==0.015, v16==0.0094, v12==0.0172, v5==0.0038)
,它会很好地工作并快速找到解决方案(sat)。但是仅使用s.add()
我无法获得 unsat 案例的 unsat 核心。我究竟做错了什么?
UPD:“未知”问题的示例Solver.assert_and_track()
:
from z3 import *
def is_number(s):
try:
float(s.numerator_as_long())
return True
except AttributeError:
return False
v0= Real('v0')
v1= Real('v1')
v2= Real('v2')
v3= Real('v3')
v4= Real('v4')
v5= Real('v5')
v6= Real('v6')
v7= Real('v7')
v8= Real('v8')
v9= Real('v9')
v10= Real('v10')
v11= Real('v11')
v12= Real('v12')
v13= Real('v13')
v14= Real('v14')
v15= Real('v15')
v16= Real('v16')
v17= Real('v17')
v18= Real('v18')
v19= Real('v19')
s = Solver()
s.set(unsat_core=True)
s.add(v0>=0, v0<=1)
s.add(v1>=0, v1<=1)
s.add(v2>=0, v2<=1)
s.add(v3>=0, v3<=1)
s.add(v4>=0, v4<=1)
s.add(v5>=0, v5<=1)
s.add(v6>=0, v6<=1)
s.add(v7>=0, v7<=1)
s.add(v8>=0, v8<=1)
s.add(v9>=0, v9<=1)
s.add(v10>=0, v10<=1)
s.add(v11>=0, v11<=1)
s.add(v12>=0, v12<=1)
s.add(v13>=0, v13<=1)
s.add(v14>=0, v14<=1)
s.add(v15>=0, v15<=1)
s.add(v16>=0, v16<=1)
s.add(v17>=0, v17<=1)
s.add(v18>=0, v18<=1)
s.add(v19>=0, v19<=1)
s.add(v0==v1*v4)
s.add(v4==(v5+v6+v19)-(v5*v6+v5*v19+v6*v19)+(v5*v6*v19))
s.add(v6==v7*v11)
s.add(v11==(v12+v15+v18)-(v12*v15+v12*v18+v15*v18)+(v12*v15*v18))
s.add(v15==(v16+v17)-(v16*v17))
s.add(v12==v13*v14)
s.add(v7==(v8+v9+v10)-(v8*v9+v8*v10+v9*v10)+(v8*v9*v10))
s.add(v1==(v2+v3)-(v2*v3))
v0_pred = Bool('v0_pred')
s.assert_and_track(v0==0.0046, v0_pred)
v19_pred = Bool('v19_pred')
s.assert_and_track(v19==0.015, v19_pred)
v16_pred = Bool('v16_pred')
s.assert_and_track(v16==0.0094, v16_pred)
v12_pred = Bool('v12_pred')
s.assert_and_track(v12==0.0172, v12_pred)
v5_pred = Bool('v5_pred')
s.assert_and_track(v5==0.0038, v5_pred)
result = s.check()
print result
if result == z3.sat:
m = s.model()
for d in m.decls():
if (is_number(m[d])):
print "%s = %s" % (d.name(), float(m[d].numerator_as_long())/float(m[d].denominator_as_long()))
else:
print "%s = %s" % (d.name(), m[d])
elif result == z3.unsat:
print s.unsat_core()
它返回 me unknown
,虽然它是sat
,并且如果使用Solver.add()
而不是解决。
解决方案
您应该使用assert_and_track
将它们跟踪到未饱和的核心中。看到这个:https ://z3prover.github.io/api/html/classz3py_1_1_solver.html#ad1255f8f9ba8926bb04e1e2ab38c8c15
处理非线性
由于您的问题包括非线性约束,z3 可能很难处理具有默认设置的那些。启发式选择取决于很多因素,选择正确的策略更像是一门艺术。对于您发布的问题,以下工作:
t = z3.Then('simplify', 'qfnra-nlsat')
s = t.solver()
result = s.check()
对于其他问题,您的里程可能会有所不同。但我怀疑上述策略应该对你有用,只要你的问题结构保持不变。
推荐阅读
- python-3.x - 对象没有属性错误(Python 代码问题)- Outlook 全局地址列表信息
- python - 如果行中的值与另一列中的任何位置匹配,则删除 Pandas 数据框中的行
- c++ - 如何插入像素坐标而不是像素值?需要它来为相机生成校正重映射
- c# - 打开文件对话框时应用程序冻结
- swift - Swift for TensorFlow - dyld:找不到符号:_$sSly7ElementQz5IndexQzcigTq
- cordova - 如何在没有此错误的情况下安装分叉和自定义的离子原生科尔多瓦插件?
- c# - 通过 X 坐标迭代列表列表?
- json - 从 Angular 7 服务传递时,ipcRenderer 参数 JSON 对象如何丢失数据?
- c# - DocumentEditor InsertBefore 似乎无法在文档中找到节点
- python - 如何在由类对象组成的列表中查找特定值的最大元素索引?