проблемы планирования z3 и блоки мира - PullRequest
Новая
       9

проблемы планирования z3 и блоки мира

1 голос
/ 26 февраля 2020

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

#!/usr/bin/env python
from z3 import *

blk = DeclareSort ("Block")
On = Function ("On", blk , blk, BoolSort () )
Above = Function ("Above", blk , blk, BoolSort () )

a, b, c, x, y, z = Consts ("a b c x y z", blk )

P0 = And(On(a,b), On(b,c))
P1 = ForAll([x, y], Implies(On(x,y), Above(x,y)))
P2 = ForAll([x, y, z], Implies(And(On(x,y), Above(z, y)), Above(x,y)))


solver = Solver()

solver.add(And(P0,P1,P2))

print solver.check()
print solver.model()

, но это выводит меня на что-то, похожее на gibberi sh. Как я могу это исправить? и где я могу найти хороший ресурс для кодирования планирования проблем для SAT? Я видел формализм STRIPS, но мне неясно, как кодировать условия pre + post в logi c props. Я бы подумал, что это не так, но мне не очень повезло с этим, и, похоже, этот метод основан на новых ограничениях, которые будут созданы из эффектов / постусловий после того, как в модели будут выполнены предварительные условия. И кажется, что z3 не может сделать это без явно запрограммированных условий записи.

1 Ответ

2 голосов
/ 26 февраля 2020

Такие проблемы, безусловно, решаются с помощью Z3 и любого SMT-решателя в целом. Но вы не получите приятных возможностей выделенной системы по понятным причинам. Кодирование может быть более многословным, и, как вы узнали, модели интерпретации могут быть довольно хитрыми.

Я думаю, что ваше кодирование - хорошее начало, но вам будет лучше, если сделать Block перечислимой сортировкой и объявить блоки в вашей системе явно. Это сделает кодирование намного ближе к тому, как обычно кодируются системы планирования, а также поможет интерпретировать сами модели.

Исходя из этого, вот как я go расскажу о кодировании вашей проблемы, предполагая, что мы жить во вселенной с тремя блоками с именами A, B и C: 

from z3 import *

Block, (A, B, C) = EnumSort('Block', ('A', 'B', 'C'))
On    = Function ("On",    Block, Block, BoolSort())
Above = Function ("Above", Block, Block, BoolSort())

objects = [A, B, C]

solver = Solver()
solver.add(And(On(A, B), On(B, C)))

x, y, z = Consts ("x y z", Block)
solver.add(ForAll([x, y], Implies(On(x, y), Above(x, y))))
solver.add(ForAll([x, y, z], Implies(And(On(x, z), Above(z, y)), Above(x, y))))
solver.add(ForAll([x], Not(On(x, x))))
solver.add(ForAll([x], Not(Above(x, x))))

if solver.check() == sat:
    print "sat"
    m = solver.model()
    for i in objects:
        for j in objects:
            if m.evaluate(On(i, j)):
                print "On(%s, %s)" % (i, j)
            if m.evaluate(Above(i, j)):
                print "Above(%s, %s)" % (i, j)
else:
    print "unsat"

(Обратите внимание, что мне пришлось настроить ваш P2, который выглядел не совсем правильно. Я также добавил две аксиомы, говоря, что On и Above нерефлексивны. Но вы можете изменить и поиграть с различными аксиомами и посмотреть, какие модели вы получаете.)

Для этого ввода z3 говорит: 

sat
On(A, B)
Above(A, B)
Above(A, C)
On(B, C)
Above(B, C)

, который является допустимым сценарием, удовлетворяющим всем ограничениям.

Я должен отметить, что решатели SMT обычно не способны к количественным рассуждениям. Но, сохраняя Вселенную конечной (и маленькой!), Они могут довольно хорошо справиться с любым количеством таких аксиом. Если вы представите объекты из бесконечной области, такие как Int, Real и др. c., Вещи станут более интересными и, возможно, слишком сложными для z3. Но вам не нужно такое причудливое кодирование для классовых c проблем с блоком / планированием.

Надеюсь, это поможет вам начать!

...