Modelling a logic puzzle

Question

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)

alias · Accepted Answer · 2018-12-11T05:54:19.073

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.

Python

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.

Haskell

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.

For the second test, i.e. to prove the hypothesis, could you instead check if a conjunction of the premises and the negation of the last statement is unsatisfiable? That is `s.add(Exists([f1, f2, f3], And(validPick(f1, f2, f3), count(B, [f1, f2, f3]) == 0)))` — Dima Chubarov, Dec 12 '18 at 04:22
@DmitriChubarov That'd simply produce `unsat` for all values of `N` as it would contradict the very first axiom that there's a flower of every color. It'd be true of course, but it wouldn't really be meaningful and you can't derive any conclusion from that. — alias, Dec 12 '18 at 05:25
_I think there's an implicit assumption that flowers of all three colors are represented in the garden._ This is an astute observation! I forgot to mention this fact, which is of course crucial. I will edit the original question to reflect this. Thanks. — buggymcbugfix, Dec 13 '18 at 10:26

Modelling a logic puzzle

1 Answers1

Python

Haskell