diff --git a/backend/Example.txt b/backend/Example.txt index b7fd65fdc91f8b8bf9c2ec52927ece0aacc4dc39..4bec444e170af61fb738bfcc812d5863f1a4d7d7 100644 --- a/backend/Example.txt +++ b/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: diff --git a/backend/Sat_cnt.txt b/backend/Sat_cnt.txt new file mode 100644 index 0000000000000000000000000000000000000000..28e3a3a819526998b4dd6d3635004fd88f6f9a66 --- /dev/null +++ b/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") \ No newline at end of file diff --git a/backend/__pycache__/solver.cpython-313.pyc b/backend/__pycache__/solver.cpython-313.pyc index 7bb020a1d458635367dd11a1e3b987480e4eec24..d0867f48cde4350326b8325eae5be7841c3253d5 100644 Binary files a/backend/__pycache__/solver.cpython-313.pyc and b/backend/__pycache__/solver.cpython-313.pyc differ diff --git a/backend/app.py b/backend/app.py index 2bc0483bea371470a552d9528c080c6821a6bf82..081320004fe9a064e4803a997e608e80dcf98452 100644 --- a/backend/app.py +++ b/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"]) diff --git a/backend/solver.py b/backend/solver.py index b85944ecc41fde38da94b8dd9323b992bae5dbbe..bcab64ce045ed2b3a7b83bc2f1e9d11a45c68b04 100644 --- a/backend/solver.py +++ b/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 } diff --git a/backend/static/asset-manifest.json b/backend/static/asset-manifest.json index 3341cd3b1c87992f3d3218a58754415e34cd8421..7db01d0a8c6c7c5f1c9e3a3b94c17c7b27254f11 100644 --- a/backend/static/asset-manifest.json +++ b/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" ] } \ No newline at end of file diff --git a/backend/static/index.html b/backend/static/index.html index 08291dc04d7569dcc6da47b65c76e49c4c7af17e..cd4b619234bc533f822b90f686fe2949c3782a6b 100644 --- a/backend/static/index.html +++ b/backend/static/index.html @@ -1 +1 @@ -