Alloy compiler for Sudoku

diff --git a/sudoku-csolver/Sudoku.py b/sudoku-csolver/Sudoku.py
index 676425d24d51b78aef5e8df82478c04fb711c5ff..e633e77d08657f5e71e662026129dca8b91e3a81 100644 (file)
--- 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 ac1fef6359463ce7adc1cf1d78edc313df140231..129fe52f5ef49632b8734deef515e57134f2e2d4 100644 (file)
--- 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 aec861598dbe5e4a41b133615cf0f0e59b58454d..89d7682d0b4cd11a7df4d3c6c1332cfb5777e1c6 100755 (executable)
--- 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