Z3, гамильтонов граф, пропозициональная логика - PullRequest
Новая
       5

Z3, гамильтонов граф, пропозициональная логика

0 голосов
/ 01 февраля 2012

Я надеюсь на предложения о том, как это сделать:

Определение: Ненаправленный граф G определяется множеством V вершин и множеством E ребер, где каждое ребро является подмножеством V размера два, то есть неупорядоченной парой {u, v} вершин. Цикл длины k в G - это последовательность v_1, ..., v_k различных вершин, для которых {v_1, v_2}, {v_2, v_3}, ..., {v_k-1, v_k}, {v_k, v_1 } - все ребра G. Гамильтонов цикл в G - это цикл длины n = | V |, т. е. цикл, проходящий через каждую вершину графа ровно один раз. Мы называем G гамильтонианом, если он имеет гамильтонов цикл.

Проблема: Предоставьте логическую формулировку высказывания следующей задачи решения: направленный граф G, является ли гамильтоновым? Состав будет проверен Z3.

Формат ввода будет: 

4
0 1
1 2
2 3
3 0
1 3

где первое число представляет количество вершин, а остальные пары - все ребра в G.

Выходные данные должны быть: 0 1 2 3

Очевидно, что на выходе всегда будет некоторая перестановка чисел 1, ..., n-1, где n = | V | но я не понимаю, как работать с целыми числами, используя только логику предложения.

Любой совет приветствуется.

Привет.

Вот решение, которое работает для данного ввода. Если бы я мог написать процедуру на Perl, которая бы вырабатывала комбинации (n Выберите k) ребер, я мог бы обобщить это на любое количество входных данных: 

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)

(declare-const e1 Bool)
(declare-const e2 Bool)
(declare-const e3 Bool)
(declare-const e4 Bool)
(declare-const e5 Bool)

(assert (xor (and e1 e2 e3 e4) (and e1 e2 e3 e5) (and e1 e2 e4 e5) (and e1 e3 e4 e5) (and e2 e3 e4 e5)))

(assert (and v0 v1 v2 v3))

(assert (=> e1 (and v0 v1)))
(assert (=> e2 (and v1 v2)))
(assert (=> e3 (and v2 v3)))
(assert (=> e4 (and v3 v0)))
(assert (=> e5 (and v1 v3)))

(check-sat)
(get-model)

Ответы [ 2 ]

2 голосов
/ 01 февраля 2012

Идея состоит в том, чтобы позволить решателю SMT генерировать n чисел, скажем a1..an, а затем утверждать все следующее:

  • Все эти числа находятся в диапазоне от 0 до n-1
  • Все числа различны
  • Вершины a1 .. формируют цикл, то есть проверяют наличие ребер между a1-a2, a2-a3, ..., a (n-1) -an и an-a1

То есть вы просто описываете, что такое "гамильтонов цикл", и решатель SMT найдет его, если он существует.

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

Например, вот как вы можете решить эту проблему, используя Haskell и Z3: http://gist.github.com/1715097. Решение - это всего лишь 7 строк Haskell, и вы можете использовать его для запроса графика любого размера. Решение использует преимущества выразительной мощи Haskell и возможностей решения SMT в Z3, предоставляя чистый интерфейс.

0 голосов
/ 24 января 2017

Вы можете кодировать отношения ребер, используя логические переменные, например, используйте R-5-4 для обозначения if (5,4) в R.

Пусть E будет вашим входным отношением ребер.

Ограничить отношение R тем, что оно является подмножеством E, так что каждая вершина связана ровно с двумя ребрами в R.

Теперь ограничим отношение T транзитивным замыканием R.

Если T полностью связен (все T-n1-n2 верны), R - цикл Гамильтона, а (V, E) - граф Гамильтона.

...