Optimised the demonstration, Added constraint judge.

backend/Example.txt

@@ -50,9 +50,9 @@ categories = [
 NUM_POSITIONS = len(categories[0][1])
 
 item_to_cat_and_index = {}
-for cat_idx, (_, item_list) in enumerate(categories):
+for cat_idx, (cat_str, item_list) in enumerate(categories):
     for item_idx, item_str in enumerate(item_list):
-        item_to_cat_and_index[item_str] = (cat_idx, item_idx)
+        item_to_cat_and_index[(cat_str, item_str)] = (cat_idx, item_idx)
 
 Vars = []
 for cat_idx, (cat_name, item_list) in enumerate(categories):
@@ -66,70 +66,70 @@ for cat_idx, (cat_name, item_list) in enumerate(categories):
         s.add(Vars[cat_idx][item_idx] >= 1, Vars[cat_idx][item_idx] <= NUM_POSITIONS)
     s.add(Distinct(Vars[cat_idx]))
 
-def pos(item_str):
-    (cat_idx, item_idx) = item_to_cat_and_index[item_str]
+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("wild pickings") == 4)
+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("cherry") > pos("green"))
+s.add(pos("Jam", "cherry") > pos("Shirt", "green"))
 
 # Isabella is selling Cherry jam.
-s.add(pos("Isabella") == pos("cherry"))
+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("backyard") < pos("pink"), pos("pink") < pos("watermelon")))
+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("14 oz") > pos("green"))
+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("14 oz") - pos("raspberry")) == 1)
+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("raspberry") == 1, pos("raspberry") == NUM_POSITIONS))
+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("Barbara") - pos("organic farm")) == 1)
+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("Nicole") < pos("Jane"), pos("Jane") < pos("Isabella")))
+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("fig") == pos("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("10 oz") == 1, pos("10 oz") == NUM_POSITIONS))
+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("raspberry") > pos("green"))
+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("12 oz") - pos("6 oz")) == 1)
+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("Isabella") - pos("black")) == 1)
+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("6 oz") - pos("local grocer")) == 1)
+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("6 oz") == 2)
+s.add(pos("Size", "6 oz") == 2)
 
 # Rachel's source of fruit is the Farmers' coop.
-s.add(pos("Rachel") == pos("farmers' coop"))
+s.add(pos("Name", "Rachel") == pos("Source", "farmers' coop"))
 
 # Barbara is next to Nicole.
-s.add(Abs(pos("Barbara") - pos("Nicole")) == 1)
+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("orange") == pos("backyard"))
+s.add(pos("Shirt", "orange") == pos("Source", "backyard"))
 
 # The producer with 12 oz jars is in the very first position.
-s.add(pos("12 oz") == 1)
+s.add(pos("Size", "12 oz") == 1)
 
 # Solve the puzzle
 if s.check() == sat:

backend/Sat_cnt.txt

@@ -0,0 +1,32 @@
+# 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))
+    print(f"sat:{cnt}")
+else:
+    print(f"error")

backend/app.py

@@ -10,13 +10,13 @@ example_path = os.path.join(BASE_DIR, "Example.txt")
 with open(example_path, "r", encoding="utf-8") as f:
     DEFAULT_SYS_CONTENT = f.read()
 
-# 只初始化一次
+# Only initialize once
 app = Flask(__name__, static_folder='static', static_url_path='')
 CORS(app)
 
 @app.route('/')
 def index():
-    # 返回静态文件夹下编译好的 index.html
+    # Return built static index.html
     return send_from_directory(app.static_folder, 'index.html')
 
 @app.route("/get_puzzle", methods=["GET"])

backend/solver.py

@@ -20,8 +20,8 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content):
     )
 
     messages = [
-        {"role": "user", "content": sys_content},  # 先把 sys_content 放进去
-        {"role": "user", "content": puzzle},       # 再放 puzzle
+        {"role": "user", "content": sys_content},
+        {"role": "user", "content": puzzle + f'\nCategories: {str(expected_solution["header"][1:])}\n'},
     ]
     attempts = 0
     current_solution = None
@@ -43,7 +43,7 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content):
             messages.append({"role": "user", "content": "Please write a complete Python code in your response. Try again."})
             continue
 
