使用 z3py 获取 unsat 核心以实现非线性约束

Question

我有一组简单但非线性的约束，例如：

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 核心。但是，求解器通常会报告它找不到解决方案（unknown）。如果我只做s.add(v0==0.0046, v19==0.015, v16==0.0094, v12==0.0172, v5==0.0038)，它会很好地工作并快速找到解决方案（sat）。但是仅使用s.add() 我无法获得未饱和案例的未饱和核心。我做错了什么？

更新： 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()

它返回我unknown，而它是sat，如果使用Solver.add() 来解决。

Answer 1

您应该使用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()

遇到其他问题，您的里程可能会有所不同。但我怀疑上述策略应该对你有用，只要你的问题结构保持不变。