backend/Example.txt

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.