Reputation: 321
I am trying to model a logic puzzle from To Mock a Mockingbird. I am struggling to translate it into SMT-LIB. The puzzle goes something like this:
There is a garden in which all flowers are either red, yellow or blue, and all colours are represented. For any three flowers you pick, at least one will be red and one will be yellow. Is the third flower always going to be blue?
I tried modelling the garden as an Array Int Flower
, but that doesn't work, I believe because the domain of the array is fixed to range over all the integers. Z3 helpfully tells me that this is unsatisfiable, CVC4 just returns unknown straight away.
The only solution to the puzzle is a garden with exactly one flower of each colour, but how do I get the solver to tell me this?
This is my failed attempt:
(declare-datatypes () ((Flower R Y B)))
(declare-const garden (Array Int Flower))
(assert (forall ((a Int) (b Int) (c Int))
(and (or (= (select garden a) R)
(= (select garden b) R)
(= (select garden c) R))
(or (= (select garden a) Y)
(= (select garden b) Y)
(= (select garden c) Y)))))
(check-sat)
Upvotes: 2
Views: 219
Reputation: 30418
I think there's an implicit assumption that flowers of all three colors are represented in the garden. With that in mind, here's how I'd go about coding it using both Python and Haskell interfaces to Z3; because it's just easier to code in those languages than directly in SMTLib.
from z3 import *
# Color enumeration
Color, (R, Y, B) = EnumSort('Color', ('R', 'Y', 'B'))
# An uninterpreted function for color assignment
col = Function('col', IntSort(), Color)
# Number of flowers
N = Int('N')
# Helper function to specify distinct valid choices:
def validPick (i1, i2, i3):
return And( Distinct(i1, i2, i3)
, 1 <= i1, 1 <= i2, 1 <= i3
, i1 <= N, i2 <= N, i3 <= N
)
# Helper function to count a given color
def count(pickedColor, flowers):
return Sum([If(col(f) == pickedColor, 1, 0) for f in flowers])
# Get a solver and variables for our assertions:
s = Solver()
f1, f2, f3 = Ints('f1 f2 f3')
# There's at least one flower of each color
s.add(Exists([f1, f2, f3], And(validPick(f1, f2, f3), col(f1) == R, col(f2) == Y, col(f3) == B)))
# You pick three, and at least one of them is red
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(R, [f1, f2, f3]) >= 1)))
# You pick three, and at least one of them is yellow
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(Y, [f1, f2, f3]) >= 1)))
# For every three flowers you pick, one of them has to be blue
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(B, [f1, f2, f3]) == 1)))
# Find a satisfying value of N
print s.check()
print s.model()[N]
# See if there's any other value by outlawing the choice
nVal = s.model()[N]
s.add(N != nVal)
print s.check()
When run, this prints:
sat
3
unsat
The way to read this output is that the given conditions are indeed satisfiable when N=3
; as you were seeking to find out. Furthermore, if you also assert that N
is not 3
, then there's no satisfying model, i.e., the choice of 3
is forced by the conditions given. I believe this is what you wanted to establish.
I hope the code is clear, but feel free to ask for clarifications. If you do need this in SMT-Lib, you can always insert:
print s.sexpr()
before the calls to s.check()
and you can see the generated SMTLib.
It's also possible to code the same in Haskell/SBV. See this gist for almost a literal coding of the same: https://gist.github.com/LeventErkok/66594d8e94dc0ab2ebffffe4fdabccc9 Note that the Haskell solution can take advantage of SBV's allSat
construct (which returns all satisfying assumptions), and more simply show that N=3
is the only solution.
Upvotes: 3