Получите ядро ​​unsat с z3py для нелинейных ограничений

У меня есть набор простых, но нелинейных ограничений, например:

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), он отлично работает и быстро находит решение (Суббота). Но используя только s.add(), я не могу получить ядро ​​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()

Он возвращает мне unknown, в то время как это sat, и решается, если вместо этого использовать Solver.add().

1
0
80
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 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()

С другими проблемами ваш пробег может отличаться. Но я подозреваю, что описанная выше тактика должна работать на вас, пока структура вашей проблемы остается неизменной.

Спасибо, это решило мою проблему. Но я не понимаю, в чем разница в использовании s.add (Подразумевает ..) и s.assert_and_track ()? Используют ли они в фоновом режиме разные решатели?

Vilena 27.08.2018 17:06

Нет, извините, после дополнительных экспериментов я столкнулся с той же проблемой - решатель не решает тот же набор ограничений (дает неизвестное), с которым он легко справляется с помощью только s.add ().

Vilena 27.08.2018 17:30

Пожалуйста, опубликуйте минимально работающий проверяемый пример. (то есть тот, который мы можем загрузить в z3 напрямую) со всем записанным импортом и т. д.

alias 27.08.2018 18:33

Большое спасибо! Это работает с уловкой Tactics. Где я могу найти справочник об использовании тактики? И можно ли это применить таким же образом с решателем Optimize () вместо Solver ()?

Vilena 29.08.2018 17:49

Я не думаю, что тактика так хорошо задокументирована, если вообще существует. Возможно, вы захотите спросить на их странице проблем с github. (github.com/Z3Prover/z3/issues)

alias 29.08.2018 18:14

Здесь есть элементарная документация: cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.ht‌ m

alias 30.08.2018 17:52

Другие вопросы по теме