-        code_to_run = code_blocks[0].strip()
+        code_to_run = code_blocks[-1].strip()
         result = subprocess.run(
             [sys.executable, "-c", code_to_run],
             stdout=subprocess.PIPE,
@@ -53,6 +53,10 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content):
         output = result.stdout.strip()
         # print(output)
 
+        if result.stderr.strip():
+            messages.append({"role": "user", "content": f"Your code has errors: {result.stderr.strip()}. Please check your code and provide the complete code in the end."})
+            continue
+
         try:
             current_solution = json.loads(output)
         except json.JSONDecodeError:
@@ -66,10 +70,117 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content):
                 "solution": current_solution,
                 "attempts": attempts,
                 "generatedCode": code_to_run,
-                "modelResponse": content
+                "modelResponse": content,
+                "problematicConstraints": None
             }
         else:
-            messages.append({"role": "user", "content": "The solution does not match the expected answer. Please check your categories and constraints and provide the complete code again."})
+            messages.append({"role": "user", "content": "The solution does not match the expected answer. Please check your categories and step by step reason your constraints and provide the complete code in the end."})
+
+    if result.stderr.strip():
+        return {
+            "index": index,
+            "success": False,
+            "solution": current_solution,
+            "attempts": attempts,
+            "generatedCode": code_to_run,
+            "modelResponse": content,
+            "problematicConstraints": "Code error:\n" + result.stderr.strip()
+        }
+
+    # if 'rows' not in current_solution.keys():
+    #     return {
+    #         "index": index,
+    #         "success": False,
+    #         "solution": current_solution,
+    #         "attempts": attempts,
+    #         "generatedCode": code_to_run,
+    #         "modelResponse": content,
+    #         "problematicConstraints": str(current_solution)
+    #     }
+
+    code_by_line = code_to_run.split("\n")
+
+    fisrt_cons_line = None
+    last_cons_line = None
+    for i, line in enumerate(code_by_line):
+        if "s.add" in line and "pos" in line:
+            if not fisrt_cons_line:
+                fisrt_cons_line = i
+            last_cons_line = i
+    
+    experiment_code_line = code_by_line[:fisrt_cons_line]
+    categories = expected_solution['header']
+    for i, houses in enumerate(expected_solution['rows']):
+        for j in range(1, len(houses)):
+            experiment_code_line.append(f"s.add(pos(\"{categories[j]}\", \"{houses[j]}\") == {i+1})")
+    experiment_code_line.append("")
+    experiment_code_line.append("print(s.check())")
+
+    def satisfied(constraint):
+        experiment_code_line[-2] = constraint
+        experiment_code = "\n".join(experiment_code_line)
+        sat_checker = experiment_code.strip()
+        result = subprocess.run(
+            [sys.executable, "-c", sat_checker],
+            stdout=subprocess.PIPE,
+            stderr=subprocess.PIPE,
+            text=True
+        )
+        output = result.stdout.strip()
+        return output.lower()
+
+    if "error" in current_solution.keys():
+        if "Multiple" in current_solution['error']:
+            problematic_constraints = "Issue: Multiple solutions\n"
+        else:
+            problematic_constraints = "Issue: No solution\n"
+    else:
+        problematic_constraints = "Issue: Wrong answer\n"
+
+    cnt_cons = 0
+    problematic_constraints += "\nSatisfaction judge:\n"
+    for i, line in enumerate(code_by_line):
+        if "s.add" in line and "pos" in line:
+            constraint = line.strip()
+            cnt_cons += 1
+            if satisfied(constraint) == "unsat":
+                problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {constraint}. Not satisfied.\n"
+
+    with open("Sat_cnt.txt", "r") as f:
+        sat_cnt = f.read()
+    cnt_cons = 0
+    problematic_constraints += "\nMultiple solutions judge:\n"
+    code_by_line_experiment = code_to_run.split("\n")[:last_cons_line + 1]
+    code_by_line_experiment.append("\n")
+    def run_result():
+        experiment_code = "\n".join(code_by_line_experiment) + sat_cnt
+        sat_checker = experiment_code.strip()
+        result = subprocess.run(
+            [sys.executable, "-c", sat_checker],
+            stdout=subprocess.PIPE,
+            stderr=subprocess.PIPE,
+            text=True
+        )
+        return result.stdout.strip()
+    res = run_result()
+    # print("\n".join(code_by_line_experiment) + sat_cnt)
+    # print(res)
+    if not res or res == "error":
+        problematic_constraints += "Unable to judge."
+    else:
+        cur = int(res.split(':')[1])
+        for i, line in enumerate(code_by_line):
+            if "s.add" in line and "pos" in line:
+                cnt_cons += 1
+                code_by_line_experiment[i] = ""
+                res = run_result()
+                if not res or res == "error":
+                    problematic_constraints += "Unable to judge."
+                    break
+                now_cnt = int(res.split(':')[1])
+                if now_cnt == cur:
+                    problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {line}. A suspect redundency.\n"
+                code_by_line_experiment[i] = line
 
     return {
         "index": index,
@@ -77,5 +188,6 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content):
         "solution": current_solution,
         "attempts": attempts,
         "generatedCode": code_to_run,
