Skip to content

Instantly share code, notes, and snippets.

@vsaraph
Created April 5, 2021 21:45
Show Gist options
  • Save vsaraph/9f06ae77d7057f43bfbad319c79e9984 to your computer and use it in GitHub Desktop.
Save vsaraph/9f06ae77d7057f43bfbad319c79e9984 to your computer and use it in GitHub Desktop.
Failed attempt at getting Z3 to spit out the symmetric group of degree 3
from z3 import *
# create sort
group = DeclareSort('G')
# create function symbols
iden = Function('e', group)
mult = Function('m', group, group, group)
inv = Function('i', group, group)
# declare the group axioms
x, y, z = Consts('x y z', group)
group_axioms = [ ForAll([x, y, z], mult(x, mult(y, z)) == mult(mult(x, y), z)),
ForAll(x, mult(x, iden()) == x),
ForAll(x, mult(iden(), x) == x),
ForAll(x, mult(x, inv(x)) == iden()),
ForAll(x, mult(inv(x), x) == iden())]
# add non-commutativity as an "axiom", to try to force z3 to produce a non-commutative group like S_3
non_comm = [ Exists([x, y], mult(x, y) != mult(y, x)) ]
s = Solver()
s.add(group_axioms + non_comm)
# run the checker, hopefully finding an instance?
print(s)
print(s.check())
print(s.model()[group])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment