mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Add example sent by Ganesh

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-31 14:37:54 -08:00
parent 6a6015e335
commit 4681281765
1 changed files with 88 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

88
examples/python/hamiltonian/hamiltonian.py Normal file
View file

@ -0,0 +1,88 @@
############################################
# Copyright (c) 2012 Ganesh Gopalakrishnan ganesh@cs.utah.edu
#
# Hamiltonian
#
# Author: Ganesh Gopalakrishnan ganesh@cs.utah.edu
############################################
from z3 import *
def gencon(gr):
"""
Input a graph as an adjacency list, e.g. {0:[1,2], 1:[2], 2:[1,0]}.
Produces solver to check if the given graph has
a Hamiltonian cycle. Query the solver using s.check() and if sat,
then s.model() spells out the cycle. Two example graphs from
http://en.wikipedia.org/wiki/Hamiltonian_path are tested.
=======================================================
Explanation:
Generate a list of Int vars. Constrain the first Int var ("Node 0") to be 0.
Pick a node i, and attempt to number all nodes reachable from i to have a
number one higher (mod L) than assigned to node i (use an Or constraint).
=======================================================
"""
L = len(gr)
cv = [Int('cv%s'%i) for i in range(L)]
s = Solver()
s.add(cv[0]==0)
for i in range(L):
s.add(Or([cv[j]==(cv[i]+1)%L for j in gr[i]]))
return s
def examples():
# Example Graphs: The Dodecahedral graph from http://en.wikipedia.org/wiki/Hamiltonian_path
grdodec = { 0: [1, 4, 5],
1: [0, 7, 2],
2: [1, 9, 3],
3: [2, 11, 4],
4: [3, 13, 0],
5: [0, 14, 6],
6: [5, 16, 7],
7: [6, 8, 1],
8: [7, 17, 9],
9: [8, 10, 2],
10: [9, 18, 11],
11: [10, 3, 12],
12: [11, 19, 13],
13: [12, 14, 4],
14: [13, 15, 5],
15: [14, 16, 19],
16: [6, 17, 15],
17: [16, 8, 18],
18: [10, 19, 17],
19: [18, 12, 15] }
import pprint
pp = pprint.PrettyPrinter(indent=4)
pp.pprint(grdodec)
sdodec=gencon(grdodec)
print(sdodec.check())
print(sdodec.model())
# =======================================================
# See http://en.wikipedia.org/wiki/Hamiltonian_path for the Herschel graph
# being the smallest possible polyhdral graph that does not have a Hamiltonian
# cycle.
#
grherschel = { 0: [1, 9, 10, 7],
1: [0, 8, 2],
2: [1, 9, 3],
3: [2, 8, 4],
4: [3, 9, 10, 5],
5: [4, 8, 6],
6: [5, 10, 7],
7: [6, 8, 0],
8: [1, 3, 5, 7],
9: [2, 0, 4],
10: [6, 4, 0] }
pp.pprint(grherschel)
sherschel=gencon(grherschel)
print(sherschel.check())
# =======================================================
if __name__ == "__main__":
examples()