Неизвестный результат в z3 python для типа Int - PullRequest
Новая
       77

Неизвестный результат в z3 python для типа Int

0 голосов
/ 19 марта 2020

Я пытался решить определенный набор ограничений, используя z3 в python. Мой код: 

import math
from z3 import *

### declaration
n_co2 = []
c_co2 = []
alpha = []
beta = []
m_dot_air = []
n_pir = []
pir_sensor = []

for i  in range(2):
    c_co2.append(Real('c_co2_'+str(i)))
    n_pir.append(Real('n_pir_'+str(i)))

n_co2.append(Real('n_co2_'+str(0)))
alpha.append(Real('alpha_'+str(0)))
beta.append(Real('beta_'+str(0)))
m_dot_air.append(Real('m_dot_air_'+str(0)))   
pir_sensor.append(Real('pir_sensor_'+str(0)))

s = Solver()

s.add(n_co2[0]>0)
s.add(c_co2[0]>0)
s.add(c_co2[1]>=0.95*c_co2[0])
s.add(c_co2[1]<=1.05*c_co2[0])
s.add(n_co2[0]>=0.95*n_pir[1])
s.add(n_co2[0]<=1.05*n_pir[1])
s.add(c_co2[1]>0)
s.add(alpha[0]<=-1)
s.add(beta[0]>0)
s.add(m_dot_air[0]>0)
s.add(alpha[0]==-1*(1+ m_dot_air[0] + (m_dot_air[0]**2)/2.0 + (m_dot_air[0]**3)/6.0 ))
s.add(beta[0]== (1-alpha[0])/m_dot_air[0])
s.add(n_co2[0]== (c_co2[1]-alpha[0]*c_co2[0])/(beta[0]*19.6)-(m_dot_air[0]*339)/19.6)
s.add(n_pir[1]>=0)
s.add(pir_sensor[0]>=-1)
s.add(pir_sensor[0]<=1)
s.add(Not(pir_sensor[0]==0))
s.add(n_pir[1]==(n_pir[0]+pir_sensor[0]))

#### testing
s.add(pir_sensor[0]==1)
s.add(n_pir[1]==1)
s.add(n_co2[0]==1)

print(s.check())
print(s.reason_unknown())
print(s.model())

Вывод кода: 

sat
[c_co2_0 = 355,
 c_co2_1 = 1841/5,
 m_dot_air_0 = 1,
 n_co2_0 = 1,
 n_pir_1 = 1,
 pir_sensor_0 = 1,
 n_pir_0 = 0,
 beta_0 = 11/3,
 alpha_0 = -8/3,
 /0 = [(19723/15, 1078/15) -> 1793/98,
       (11/3, 1) -> 11/3,
       else -> 0]]

Какое значение имеет "/ 0 = ..." часть модели вывода.

Но когда я изменяю тип n_pir с Real на Int, z3 не может решить эту проблему. Хотя мы видели, что у нас есть решение Int для n_pir. Причина неизвестна: 

smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))

Как решить эту проблему? Может ли кто-нибудь представить обоснование этой проблемы?

1 Ответ

0 голосов
/ 19 марта 2020

Для части "/ 0": это внутренне генерируемое ограничение от преобразования реальных в int решения. Вы можете полностью игнорировать это. На самом деле, вы не должны даже смотреть на это значение, это артефакт привязок z3py и, вероятно, должно быть скрыто от пользователя.

На ваш вопрос о том, почему вы не можете сделать «Реальным» 'Int'. Это потому, что у вас есть нелинейный набор уравнений (где вы умножаете или делите две переменные), и нелинейная целочисленная арифметика c вообще неразрешима. (Принимая во внимание, что нелинейная вещественная арифметика c является разрешимой.) Таким образом, когда вы используете 'Int', решатель просто использует некоторую эвристику, и в этом случае происходит сбой и говорит неизвестно. Это вполне ожидаемо. Прочтите этот ответ для более подробной информации: Как Z3 обрабатывает нелинейную целочисленную арифметику c?

Z3 действительно поставляется с решателем NRA, вы можете попробовать. Объявите свой решатель как: 

s = SolverFor("NRA")

Но, опять же, вы зависите от эвристики и можете или не можете получить решение. Кроме того, следите за константами принудительного связывания z3py, когда вы смешиваете и подбираете арифметику c таким образом. Хороший способ - написать: 

print s.sexpr()

, прежде чем позвонить s.check(), взглянуть на вывод и убедиться, что перевод выполнен правильно. Подробнее об этом см. Этот вопрос: Python и Z3: целые числа и числа с плавающей запятой, как правильно ими управлять?

...