Using Z3 to solve a simple logic puzzle

I was checking out Smullyan’s Lady of the Tiger. It starts with some very simple logic puzzles. Let’s make Z3 do one for us!

There are 100 politicians

at least one is honest

for any two at least one is crooked

How many honest politicians are there?

And here is one way of encoding this into z3:

Z3 is kind of a pain in that it won’t immediately cast to bools when I want them. A mistake I made at first was missing that “not i is j” in the list comprehension. Also an unfortunate feature is that this does not make it clear that there is a unique answer, due to permutations of the variables. But if we just asked for the number of honest, it’s not clear to me how to encode the forall2 constraint. Very curiously, z3 picks ‘x18’ to be the one honest man. I wonder why?

Leave a Reply

Your email address will not be published. Required fields are marked *