diff --git a/ChessBoard.py b/ChessBoard.py index f461d2b553fd0bfe54f02c569be5d61de6ba363f..5cd2d02edc1a6229b60a79154c5a44e46215f7d0 100644 --- a/ChessBoard.py +++ b/ChessBoard.py @@ -8,21 +8,34 @@ Created on Tue Feb 2 09:36:24 2021 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): + # 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.vars = [i for i in range(1, (n*n) + 1)] + 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() - self.solve() - self.ns1d0 = self.getNS1D0FromSolution() # Gets a row from the chessboard # input: row, the row number desired (int) @@ -149,33 +162,68 @@ class ChessBoardRepresentation: # Solves the SAT problem and stores the solution to self.solution # input: none # result: self.solution contains solution - def solve(self): - g3 = Glucose3() + def solve(self, assumptions=None): + for clause in self.clauses: - g3.add_clause(clause) - - if g3.solve(): - self.solution = g3.get_model() + 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: None - # output: an NS1D0 sequence from this order n - def getNS1D0FromSolution(self): + # 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: - pair = self.positionFromNumber(num) - if pair[0] == sequence[-1]: - sequence.append(pair[1]) + 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() - return sequence + 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 \ No newline at end of file