Решение простой TSP с использованием Z3

Вы можете сформулировать свою проблему TSP как проблему ILP. Теперь вопрос заключается в том, как кодировать TSP как ILP. Есть два хорошо известных ответа: Миллер-Такер. –Землин и Данциг – Фулкерсон – Джонсон.

Основная идея такова: допустим, у нас есть n городов. Обозначим через d_ij расстояние между городами i и j, а через x_{ij} обозначим логическое значение (0 или 1) независимо от того, содержит ли TSP ребро от i до j. Тогда поиск наименьшего тура означает

minimize sum_{i,j} x_{ij} d_{ij}

такие, что x_{ij} описывают цикл. С этими двумя условиями мы получаем один или несколько циклов:

sum_{j} x_{ij} = 1 for all i              exactly one outgoing edge per city
sum_{i} x_{ij} = 1 for all j              exactly one ingoing edge per city

Теперь нам нужно исключить случай, когда решения состоят из нескольких циклов. Мы можем добавить это экспоненциальное число Dantzig-Fulkerson – Условия Джонсона:

sum_{i in S} sum_{j in S} x_{ij} < |S| for all proper subsets S of {1, ..., n}

Обратите внимание, что если наше решение содержит два цикла, то для множества вершин одного из циклов S сумма x_{ij} будет равна |S|. С другой стороны, если есть только один цикл, то сумма x_{ij} никогда не достигнет |S|, например, если вы удалите одну вершину из {1, ..., n}, то количество оставшихся ребер равно n-2, но |S| = п-1.

Конечно, экспоненциальное число ограничений — это не то, что нам нужно, поэтому мы ищем более умный способ исключить случаи подциклов. И вот где Миллер-Такер-Землин вскакивает.

Другой подход состоял бы в том, чтобы просто игнорировать проблему подцикла, вычислить решение и проверить, содержит ли решение подциклы. Если это так, исключите решение, добавив его как ленивое ограничение, и повторяйте, пока не получите решение за один цикл. Ключевое слово здесь — ленивое ограничение.

Вот хороший пример, который может быть вам полезен: http://z3.codeplex.com/SourceControl/changeset/view/1235b3ea24d9#examples/python/hamiltonian/hamiltonian.py