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:

from z3 import *

politicians = [ Bool('x%s' % i) for i in range(100) ]
#True is an honest politicians#false is a crooked one
atleastonehonest = Or(politicians)

forall2atleastonecrooked = And([ Or(Not(i), Not(j)) for i in politicians for j in politicians if not i is j])

#sol, something = solve(forall2atleastonecrooked,atleastonehonest)
s = Solver()