-        "modelResponse": content
+        "modelResponse": content,
+        "problematicConstraints": problematic_constraints
     }

backend/static/asset-manifest.json

@@ -1,15 +1,15 @@
 {
   "files": {
     "main.css": "/static/css/main.e6c13ad2.css",
-    "main.js": "/static/js/main.f13a7657.js",
+    "main.js": "/static/js/main.120fc3ad.js",
     "static/js/453.8ab44547.chunk.js": "/static/js/453.8ab44547.chunk.js",
     "index.html": "/index.html",
     "main.e6c13ad2.css.map": "/static/css/main.e6c13ad2.css.map",
-    "main.f13a7657.js.map": "/static/js/main.f13a7657.js.map",
+    "main.120fc3ad.js.map": "/static/js/main.120fc3ad.js.map",
     "453.8ab44547.chunk.js.map": "/static/js/453.8ab44547.chunk.js.map"
   },
   "entrypoints": [
     "static/css/main.e6c13ad2.css",
-    "static/js/main.f13a7657.js"
+    "static/js/main.120fc3ad.js"
   ]
 }

backend/static/index.html

@@ -1 +1 @@
-<!doctype html><html lang="en"><head><meta charset="utf-8"/><link rel="icon" href="/favicon.ico"/><meta name="viewport" content="width=device-width,initial-scale=1"/><meta name="theme-color" content="#000000"/><meta name="description" content="Web site created using create-react-app"/><link rel="apple-touch-icon" href="/logo192.png"/><link rel="manifest" href="/manifest.json"/><title>React App</title><script defer="defer" src="/static/js/main.f13a7657.js"></script><link href="/static/css/main.e6c13ad2.css" rel="stylesheet"></head><body><noscript>You need to enable JavaScript to run this app.</noscript><div id="root"></div></body></html>
+<!doctype html><html lang="en"><head><meta charset="utf-8"/><link rel="icon" href="/favicon.ico"/><meta name="viewport" content="width=device-width,initial-scale=1"/><meta name="theme-color" content="#000000"/><meta name="description" content="Web site created using create-react-app"/><link rel="apple-touch-icon" href="/logo192.png"/><link rel="manifest" href="/manifest.json"/><title>React App</title><script defer="defer" src="/static/js/main.120fc3ad.js"></script><link href="/static/css/main.e6c13ad2.css" rel="stylesheet"></head><body><noscript>You need to enable JavaScript to run this app.</noscript><div id="root"></div></body></html>

frontend/src/App.js

