#python #graph #z3 #sat
#python #График #z3 #сидел
Вопрос:
По сути, я пытаюсь найти путь от v1 до v2 на графике, но некоторые узлы окрашены, и мы не можем их посетить.
Я понимаю ограничения, но часть, с которой у меня действительно возникла проблема, заключается в понимании того, как добавить возможные ходы к ограничениям.
Если я настрою логические значения таким образом
nodes = [Int('"n%i_%i" % (i, j)) for i in range(len(G))]
moves = []
for i in range(len(G)):
moves = ?
Условием было бы, чтобы узлы находились рядом друг с другом, поэтому i = i и j = j 1 (или i = i 1 и j = j) и что узлу разрешено посещать, поэтому path = True, что является особенностью графика. Так, например, G[i] [j] == True.
Я бы использовал что-то вроде (или(И(узлы находятся рядом друг с другом), (G [i] [j] == True))) И как я могу выразить, что узлы находятся рядом друг с другом?
Спасибо!!
Комментарии:
1. Вы пытаетесь реализовать поиск пути в представлении матрицы смежности? Что конкретно вы подразумеваете под «цветными» узлами? Или вы пытаетесь пересечь 2d-сетку, начиная с (0,0) и двигаясь только вниз и вправо?
2. Спасибо за ваш комментарий. Таким образом, цветные означают, что мы не можем их посетить, и узлы имеют координаты, подобные 2d-сетке, но мы не обязательно начинаем с (0,0). Да, мы движемся только в направлении вправо и вниз.
Ответ №1:
Поскольку я не понимаю, что вы имеете в виду под цветными узлами, здесь будет предварительное решение:
Предикаты
Сначала мы определяем некоторые предикаты и то, что они интуитивно означают для нас:
p(X, Y, n) обозначает, что мы посещаем узел в координатах X, Y в момент времени n, где момент времени начинается с 0 и достигает длины G.
go(right, n) обозначает, что мы идем вправо в момент времени n.
go(down, n) обозначает, что мы спускаемся в момент времени n.
Кодирование
Начальное состояние
Изначально мы знаем, что p(Start_X, Start_Y, 0) это правда. Следовательно, мы добавляем предложение unit [p(Start_X, Start_Y, 0)]
Движение
В каждый момент времени мы должны двигаться. Поэтому для каждого момента времени t добавляйте предложения [go(right, t), go(down, t)] , и [not go(right, t), not go(down, t)] это также известно как ограничение ровно один раз, т. Е. Мы можем двигаться либо вправо, либо вниз.
Теперь нам нужно связать предикат p и предикат go: если p(X, Y, T) истинно, и go(right, T), то p(X 1, Y, T 1) истинно. Следовательно, добавьте предложения [not p(X, Y, T), not go(right, T), p(X 1, Y, T 1)] .
Аналогичным образом вы можете закодировать действие «go down».
Конечное состояние
Теперь мы должны убедиться, что мы, наконец, достигли узла v2. Пожалуйста, обратите внимание, что недостаточно добавить, что p(v2_x, v2_y, t) это верно для некоторого момента времени. Вместо этого мы должны убедиться, что модели, нарушающие это условие, исключены: поскольку мы можем двигаться только вниз или вправо, мы знаем, что мы не можем посещать узлы, которые находятся ниже v2 или справа от него. Следовательно, мы добавляем единичные предложения вида [not p(X, Y, t)] , где t — расстояние от v1 и v2.
Вспомогательный
Теперь решение может быть считано из вашей модели, но ваша модель может выглядеть немного странно в том смысле, что несколько p-предикатов являются истинными в один и тот же момент времени. В общем, это не повредит, но может быть исключено, если вы так скажете: [not p(X1, Y1, t), not p(X2, Y2, t)] для каждого t и различных координат.