From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Tue, 22 Jan 2019 08:12:37 +0000 (-0800)
Subject: Alloy compiler for Sudoku
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=dc7a6d88d925c769460697015fe01a08d59a9fd9;p=Benchmarks_CSolver.git

Alloy compiler for Sudoku
---

diff --git a/sudoku-csolver/Sudoku.py b/sudoku-csolver/Sudoku.py
index 676425d2..e633e77d 100644
--- a/sudoku-csolver/Sudoku.py
+++ b/sudoku-csolver/Sudoku.py
@@ -1,4 +1,4 @@
-import glucose
+import pycosat
 import sys, getopt 
 import time
 import numpy as np
@@ -30,12 +30,15 @@ def main(argv):
 			print opts, args
 			if "--csolver" in args:
 				print "Solving the problem using csolver ..."
-				read_problem_from_file(args[indx], True)
+				read_problem_from_file(args[indx], 1)
 			elif "--dump" in args:
 				print "Solving the problem using csolver ..."
-				read_problem_from_file(args[indx], True, True)
+				read_problem_from_file(args[indx], 2)
+			elif "--alloy" in args:
+				print "Solving the problem using alloy ..."
+				read_problem_from_file(args[indx], 3)
 			else:
-				read_problem_from_file(args[indx])
+				read_problem_from_file(args[indx], 0)
 		elif opt in ( "--gen"):
 			N, K = extractProblemSpecs(args)
 			if "--csolver" in args:
@@ -54,7 +57,7 @@ def help():
 	print('Sudoku.py -h [or] --hard')
 	print('Sudoku.py -v [or] --evil')
 	print('Sudoku.py -b [or] --blank')
-	print('Sudoku.py --file file.problem [--csolver/--dump]')
+	print('Sudoku.py --file file.problem [--csolver/--dump/--alloy]')
 	print('Sudoku.py --gen 9 20 [--csolver/--dump]')
 	print('All problems generated by websudoku.com')
 	sys.exit()
@@ -126,18 +129,18 @@ def generate_problem(N, K):
 	pprint(problem)
 	np.savetxt('problems/'+str(N) + 'x' + str(N) + '-' + str(K) + '.problem',problem)
 
-def read_problem_from_file(filename, useCsolver=False, serialize=False):
+def read_problem_from_file(filename, solverID):
 	problem = np.loadtxt(filename)
 	global N
 	N=int(re.findall('\d+', filename)[0])
 	problem = problem.astype(int)
-	solve_problem(problem, useCsolver, serialize)
+	solve_problem(problem, solverID)
 
-def solve_problem(problemset, useCsolver, serialize):
+def solve_problem(problemset, solverID):
 	print('Problem:') 
 	pprint(problemset)
-	if useCsolver:
-		problemset=cs.solveProblem(N, problemset, serialize)
+	if solverID != 0:
+		problemset=cs.solveProblem(N, problemset, solverID)
 		np.savetxt('solved/'+str(N) + 'x' + str(N) + '.problem',problemset)
 	else: 
 		solve(problemset) 
@@ -202,7 +205,7 @@ def solve(grid):
 # 		print c
 	# solve the SAT problem
 	start = time.time()
-	sol = set(glucose.solve(clauses, N**3))
+	sol = set(pycosat.solve(clauses, N**3))
 	end = time.time()
 	print("SUDOKU SAT SOLVING TIME: "+str(end - start))
     
diff --git a/sudoku-csolver/csolversudoku.py b/sudoku-csolver/csolversudoku.py
index ac1fef63..129fe52f 100644
--- a/sudoku-csolver/csolversudoku.py
+++ b/sudoku-csolver/csolversudoku.py
@@ -3,11 +3,16 @@ from ctypes import *
 import numpy as np
 import sys
 
+class Solver:
+	CSOLVER=1
+	SERIALISE=2
+	ALLOY=3
+
 def generateProblem(N):
 	return generateSudokuConstraints(N)	
 
-def solveProblem(N, problem, serialize):
-	return generateSudokuConstraints(N, problem, serialize)
+def solveProblem(N, problem, solverID):
+	return generateSudokuConstraints(N, problem, solverID)
 
 def replaceWithElemConstOptimization(elemConsts, problem, sudoku):
 	for i,row in enumerate(sudoku):
@@ -53,7 +58,7 @@ def extractItemInSetOptimization(csolverlb, solver, sudoku, N):
 	
 	return np.array([[csolverlb.getElementVar(solver,sets[i][j]) for j in range(N)] for i in range(N)])
 
-def generateSudokuConstraints(N, sudoku = None, serialize=False):
+def generateSudokuConstraints(N, sudoku = None, solverID  = -1):
 	csolverlb = ps.loadCSolver()
 	solver = csolverlb.createCCSolver()
 	s1 = [ i for i in range(1, N+1)]
@@ -122,8 +127,10 @@ def generateSudokuConstraints(N, sudoku = None, serialize=False):
 
 #	csolverlb.printConstraints(solver);	
 	#Serializing the problem before solving it ....
-	if serialize:
+	if solverID == Solver.SERIALISE:
 		csolverlb.serialize(solver)
+	if solverID == Solver.ALLOY:
+		csolverlb.setAlloyEncode(solver)
 	if csolverlb.solve(solver) != 1:
 		print "Problem is unsolvable!"
                 sys.exit(1)
diff --git a/sudoku-csolver/run.sh b/sudoku-csolver/run.sh
index aec86159..89d7682d 100755
--- a/sudoku-csolver/run.sh
+++ b/sudoku-csolver/run.sh
@@ -1,6 +1,7 @@
 #!/bin/bash
 
 export PYTHONPATH=./csolver
+export CLASSPATH=./csolver/original.jar:.:$CLASSPATH
 export LD_LIBRARY_PATH=./csolver
 # For Mac OSX
 export DYLD_LIBRARY_PATH=./csolver