mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fixed newline characters

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-10-24 23:52:40 +01:00
parent 6a496a1bfb
commit cee7dd3944
1 changed files with 88 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

176
examples/python/hamiltonian/hamiltonian.py
View file

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