diff --git a/ChessBoard.py b/ChessBoard.py new file mode 100644 index 0000000000000000000000000000000000000000..f461d2b553fd0bfe54f02c569be5d61de6ba363f --- /dev/null +++ b/ChessBoard.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- +""" +Created on Tue Feb 2 09:36:24 2021 + +@author: lukepatton +""" +import math +from pysat.solvers import Glucose3 + +class ChessBoardRepresentation: + # The initialization sets up the chess board and solves it using Glucose3 + # input: n, the order of the NS1D0 sequence (int) + # result: the chess board is setup, NS1D0 contains the ns1d0 sequence + def __init__(self, n): + self.size = n + self.vars = [i for i in range(1, (n*n) + 1)] + self.clauses = [] + self.ruleOne() + self.ruleTwo() + self.ruleThreeA() + self.ruleThreeB() + self.ruleFour() + self.solve() + self.ns1d0 = self.getNS1D0FromSolution() + + # Gets a row from the chessboard + # input: row, the row number desired (int) + # output: all the variables in that row (list of ints) + def getRow(self, row): + row = row % self.size + firstVar = (self.size * row) + 1 + lastVar = (self.size * (row + 1)) + return [i for i in range(firstVar, lastVar + 1)] + + # Gets a column from the chessboard + # input: column, the column number desired (int) + # output: all the variables in that column (list of ints) + def getColumn(self, col): + col = col % self.size + return [(i*self.size) + (col + 1) for i in range(self.size)] + + # Gets a diagonal from the chessboard + # input: diag, the diagonal number desired (int) + # output: all the variables in that diagonal (list of ints) + def getDiagonal(self, diag): + diag = diag % self.size + answer = [] + for i in range(self.size): + j = (diag + i) % self.size + answer.append((i*self.size) + j + 1) + return answer + + # Cancels all variables in a list + # input: varList, a list of variables to be set to False (list of ints) + # result: adds a clause of -i for every i in the list + def cancelList(self, varList): + for i in varList: + self.clauses.append([-i]) + + # Guarantees only one of the items from a list is True + # input: varList, a list of variables, from which one should be True (list + # of ints) + # result: adds a clause to guarantee at least one of the variables is True + # as well as clauses guaranteeing no more than one of the variables are + # True + def exactlyOneFromList(self, varList): + atLeastOneClause = varList + self.clauses.append(atLeastOneClause) + + for i in range(len(varList)): + for j in range(i + 1, len(varList)): + noDoublesClause = [-varList[i], -varList[j]] + self.clauses.append(noDoublesClause) + + # Gets the board position from the variable number + # input: i, the variable number (int) + # output: board position of the variable (2-tuple of ints) + def positionFromNumber(self, i): + row = ((i - 1) // self.size) + col = ((i - 1) % self.size) + return (row, col) + + # Adds clauses for Rule One (column 0 and row 1 are free, column 1 and row + # 0 have exactly one position filled) + # input: none + # result: clauses have been added + def ruleOne(self): + self.cancelList(self.getColumn(0)) + self.cancelList(self.getRow(1)) + + self.exactlyOneFromList(self.getColumn(1)) + self.exactlyOneFromList(self.getRow(0)) + + # Adds clauses for Rule Two (column and row 1/2 are free) + # input: none + # result: clauses have been added + def ruleTwo(self): + half = math.ceil(self.size / 2) + self.cancelList(self.getColumn(half)) + self.cancelList(self.getRow(half)) + + # Adds clauses for Rule Three A (for every j from 2 to n, either row j or + # row 1 - j is occupied. Same with columns) + # input: none + # result: clauses have been added + def ruleThreeA(self): + for j in range(2, self.size): + if j != math.ceil(self.size / 2): + combinedRowList = self.getRow(j) + combinedRowList.extend(self.getRow(1-j)) + + combinedColList = self.getColumn(j) + combinedColList.extend(self.getColumn(1-j)) + + self.exactlyOneFromList(combinedRowList) + self.exactlyOneFromList(combinedColList) + # Adds clauses for Rule Three B (row j occupied iff col j is ocucpied) + # input: none + # result: clauses have been added + def ruleThreeB(self): + for j in range(2, self.size): + crossSection = ((j - 1) * self.size) + j + row = self.getRow(j) + for space in row: + if space != crossSection: + impliesClause = [-space] + implication = [i for i in self.getColumn(j) if i != crossSection] + impliesClause.extend(implication) + self.clauses.append(impliesClause) + col = self.getColumn(j) + for space in col: + if space != crossSection: + impliesClause = [-space] + implication = [i for i in self.getRow(j) if i != crossSection] + impliesClause.extend(implication) + self.clauses.append(impliesClause) + + # Adds clauses for Rule Four (either diagonal j or -j is occupied, but not + # both) + # input: none + # result: clauses have been added + def ruleFour(self): + for j in range(1, self.size): + combinedList = self.getDiagonal(j) + combinedList.extend(self.getDiagonal(-j)) + self.exactlyOneFromList(combinedList) + + # Solves the SAT problem and stores the solution to self.solution + # input: none + # result: self.solution contains solution + def solve(self): + g3 = Glucose3() + for clause in self.clauses: + g3.add_clause(clause) + + if g3.solve(): + self.solution = g3.get_model() + + return + + # Gets the NS1D0 from the stored solution. If the NS1D0 received is too + # short, that means that there is a sub-sequence. Eliminate the current + # solution and try again + # input: None + # output: an NS1D0 sequence from this order n + def getNS1D0FromSolution(self): + sequence = [0] + while sequence[-1] != 1: + for num in self.solution: + pair = self.positionFromNumber(num) + if pair[0] == sequence[-1]: + sequence.append(pair[1]) + if len(sequence) <(self.size + 1)/2: + notASolution = [-i for i in self.solution] + self.clauses.append(notASolution) + self.solve() + return self.getNS1D0FromSolution() + return sequence + + \ No newline at end of file