-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathrun_experiment.py
67 lines (53 loc) · 2.53 KB
/
run_experiment.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
import os
import argparse
import json
from solver.solver_class import SatSolver
from solver.utils import parse_dimacs
def run_experiment(puzzles_path: str, strategies: dict, results_folder: str) -> None:
"""
Run the experimental loop for specified heuristics on Sudoku puzzles.
Args:
puzzles_path (str): Path to the folder containing Sudoku puzzles in DIMACS format.
strategies (dict): Dictionary of strategy names and their corresponding numbers.
results_folder (str): Path to the folder to save results.
"""
os.makedirs(results_folder, exist_ok=True) # Ensure results folder exists
# Track file progress for sanity checks
all_files = [f for f in os.listdir(puzzles_path) if f.endswith(".cnf")]
total_files = len(all_files)
for strategy_name, strategy_number in strategies.items():
output_file = os.path.join(results_folder, f"{strategy_name}.json")
results = []
print(f"Running experiments for {strategy_name} heuristic...")
files_left = total_files
for puzzle_file in os.listdir(puzzles_path):
puzzle_path = os.path.join(puzzles_path, puzzle_file)
print(f"Solving {puzzle_file} with {strategy_name} heuristic")
print(f"Files left {files_left}")
files_left -= 1
if not puzzle_path.endswith(".cnf"):
continue # Skip non-CNF files
clauses = parse_dimacs(puzzle_path)
solver = SatSolver(strategy=strategy_number)
assignment, metrics = solver.solve(clauses)
results.append({
"puzzle": puzzle_file,
"metrics": metrics,
"satisfiable": bool(assignment)
})
# Save to JSON
with open(output_file, "w") as f:
json.dump(results, f, indent=4)
print(f"Results for {strategy_name} saved to {output_file}")
if __name__ == "__main__":
parser = argparse.ArgumentParser(description="Run experiments on Sudoku puzzles using different SAT solver heuristics.")
parser.add_argument("--puzzles_path", required=True, help="Path to the folder containing Sudoku puzzles in DIMACS format.")
args = parser.parse_args()
strategies = {
"JW_2_Sided": 3, # Literal-oriented
"DLIS": 5, # Literal-oriented
"MOMS": 4, # Clause-oriented
"BOHMS": 6 # Clause-oriented
}
results_folder = os.path.join(os.path.dirname(__file__), "results")
run_experiment(args.puzzles_path, strategies, results_folder)