Alloy Support for Killer Sudoku
authorHamed Gorjiara <hgorjiar@uci.edu>
Fri, 25 Jan 2019 20:15:40 +0000 (12:15 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Fri, 25 Jan 2019 20:15:40 +0000 (12:15 -0800)
killerSudoku/argprocessor.py
killerSudoku/csolversudoku.py
killerSudoku/killerSolver.py
killerSudoku/run.sh

index c748e5588566c543b7191ebba093a2d9c8831e71..1c505ee9f54ebea58021341680808b1ee914ed22 100644 (file)
@@ -9,16 +9,22 @@ class KSudokuArgParser:
         self.parser.add_argument('--problem', '-p', metavar='problem.killer', type=str, nargs=1,help='Files generated by KillerSudokuGenerator.py')
         self.parser.add_argument('--csolver', '-cs', action='store_true',help='Encode with the constraint solver (default: uses the original hand crafted encoding)')
         self.parser.add_argument('--dump', '-dp', action='store_true',help='Dumps the problem into a file')
+        self.parser.add_argument('--alloy', '-al', action='store_true',help='Solve problem via Alloy')
         self.args = self.parser.parse_args()
         
     def getProblemName(self):
         return self.args.problem
-    
-    def useCSolverEncoding(self):
-        return self.args.csolver
 
-    def shouldSerialize(self):
-        return self.args.dump
+    def getCSolverOption(self):
+        if self.args.alloy:
+            return 3
+        if self.args.dump:
+            return 2
+        if self.args.csolver:
+            return 1
+        else:
+            return 0
+
 # def main():
 #     print sys.argv
 #     argParser = KSudokuArgParser()
index ed20da85d7b1bb2a5abf862c89351d07402abc8a..3a17e98f7a98e3fabc4ac3d7bb5374c012edda11 100644 (file)
@@ -4,9 +4,14 @@ import numpy as np
 import sys
 from itertools import combinations, ifilter, chain
 
-def solveProblem(N, killerRules, serialize = False):
+class Solver:
+       CSOLVER=1
+       SERIALISE=2
+       ALLOY=3
+
+def solveProblem(N, killerRules, solverOption):
        
-       return generateKillerSudokuConstraints(N, killerRules, serialize)
+       return generateKillerSudokuConstraints(N, killerRules, solverOption)
 
 def getDomain(allPossible):
        assert len(allPossible) > 0
@@ -34,7 +39,7 @@ def generateEqualityConstraint(csolverlb, solver, e1, e2):
         b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(2))
         return b
 
-def generateKillerSudokuConstraints(N, killerRules, serialize):
+def generateKillerSudokuConstraints(N, killerRules, solverOption):
        csolverlb = ps.loadCSolver()
        solver = csolverlb.createCCSolver()
        s1 = [ i for i in range(1, N+1)]
@@ -227,8 +232,10 @@ def generateKillerSudokuConstraints(N, killerRules, serialize):
                        valid([problem[i + k % root, j + k // root] for k in range(N)])
        
        #Serializing the problem before solving it ....
-       if serialize:
+       if solverOption == Solver.SERIALISE:
                csolverlb.serialize(solver)
+       if solverOption == Solver.ALLOY:
+               csolverlb.setAlloyEncoder(solver)
        if csolverlb.solve(solver) != 1:
                return None
        result = [[0 for i in range(N)] for i in range(N)]
index 803ef2f182c0169d76a0216600d9fc1a33d3657e..779e4d1d7300a236050eb5357512461a6c9aae75 100644 (file)
@@ -323,8 +323,8 @@ def solveKillerSudoku(killerRules):
     global argparser
     result_matrix = None
     
-    if argparser.useCSolverEncoding() or argparser.shouldSerialize():
-        result_matrix = cs.solveProblem(N, killerRules, argparser.shouldSerialize())
+    if argparser.getCSolverOption() > 0:
+        result_matrix = cs.solveProblem(N, killerRules, argparser.getCSolverOption())
     else:
         result_matrix = solveOriginalEncoding(killerRules)
     
index aec861598dbe5e4a41b133615cf0f0e59b58454d..7e18441782f1154f86eae12ca2a2b4e69855bfe8 100755 (executable)
@@ -1,5 +1,6 @@
 #!/bin/bash
 
+export CLASSPATH=./csolver/original.jar:.:$CLASSPATH
 export PYTHONPATH=./csolver
 export LD_LIBRARY_PATH=./csolver
 # For Mac OSX