@@ -2,23 +2,26 @@
 import React, { useState, useEffect } from 'react';
 
 function App() {
-  // 用于存储 puzzle index 及其 puzzle 数据
+  // For puzzle index and puzzle data
   const [puzzleIndex, setPuzzleIndex] = useState(0);
   const [puzzleText, setPuzzleText] = useState("");
   const [expectedSolution, setExpectedSolution] = useState(null);
 
-  // sysContent 如果用户不改，就用默认 Example.txt
+  // sysContent can be editted, default using Example.txt
   const [sysContent, setSysContent] = useState("");
 
-  // 交互结果
-  const [modelResponse, setModelResponse] = useState("");
+  // Interaction results
   const [generatedCode, setGeneratedCode] = useState("");
   const [executionSuccess, setExecutionSuccess] = useState(null);
   const [attempts, setAttempts] = useState(0);
+  const [isSolving, setIsSolving] = useState(false);
+  const [problematicConstraints, setProblematicConstraints] = useState("");
 
-  // 前端先获取默认 sysContent
+  const FLASK_BASE_URL = 'http://localhost:7860';
+
+  // Frontend fetch sysContent in default
   useEffect(() => {
-    fetch("/default_sys_content")
+    fetch(`${FLASK_BASE_URL}/default_sys_content`)
       .then(res => res.json())
       .then(data => {
         if(data.success) {
@@ -28,16 +31,16 @@ function App() {
       .catch(e => console.error(e));
   }, []);
 
-  // 当 puzzleIndex 改变时，自动获取对应 puzzle
+  // When puzzleIndex changing，auto get puzzle
   useEffect(() => {
-    fetch(`/get_puzzle?index=${puzzleIndex}`)
+    fetch(`${FLASK_BASE_URL}/get_puzzle?index=${puzzleIndex}`)
       .then(res => res.json())
       .then(data => {
         if(data.success) {
           setPuzzleText(data.puzzle);
           setExpectedSolution(data.expected_solution);
         } else {
-          console.error("获取 puzzle 失败", data.error);
+          console.error("Failed to fetch puzzle", data.error);
           setPuzzleText("");
           setExpectedSolution(null);
         }
@@ -47,17 +50,20 @@ function App() {
 
   const handleSolve = () => {
     if(!puzzleText || !expectedSolution) {
-      alert("puzzle 或 expectedSolution 不完整");
+      alert("puzzle or expectedSolution incomplete");
       return;
     }
     const payload = {
       index: puzzleIndex,
       puzzle: puzzleText,
       expected_solution: expectedSolution,
-      sys_content: sysContent
+      sys_content: sysContent,
+      problematic_constraints: problematicConstraints
     };
 
-    fetch("/solve", {
+    setIsSolving(true);
+
+    fetch(`${FLASK_BASE_URL}/solve`, {
       method: "POST",
       headers: { "Content-Type": "application/json" },
       body: JSON.stringify(payload)
@@ -65,16 +71,19 @@ function App() {
     .then(res => res.json())
     .then(data => {
       if(!data.success) {
-        alert("后端处理错误: " + data.error);
+        alert("Backend error: " + data.error);
         return;
       }
       const result = data.result;
-      setModelResponse(result.modelResponse || "");
       setGeneratedCode(result.generatedCode || "");
       setExecutionSuccess(result.success);
       setAttempts(result.attempts || 0);
+      setProblematicConstraints(result.problematicConstraints || "");
     })
-    .catch(e => console.error(e));
+    .catch(e => console.error(e))
+    .finally(() => {
+      setIsSolving(false);
+    });
   };
 
   return (
@@ -82,7 +91,7 @@ function App() {
       <h1>Zebra Puzzle Demo</h1>
 
       <div style={{ marginBottom: 20 }}>
-        <label>选择 puzzle index (0 - 999): </label>
+        <label>Choose puzzle index (0 - 999): </label>
         <input
           type="number"
           value={puzzleIndex}
@@ -101,7 +110,7 @@ function App() {
       </div>
 
       <div style={{ marginBottom: 20 }}>
-        <h3>sys_content (可编辑)</h3>
+        <h3>sys_content</h3>
         <textarea
           rows={10}
           cols={80}
@@ -111,17 +120,17 @@ function App() {
       </div>
 
       <div style={{ marginBottom: 20 }}>
-        <button onClick={handleSolve}>Solve Puzzle with LLM</button>
+        <button onClick={handleSolve} disabled={isSolving}>Solve Puzzle with LLM</button>
       </div>
 
       <div>
         <h2>Result</h2>
         <p>Success: {executionSuccess === null ? "N/A" : executionSuccess ? "✅" : "❌"}</p>
         <p>Attempts: {attempts}</p>
+        <h3>Problematic Constraints</h3>
+        <pre>{problematicConstraints}</pre>
         <h3>Generated Code</h3>
         <pre>{generatedCode}</pre>
-        <h3>Model Response</h3>
-        <pre>{modelResponse}</pre>
       </div>
     </div>
   );

test.py

@@ -0,0 +1,146 @@
+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 = [
+    ("Name", ["Bob", "Arnold", "Carol", "Alice", "Peter", "Eric"]),
+    ("Mother", ["Sarah", "Janelle", "Aniya", "Kailyn", "Holly", "Penny"]),
+    ("Children", ["Fred", "Samantha", "Bella", "Meredith", "Alice", "Timothy"]),
+    ("Vacation", ["city", "mountain", "camping", "beach", "cruise", "cultural"]),
+    ("BookGenre", ["romance", "mystery", "historical fiction", "science fiction", "biography", "fantasy"])
+]
+
+# 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
+# 1. The person who loves beach vacations is not in the second house.
+s.add(pos("Vacation", "beach") != 2)
+
+# 2. The person who loves fantasy books is somewhere to the left of Peter.
+s.add(pos("BookGenre", "fantasy") < pos("Name", "Peter"))
+
+# 3. The person whose mother's name is Sarah is the person who prefers city breaks.
+s.add(pos("Mother", "Sarah") == pos("Vacation", "city"))
+
+# 4. The person who enjoys camping trips is somewhere to the right of Peter.
+s.add(pos("Vacation", "camping") > pos("Name", "Peter"))
+
+# 5. The person who likes going on cruises is the person's child is named Meredith.
+s.add(pos("Vacation", "cruise") == pos("Children", "Meredith"))
+
+# 6. There is one house between the person who is the mother of Timothy and Eric.
+s.add(Abs(pos("Mother", "Timothy") - pos("Name", "Eric")) == 2)
+
+# 7. The person whose mother's name is Janelle is not in the second house.
+s.add(pos("Mother", "Janelle") != 2)
+
+# 8. The person's child is named Fred is somewhere to the left of Eric.
+s.add(pos("Children", "Fred") < pos("Name", "Eric"))
+
+# 9. The person who goes on cultural tours is in the fourth house.
+s.add(pos("Vacation", "cultural") == 4)
+
+# 10. The person whose mother's name is Janelle is not in the first house.
+s.add(pos("Mother", "Janelle") != 1)
+
+# 11. The person whose mother's name is Holly is somewhere to the right of the person who loves historical fiction books.
+s.add(pos("Mother", "Holly") > pos("BookGenre", "historical fiction"))
+
+# 12. The person's child is named Bella is somewhere to the left of Alice.
+s.add(pos("Children", "Bella") < pos("Name", "Alice"))
+
+# 13. Arnold is somewhere to the right of the person who loves fantasy books.
+s.add(pos("Name", "Arnold") > pos("BookGenre", "fantasy"))
+
+# 14. The person who loves mystery books is in the fourth house.
+s.add(pos("BookGenre", "mystery") == 4)
+
+# 15. The person's child is named Alice is the person who enjoys camping trips.
+s.add(pos("Children", "Alice") == pos("Vacation", "camping"))
+
+# 16. The person whose mother's name is Kailyn is the person who likes going on cruises.
+s.add(pos("Mother", "Kailyn") == pos("Vacation", "cruise"))
+
+# 17. There are two houses between the person who loves fantasy books and The person whose mother's name is Aniya.
+s.add(Abs(pos("BookGenre", "fantasy") - pos("Mother", "Aniya")) == 3)
+
+# 18. The person who loves fantasy books is Carol.
+s.add(pos("BookGenre", "fantasy") == pos("Name", "Carol"))
+
+# 19. The person who likes going on cruises is the person who loves biography books.
+s.add(pos("Vacation", "cruise") == pos("BookGenre", "biography"))
+
+# 20. The person who loves fantasy books is in the third house.
+s.add(pos("BookGenre", "fantasy") == 3)
+
+# 21. The person whose mother's name is Aniya is the person who loves romance books.
+s.add(pos("Mother", "Aniya") == pos("BookGenre", "romance"))
+
+# 22. The person whose mother's name is Janelle is not in the fourth house.
+s.add(pos("Mother", "Janelle") != 4)
+
+# 23. The person's child is named Fred is not in the fourth house.
+s.add(pos("Children", "Fred") != 4)
+
+# 24. The person who loves biography books is not in the second house.
+s.add(pos("BookGenre", "biography") != 2)
+
+# 25. There are two houses between The person whose mother's name is Holly and Eric.
+s.add(Abs(pos("Mother", "Holly") - pos("Name", "Eric")) == 3)
+
+# 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))
+    print(f"sat:{cnt}")
+else:
+    print(f"error")