1 z3-solver
 2 from z3 import *
 3 Group= [BitVec('solveL%d'%i,8) for i in range(0,2)]
 4 //Group=['solveL1','solveL2','solveL3'……]
 5 #a,b=Ints('a b')//Real()
 6 #''内的为求解出的解的名字，=前的为py代码里的名字，一般相同即可
 7 solve=Solver()
 8 solve.add()
 9 if solve.check()==sat:
10     print solve.model()
11 //
12 //多解的写法
13 while solve.check()==sat:
14     m=solve.model()
15     print m
16     solve.add(Or(T[0]!=m[T[0]],T[1]!=m[T[1]]))
17 //注意递归解题