SolveSudoku.py

# Annika Kouhia
# CS76 Artificial Intelligence
# October 2017
# SAT2 class holds the implementation of walkSat and gSat
# along with a lot of useful helper methods to store and access data efficiently

from random import *
from timeit import default_timer as timer

class SAT2:

    def __init__(self, cnfFile):
        self.cnfFile = cnfFile

        # a list of all of our constraints, each stored as a set in the form 111, -112, 113 etc.
        self.constraintList = []

        # our final answer
        self.results=[]

        #maps from an index to the absolute value of the corresponding sudoku value as in from 1 to 111, 2, to 112, etc.
        self.indToSud = {}

        #maps from the abosolute value of a sudoku value to the index as in from 111 to 1 and 112 to 2
        self.sudToInd = {}

        #maps from the absolute value of a sudoku value to a list of indeces of sets the value is referenced in (index in our constraintList of that set)
        self.sudToConstraintInd = {}

        # if a puzzle with preset values (constraints of size 1) keeps a set of the indeces these are stored at in our assignment
        self.setValuesIndeces = set()

    # builds indToSud and sudToInd
    # sudokuValue will always be positive since we strip off the negative sign
    def convertToVariable(self, sudokuValue):
        val = int(sudokuValue[2])
        col = int(sudokuValue[1])
        row = int(sudokuValue[0])
        index = 9 * (col - 1) + 81 * (row - 1) + val
        self.indToSud[index] = int(sudokuValue)
        self.sudToInd[int(sudokuValue)] = index


    # builds our random assignment of each spot in our list of assignments
    def randomlyFill(self, assignment):
        for i in range(1, len(self.indToSud)+1):
            #if this is a preset location in the game, set it correctly
            if i in self.setValuesIndeces:
                assignment.append(self.indToSud[i])
            # otherwise, ~randomize~
            else:
                decision = randint(0,1)
                if decision == 0:
                    assignment.append(-1*self.indToSud[i])
                else:
                    assignment.append(self.indToSud[i])


    # checks if our current assignment satisfies all constraints
    def accurateSolution(self, assignment):
        for constraintSet in self.constraintList:
            if not self.checkSatisfaction(assignment, constraintSet):
                return False
        return True


    # creates our list of constraints in the form of sets
    # also builds our dictionary of sudoku values to indeces of constraints they are involved with
    def createConstraintSets(self, file):
        file_object = open(file, "r")
        for line in file_object:
            line = line.strip()
            split_line = line.split(" ")
            currSet = set()
            # looks at each number on the line
            for numberstring in split_line:
                # converts to index value and stores the pair in twin dictionaries
                if numberstring[0]=="-":
                   self.convertToVariable(numberstring[1:])
                else:
                   self.convertToVariable(numberstring)

                #add the number to the line's set
                currSet.add(int(numberstring))

                # add the index of the set we're building to this number's value in our dictionary of variables
                # to constraints they are a part of
                if abs(int(numberstring)) not in self.sudToConstraintInd:
                    self.sudToConstraintInd[abs(int(numberstring))] = []
                ourList = self.sudToConstraintInd[abs(int(numberstring))]
                ourList.append(int(len(self.constraintList)))
                self.sudToConstraintInd[abs(int(numberstring))] = ourList

            # if the set is of size 1, add the index of this set to our set of preset values' indeces
            if len(currSet) == 1:
                for val in currSet:
                    self.setValuesIndeces.add(self.sudToInd[abs(val)])

            # add our full constraint set to our list of constraints
            self.constraintList.append(currSet)

        file_object.close()



    # writes out our solution to our solution file
    def write_solution(self, sol_filename):
        solution = open(sol_filename, 'w')
        for i in range (0, len(self.results)):
            if i<len(self.results)-1:
                if self.results[i]:
                    solution.write(str(self.results[i]) + "\n")
                else:
                    solution.write(str(self.results[i]) + "\n")
            else:
                if self.results[i]<0:
                    solution.write(str(self.results[i]))
                else:
                    solution.write(str(self.results[i]))
        solution.close()


    # randomly finds an unsatisfied constraint and returns its index
    def chooseUnsatisfiedConstraint(self, assignment):
        # uses the Random class' "choice" method
        randSet = choice(self.constraintList)

        # if satisfied, find another
        satisfied = self.checkSatisfaction(assignment, randSet)
        while satisfied:
            randSet = choice(self.constraintList)
            satisfied = self.checkSatisfaction(assignment, randSet)

        # return that unsatisifed set
        return randSet


    # see if the constraint is satisfied
    def checkSatisfaction(self, assignment, constraint):

        # if its a negative (length 2), one must be false
        # so if we find one whose value is equal to that of our constraint (constraint's value is negative)
        # return true
        if len(constraint) == 2 or len(constraint) == 1:
            for sudokuValue in constraint:
                if assignment[self.sudToInd[abs(sudokuValue)]] == sudokuValue:
                    return True
            return False
        # if its a long list, only one can be true
        # so if more than one is true (positive) return false
        else:
            found = 0
            for sudokuValue in constraint:
                if assignment[self.sudToInd[abs(sudokuValue)]] == sudokuValue:
                    found += 1
            if found != 1:
                return False
            return True


    # our main walkSat function as described in the write up
    def walkSat(self):
        #start stopwatch
        start = timer()
        # creates our list of constraints in the form of sets
        # also calls a method within which creates our dictionaries from sudvalues to indeces and from indeces back to sudvalues
        self.createConstraintSets(self.cnfFile)

        # creates and randomly fills our assignment
        assignments = [0]
        self.randomlyFill(assignments)

        # while assignment is incorrect
        i=0
        while not self.accurateSolution(assignments):
            #counting iteratinos
            i+=1

            #randomize and see if it makes the cut
            randomizer = randint(1,10)
            if randomizer<=7:
                #if made the cut off, choose a random unsatisfied set
                currSet = self.chooseUnsatisfiedConstraint(assignments)

                # find highest scoring value and flip it
                flipSudValue = self.highestScoringSud(assignments, currSet)
                flipSudValueIndex = self.sudToInd[abs(flipSudValue)]
                assignments[flipSudValueIndex] = -1*assignments[flipSudValueIndex]
            else:
                # otherwise, flip a random variable that isn't set (from the beginning)
                flipSudValueIndex = randint(1,len(assignments)-1)
                while flipSudValueIndex in self.setValuesIndeces:
                    flipSudValueIndex = randint(1,len(assignments)-1)
                assignments[flipSudValueIndex] = -1 * assignments[flipSudValueIndex]

        # set results equal to valid assignments for writing out
        self.results = assignments[1:]
        #stop our stopwatch
        end = timer()
        print("The following solution was brought to you by walkSAT after " + str(i) + " iterations and time: " + str(
            end - start) + " seconds")
        return True


    def gsat(self):
        # start Stopwatch
        start = timer()
        # creates our list of constraints in the form of sets
        # also calls a method within which creates our dictionaries from sudvalues to indeces and from indeces back to sudvalues
        self.createConstraintSets(self.cnfFile)

        # creates and randomly fills our assignment
        assignments = [0]
        self.randomlyFill(assignments)

        i = 0
        # while assignment is incorrect
        while not self.accurateSolution(assignments):
            #increment
            i += 1

            randomizer = randint(1,10)

            #if our randomizer meets the cut off
            if randomizer<=7:
                #find the highest scoring variable and flip
                flipSudValue = self.highestScoringSudGSAT(assignments)
                flipSudValueIndex = self.sudToInd[abs(flipSudValue)]
                assignments[flipSudValueIndex] = -1*assignments[flipSudValueIndex]
            else:
                # otherwise, flip a random variable that isn't set (from the beginning)
                flipSudValueIndex = randint(1,len(assignments)-1)
                while flipSudValueIndex in self.setValuesIndeces:
                    flipSudValueIndex = randint(1,len(assignments)-1)
                assignments[flipSudValueIndex] = -1 * assignments[flipSudValueIndex]

        # set results equal to valid assignments for writing out
        self.results = assignments[1:]
        #stop our stopwatch
        end = timer()
        print("The following solution was brought to you by GSAT after " + str(i) + " iterations and time: " + str(end - start) + " seconds" )
        return True



    # find the highest scoring variable--the one whose flip will create the most satisifed constraints
    def highestScoringSud(self, assignment, constraint):
        #base values that will change
        maxSudValue = 111
        maxSatisfied = -1

        #loop through values in specified constraint
        for sudValue in constraint:
            #if not a set value
            if self.sudToInd[abs(sudValue)] not in self.setValuesIndeces:
                index = self.sudToInd[abs(sudValue)]
                satisfied = 0

                #flip assignment for a second
                assignment[index] = -1 * assignment[index]

                # check each constraint it is involved with and see if the flipped assignment would
                # make that constraint satisfied, if so increment satisfied
                for involvedConstraintIndex in self.sudToConstraintInd[abs(sudValue)]:
                    if self.checkSatisfaction(assignment, self.constraintList[involvedConstraintIndex]):
                        satisfied += 1

                #flip assignment back now that testing is done
                assignment[index] = -1 * assignment[index]

                # update max values as necessary
                if satisfied>maxSatisfied:
                    maxSudValue = sudValue
                    maxSatisfied = satisfied

        #return!
        return maxSudValue



    # find the highest scoring variable--the one whose flip will create the most satisifed constraints
    # the only difference is that this goes through ALL variables instead of just the ones in a specified constraint
    def highestScoringSudGSAT(self, assignment):
        #base values that will change
        maxSudValue = 111
        maxSatisfied = -1

        # loop through all variables
        for sudValue in assignment:
            # if not 0 (fake news, not an assignment, just a placeholder) and not a set value
            if sudValue!=0 and self.sudToInd[abs(sudValue)] not in self.setValuesIndeces:
                index = self.sudToInd[abs(sudValue)]
                satisfied = 0

                #flip assignment and do testing
                assignment[index] = -1 * assignment[index]
                for constraint in self.constraintList:
                    if self.checkSatisfaction(assignment, constraint):
                        satisfied += 1

                #flip back!
                assignment[index] = -1 * assignment[index]


                # if more satisfaction, update appropriately
                if satisfied>maxSatisfied:
                    maxSudValue = sudValue
                    maxSatisfied = satisfied

        return maxSudValue