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
    # OR if immediate_setup = False, just initialize self.size = n so that 
    # setup and solve can be timed independently
    def __init__(self, n, solver_origin=Glucose3, immediate_setup = True):
        self.size = n
        self.solver = solver_origin()
        self.assumptions = []
        if immediate_setup:
            self.setUpBoard()
            
            
            self.solve()
            self.ns1d0 = self.getNS1D0FromSolution(0)[0]
    
    # Sets up the chess board for size n
    # result: the chess board is set up
    def setUpBoard(self):
        self.vars = [i for i in range(1, (self.size * self.size) + 1)]
        self.clauses = []
        self.ruleOne()
        self.ruleTwo()
        self.ruleThreeA()
        self.ruleThreeB()
        self.ruleFour()
    
    # 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, assumptions=None):
       
        for clause in self.clauses:
            self.solver.add_clause(clause)
        if assumptions != None:
            if self.solver.solve(assumptions=assumptions):
                self.solution = self.solver.get_model()
        else:
            if self.solver.solve():
                self.solution = self.solver.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: n, the number of times the function has been run already
    # output: an NS1D0 sequence from this order n, and the number of times the 
        # function was run already
    def getNS1D0FromSolution(self, n):
        n+= 1
        sequence = [0]
        while sequence[-1] != 1:
            for num in self.solution:
                if num > 0:
                    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(n)
        return sequence, n
        
     # Gets the NS1D0 from the stored solution using assumptions. If the NS1D0 
        # received is tooshort, that means that there is a sub-sequence. 
        # Eliminate the current solution and try again
    # input: n, the number of times the function has been run already
    # output: an NS1D0 sequence from this order n, and the number of times the 
        # function was run already
    def getNS1D0FromSolutionWithAssumptions(self, n):
        n+= 1
        print(n)
        sequence = [0]
        while sequence[-1] != 1:
            for num in self.solution:
                if num > 0:
                    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 [j for j in self.solution if j > 0]]
            assumptionsSet = set(self.assumptions)
            originalSet = assumptionsSet.copy()
            assumptionsSet.update(set(notASolution))
            if assumptionsSet == originalSet:
                return None
                                 
            self.assumptions = list(assumptionsSet)
            self.solve(self.assumptions)
            return self.getNS1D0FromSolutionWithAssumptions(n)
        return sequence, n