Update ChessBoard.py with assumptions-based function and finer control over...

Update ChessBoard.py with assumptions-based function and finer control over when bits of setup and solve begin (for timing purposes). By default, everything acts the same as before, but with new options.

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