Basi c способ перечислить отношение в z3py - PullRequest
Новая
       4

Basi c способ перечислить отношение в z3py

0 голосов
/ 09 февраля 2020

Я хочу построить базовую c модель, которая ищет отношение между двумя объектами.

Предположение)

  • Объект: Существуют A и B, принадлежащие классу Person .
  • Правило: человек может убить человека. Человек становится мертвым, если кто-то убил его.
  • Факт: А мертв. B не умер.

Ожидаемый результат)

  • B убит A
  • B убит A. A убит A.
  • A убит А.

Мой код относится к примеру программы, распространяемой официальными смертными Сократом. Однако я не могу понять, как описать это отношение. 

from z3 import *

Person, (a,b) = EnumSort("Person",["a","b"])

Kill = Function('Kill', Person,Person, BoolSort())
Dead = Function('Dead', Person, BoolSort())

# free variables used in forall must be declared Const in python
x = Const('x', Person)
y = Const('y', Person)

s = Solver()

s.add(ForAll([x,y],Implies(Kill(x,y),Dead(y))))
s.add(Dead(a))
s.add(Not(Dead(b)))

print(s.check()) # prints sat so axioms are coherent    
m=s.model()
print(m)

1 Ответ

0 голосов
/ 10 февраля 2020

Ты совсем близко! Просто добавьте следующее в конце: 

res = s.check()

if res == sat:
   m = s.model()
   print "Is A dead   : %s" % m.eval(Dead(a))
   print "Is B dead   : %s" % m.eval(Dead(b))
   print "Did A kill A: %s" % m.eval(Kill(a, a))
   print "Did A kill B: %s" % m.eval(Kill(a, b))
   print "Did B kill A: %s" % m.eval(Kill(b, a))
   print "Did B kill B: %s" % m.eval(Kill(b, b))
else:
    print "Not satisfiable, got: %s" % res

С этим z3 говорит: 

Is A dead   : True
Is B dead   : False
Did A kill A: False
Did A kill B: False
Did B kill A: False
Did B kill B: False

Модель может выглядеть немного странно. Если A мертв, кто его убил? Найденная модель говорит, что никто никого не убивал. Мгновенное размышление показывает, что оно совершенно соответствует аксиомам, которые вы представили: кто-то может просто начать с мертвой точки. Но, возможно, это не то, что вы хотели. Итак, давайте добавим кое-что к эффекту: если ты мертв, кто-то, должно быть, убил тебя: 

s.add(ForAll([x], Implies(Dead(x), Exists([y], Kill(y, x)))))

Теперь мы получаем: 

Is A dead   : True
Is B dead   : False
Did A kill A: True
Did A kill B: False
Did B kill A: True
Did B kill B: False

Это лучше! Но о, теперь z3 говорит, что A был убит как A, так и B. Возможно, нам нужно что-то сказать о том, что если кто-то умер, то только один человек убил его. Или, по крайней мере, мертвец не был вовлечен. (Сначала было бы немного сложнее моделировать, но с двумя Person в вашем мире не должно быть так сложно.) Итак, давайте просто запретим самоубийство: 

s.add(ForAll([x], Not(Kill(x, x))))

, которое производит: 

Is A dead   : True
Is B dead   : False
Did A kill A: False
Did A kill B: False
Did B kill A: True
Did B kill B: False

Это выглядит вполне разумно!

В то время как с такими задачами забавно играть, решатели SMT обычно плохо разбираются в присутствии квантификаторов. С такими конечными моделями проблем не будет. Но если вы начнете включать объекты типа Int, Real et c., Особенно с чередующимися квантификаторами, z3 вряд ли ответит на подобные запросы. Скорее всего, вы получите ответ unknown, который позволяет SMT-решателям сказать, что проблема слишком сложна для базовых рассуждений на основе SMT.

Перечисление всех возможных решений

Если вы не хотите добавлять новые аксиомы, а просто хотите найти все модели, которые удовлетворяют вашему первоначальному набору, вы можете сделать это, добавив блокирующие предложения. То есть вы можете получить модель, найти значения, которые она задает, и утверждать, что эти значения не годятся; и повторить. Существует много ответов на переполнение стека, описывающих, как это сделать, см. Этот пример, например: (Z3Py), проверяющий все решения для уравнения Вам необходимо соответствующим образом изменить их, чтобы учесть неинтерпретированные функции, которые у вас есть здесь Это немного многословно, но не особенно сложно. Не стесняйтесь задавать новый вопрос, если вам трудно!

...