Upload ChessBoard

ChessBoard.py

+#!/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