| This is an example of representing a Zebra Puzzle using a Z3-based Python code: |
|
|
| There are 5 Producers in this puzzle. |
|
|
| Categories and possible items: |
| - Shirt: black, green, orange, pink, red |
| - Name: Barbara, Isabella, Jane, Nicole, Rachel |
| - Jam: apricot, cherry, fig, raspberry, watermelon |
| - Size: 10 oz, 12 oz, 14 oz, 20 oz, 6 oz |
| - Source: backyard, farmers' coop, local grocer, organic farm, wild pickings |
|
|
| Clues: |
| - The producer whose jam comes from Wild pickings is in the fourth position. |
| - The producer selling Cherry jam is somewhere to the right of the one wearing a Green shirt. |
| - Isabella is selling Cherry jam. |
| - The producer wearing a Pink shirt is somewhere between the producer whose jam source is the Backyard and the one selling Watermelon jam, in that order. |
| - The producer selling 14 oz jars is somewhere to the right of the one wearing a Green shirt. |
| - The producer with 14 oz jars is next to the one selling Raspberry jam. |
| - The Raspberry jam producer is positioned at one of the ends. |
| - Barbara is next to the producer whose jam source is the Organic farm. |
| - Jane is located somewhere between Nicole and Isabella, in that order. |
| - The producer of Fig jam sources the fruit from an Organic farm. |
| - The producer with 10 oz jars is at one of the ends. |
| - The Raspberry jam producer is somewhere to the right of the one wearing a Green shirt. |
| - The producer with 12 oz jars is next to the one who has 6 oz jars. |
| - Isabella is next to the producer wearing a Black shirt. |
| - The producer with 6 oz jars is next to the one whose source is the Local grocer. |
| - The producer with 6 oz jars is in the second position. |
| - Rachel's source of fruit is the Farmers' coop. |
| - Barbara is next to Nicole. |
| - The producer wearing an Orange shirt gets her fruit from the Backyard. |
| - The producer with 12 oz jars is in the very first position. |
|
|
| ```python |
| from z3 import * |
| import json |
| import sys |
|
|
| # Define all categories in a single list of tuples: |
| # (House is implicit; each row's first column will be the house number.) |
| categories = [ |
| ("Shirt", ["black", "green", "orange", "pink", "red"]), |
| ("Name", ["Barbara", "Isabella", "Jane", "Nicole", "Rachel"]), |
| ("Jam", ["apricot", "cherry", "fig", "raspberry", "watermelon"]), |
| ("Size", ["10 oz", "12 oz", "14 oz", "20 oz", "6 oz"]), |
| ("Source", ["backyard", "farmers' coop", "local grocer", "organic farm", "wild pickings"]) |
| ] |
|
|
| # No need to change here, automatically processing |
| NUM_POSITIONS = len(categories[0][1]) |
|
|
| item_to_cat_and_index = {} |
| for cat_idx, (cat_str, item_list) in enumerate(categories): |
| for item_idx, item_str in enumerate(item_list): |
| item_to_cat_and_index[(cat_str, item_str)] = (cat_idx, item_idx) |
|
|
| Vars = [] |
| for cat_idx, (cat_name, item_list) in enumerate(categories): |
| var = IntVector(cat_name, len(item_list)) |
| Vars.append(var) |
|
|
| s = Solver() |
|
|
| for cat_idx, (cat_name, item_list) in enumerate(categories): |
| for item_idx, item_str in enumerate(item_list): |
| s.add(Vars[cat_idx][item_idx] >= 1, Vars[cat_idx][item_idx] <= NUM_POSITIONS) |
| s.add(Distinct(Vars[cat_idx])) |
|
|
| def pos(cat_str, item_str): |
| (cat_idx, item_idx) = item_to_cat_and_index[(cat_str, item_str)] |
| return Vars[cat_idx][item_idx] |
|
|
| # All clues here |
| # The producer whose jam comes from Wild pickings is in the fourth position. |
| s.add(pos("Source", "wild pickings") == 4) |
|
|
| # The producer selling Cherry jam is somewhere to the right of the one wearing a Green shirt. |
| s.add(pos("Jam", "cherry") > pos("Shirt", "green")) |
|
|
| # Isabella is selling Cherry jam. |
| s.add(pos("Name", "Isabella") == pos("Jam", "cherry")) |
|
|
| # The producer wearing a Pink shirt is somewhere between the producer whose jam source is the Backyard and the one selling Watermelon jam, in that order. |
| s.add(And(pos("Source", "backyard") < pos("Shirt", "pink"), pos("Shirt", "pink") < pos("Jam", "watermelon"))) |
|
|
| # The producer selling 14 oz jars is somewhere to the right of the one wearing a Green shirt. |
| s.add(pos("Size", "14 oz") > pos("Shirt", "green")) |
|
|
| # The producer with 14 oz jars is next to the one selling Raspberry jam. |
| s.add(Abs(pos("Size", "14 oz") - pos("Jam", "raspberry")) == 1) |
|
|
| # The Raspberry jam producer is positioned at one of the ends. |
| s.add(Or(pos("Jam", "raspberry") == 1, pos("Jam", "raspberry") == NUM_POSITIONS)) |
|
|
| # Barbara is next to the producer whose jam source is the Organic farm. |
| s.add(Abs(pos("Name", "Barbara") - pos("Source", "organic farm")) == 1) |
|
|
| # Jane is located somewhere between Nicole and Isabella, in that order. |
| s.add(And(pos("Name", "Nicole") < pos("Name", "Jane"), pos("Name", "Jane") < pos("Name", "Isabella"))) |
|
|
| # The producer of Fig jam sources the fruit from an Organic farm. |
| s.add(pos("Jam", "fig") == pos("Source", "organic farm")) |
|
|
| # The producer with 10 oz jars is at one of the ends. |
| s.add(Or(pos("Size", "10 oz") == 1, pos("Size", "10 oz") == NUM_POSITIONS)) |
|
|
| # The Raspberry jam producer is somewhere to the right of the one wearing a Green shirt. |
| s.add(pos("Jam", "raspberry") > pos("Shirt", "green")) |
|
|
| # The producer with 12 oz jars is next to the one who has 6 oz jars. |
| s.add(Abs(pos("Size", "12 oz") - pos("Size", "6 oz")) == 1) |
|
|
| # Isabella is next to the producer wearing a Black shirt. |
| s.add(Abs(pos("Name", "Isabella") - pos("Shirt", "black")) == 1) |
|
|
| # The producer with 6 oz jars is next to the one whose source is the Local grocer. |
| s.add(Abs(pos("Size", "6 oz") - pos("Source", "local grocer")) == 1) |
|
|
| # The producer with 6 oz jars is in the second position. |
| s.add(pos("Size", "6 oz") == 2) |
|
|
| # Rachel's source of fruit is the Farmers' coop. |
| s.add(pos("Name", "Rachel") == pos("Source", "farmers' coop")) |
|
|
| # Barbara is next to Nicole. |
| s.add(Abs(pos("Name", "Barbara") - pos("Name", "Nicole")) == 1) |
|
|
| # The producer wearing an Orange shirt gets her fruit from the Backyard. |
| s.add(pos("Shirt", "orange") == pos("Source", "backyard")) |
|
|
| # The producer with 12 oz jars is in the very first position. |
| s.add(pos("Size", "12 oz") == 1) |
|
|
| # Solve the puzzle |
| if s.check() == sat: |
| m = s.model() |
| rows = [] |
| header = ["House"] + [cat_name for cat_name, _ in categories] |
| for position in range(1, NUM_POSITIONS + 1): |
| row = [str(position)] |
| for cat_idx, (cat_name, item_list) in enumerate(categories): |
| for item_idx, item_str in enumerate(item_list): |
| if m.evaluate(Vars[cat_idx][item_idx]).as_long() == position: |
| row.append(item_str) |
| break |
| rows.append(row) |
| result_dict = {"header": header, "rows": rows} |
|
|
| cnt = 1 |
| block = [] |
| for cat_idx, (cat_name, item_list) in enumerate(categories): |
| for i in range(NUM_POSITIONS): |
| block.append(Vars[cat_idx][i] != m[Vars[cat_idx][i]]) |
| s.add(Or(block)) |
| while s.check() == sat: |
| m = s.model() |
| cnt += 1 |
| block = [] |
| for cat_idx, (cat_name, item_list) in enumerate(categories): |
| for i in range(NUM_POSITIONS): |
| block.append(Vars[cat_idx][i] != m[Vars[cat_idx][i]]) |
| s.add(Or(block)) |
|
|
| if cnt == 1: |
| # Output the solution as a JSON string. |
| print(json.dumps(result_dict)) |
| else: |
| print(json.dumps({"error": "Multiple solutions found."})) |
| else: |
| print(json.dumps({"error": "No solution found."})) |
| sys.stdout.flush() # Force immediate output |
| ``` |
|
|
| Based on this example, write a similar Z3-based Python code by changing only categories and constraints to represent the puzzle given below. |
