At this point in the project, I have written all of the code necessary to generate a Steiner Triple System through our chess board method, solved via a SAT solver. This seems like a good time to update on how my code works, what it does, and where you can access it!
Note: This update was written on February 11th, 2021 and refers to file status as of commit 032dbe4f.
bruteForce.py
This is the very first piece of code I wrote for this project. Its purpose is to generate an NS1D0 sequence by brute force; essentially, it takes every potential sequence and checks to see if it matches the rules for NS1D0 sequences. If it does, then that sequence is returned.
The Important Function: In this file, the most important function is generateNS1D0. This function takes an integer input, n, that represents the order of the desired NS1D0 sequence. It generates all possible sequences: all sequences of length (n+1)/2 containing numbers from 2 to n, starting with a 0, and ending with a 1. It then checks each of those lists against 5 criteria: the size, and all four rules of NS1D0 sequences. It returns every sequence that met all of those criteria.
generateSteiner.py
This file, as you may guess, generates a Steiner Triple System. It will take an NS1D0 sequence and, following the algorithm laid out in the NS1D0 paper, generate a Steiner Triple System from that sequence.
The Important Function: In generateSteiner, the most important function is generateSteinerTripleSystem. This function takes as input a valid NS1D0 sequence, which can be generated any number of ways, and gets its inductor sequence and its sign inductor sequence using other functions in the file. Then, it generates a 3-Triangulation by getting every pair of numbers in the NS1D0 sequence and generating the third number by using the circular operator on a and b with the inductor. The Steiner System is then generated using the algorithm described in the NS1D0 paper.
ChessBoard.py
This file implements a class that creates a Chess Board representation of the desired NS1D0 sequence and will solve for it using the Glucose 3 SAT solver.
This is the most important file to our project, as it actually generates the NS1D0 sequence through the chess board method. For that reason, I will not just focus on a single method, but talk about how it works as a whole.
First Steps
To initialize a ChessBoardRepresentation, the programmer must provide it with an order of the desired NS1D0 sequence, n. From that n, the program sets what the SAT solver’s variables will be; specifically, it sets up the numbers 1 to n*n + 1, where each variable will represent a spot on the board. The top left spot is 1, and the rest are numbered sequentially from left to right and top to bottom. Each variable can either be True (the space is occupied by a queen) or False (the space is unoccupied). The initializer also initializes its clauses to be an empty list, as we don’t have any clauses yet.
An Aside on SAT Solvers
Because I have not yet had the chance to write a blog post on SAT solvers, I will use this space to briefly discuss what a SAT solver inputs and outputs. I will not cover exactly how the SAT solver works here.
A SAT solver is a program that can quickly solve Boolean equations. A Boolean equation is an equation using Boolean operators (AND, OR, XOR, etc) that is performed on a set of Boolean variables (variables that have two possible values, true or false). A solution to a Boolean equation is a set of variables that fulfills that equation. For example, the equation: ((a and b) or c)
Has this:
A=true
B=true
C=false
As one possible solution. SAT solvers work on a specific type of Boolean equation, Boolean equations that are in Conjunctive Normal Form (CNF). CNF equations contain only the AND and OR operators; specifically, they are composed of a series of OR clauses that are connected by ANDs. The example equation of ((a and b) or c) is not in CNF because it is two AND clauses connected by an OR. However, all Boolean expressions can be reordered to be in CNF: ((a and b) or c)
Can become
(a or c) and (b or c)
The two equations will have all the same solutions. As you can see, changing an expression to CNF can introduce more clauses than the original equation had, and some transformations become very expensive. For this reason, not all problems are suitable for SAT solvers. However, this particular problem wound up being a good match.
Types of Clauses
After determining our variables, the ChessBoardRepresentation class has to add clauses to get our final equation. The vast majority of these clauses arise simply from the rules of an NS1D0 queens-layout; and most of those rules can be written as one of these types of clause:
Only One of These Can Be True
None of These Can Be True
Only One of These Can Be True
This is an interesting equation to make in a SAT solver. In order to tell the solver we want only one of a list of variables to be true, we have to first tell it that AT LEAST one of those variables must be true, and then tell it that AT MOST one of those variables must be true. The first is easy, for the variables a, b, c, and d, saying that at least one of them must be true is as simple as
a or b or c or d
This holds true for any number of variables, the AT LEAST ONE clause is simply an OR clause of all of the variables.
Saying that AT MOST is true is more difficult. This is essentially saying that no pair of the variables can be true, so we generate all pairs of the variables and say that one of them must be false. For variables a, b, c, and d, this looks like: a’ or b’
a’ or c’
a’ or d’
b’ or c’
b’ or d’
c’ or d’
(a’ is the same as NOT a)
You can see that the combination of these two sets of clauses will tell the SAT solver that exactly one of the variables must be true.
None of These Can Be True
This one is very simple. We just tell the sat solver “NOT variable” for every variable in the given list. For variables a, b, c, and d, this looks like:
a’
b’
c’
d’
Easy as pie!
Making the Clauses
The ChessBoardRepresentation has a method for each of those requirements, from there we can generate each of the rules.
Rule One
Rule one of legal NS1D0 n-queens layouts is simple: row 1 and column 0 must be unoccupied, while column 1 and row 0 must have one queen each. We simply call the None Of These Can Be True method on the variables in row 1 and column 0, and the Only One of These Can Be True method on the variables in column 1 and row 0
Rule 2
Rule 2 is also fairly simple! The row and column at the position (n+1)/2 must be unoccupied. We call the None of These Can Be True method on row and column (n+1)/2
Rule 3
Rule 3 more easily breaks down into two parts: Rule 3A and Rule 3B.
Rule 3A
The first part of rule 3 is as follows: for all j between 2 and n (excluding (n+1)/2), either row j or row 1-j must be occupied, but not both. The same is true for columns. For this method, I loop through every j in that sequence and create a list of variables containing both row j and row 1 – j. If we call the Only One of These Can Be True method on that list, we know that one or the other row will be occupied but not both! The same applies to the columns.
Rule 3B
The second part of rule 3 is tricky. It states that row j can be occupied IF AND ONLY IF column j is occupied. This is the only rule that can not be expressed as Only One of These Can Be True or None of These Can Be True. This can be written as a set of “implies” clauses; for instance:
If position (3,2) is occupied, then one of the pieces in column 3 must be occupied.d
An implies clause is easily changed to a CNF clause as follows:
A => (B or C or D)
Becomes
A’ or B or C or D.
Therefore, to assemble this rule we must have two implies clause for every piece on the board (i, j); one that says that one of the spaces in the column i must be occupied, and one that says that one of the spaces in row j must be occupied.
Rule 4
Rule 4 is a return to normalcy. It states that for every i between 1 and n, either the diagonal i or the diagonal -i must be occupied. This is fulfilled in much the same way as rule 3A.
Solving the Equation
Once all of the rules have been assembled, the class will call the solve function. This puts the list of clauses into a SAT solver, we used Glucose 3 from the pySAT module and save its solution to the class’s solution field.
Interpreting the Solution
Of course, the solution is merely a set of trues and falses for the variables, so it must be interpreted. We have a function, getNS1D0FromSolution that addresses this by: a) retrieving the board spaces associated with every variable and saving the true ones (the occupied spaces), and
b) turning that set of spaces into an NS1D0 sequence. The method for doing this is as follows:
1) Make an empty list, called ns1d0
2) Find the piece in row 0. Add a 0 to ns1d0.
3) Look at that piece’s column, call it i. Add i to ns1d0
4) Find the piece in row i.
5) Repeat 3 and 4 until 4 doesn’t find a piece (should be when i = 1).
Interestingly, the chess board doesn’t always return a solution that will return a valid NS1D0 sequence. This is because we are using the chess board in the reverse situation of its expected use. The rules of the chessboard were intended to be used to verify whether a sequence was an NS1D0 sequence; you would place pieces in the correct spaces for the NS1D0 sequence and if it followed the chessboard rules it was guaranteed to be an NS1D0 sequence. However, not every n-queens legal arrangement on the board is guaranteed to return a valid sequence. The layouts that do not create an NS1D0 sequence have pieces that are never reached by the method described above, so they are not incorporated into the sequence.
The simplest workaround to this problem is simply to run the SAT solver again after adding a clause that the previous solution is not allowed, which is what I have currently implemented. The method will keep resolving the problem until it encounters a valid solution, which usually takes less than 3 tries. It then returns the NS1D0 Sequence!
main.py
The final piece of the puzzle, and the python file meant to be run independently. When run, it prompts the user to enter a number n, the order of the desired NS1D0 sequence. It puts that number into a ChessBoardRepresentation, gets the NS1D0 sequence from that and puts it into generateSteiner.py’s generateSteinerTripleSystem function and prints out the triple system!
All of my code can be accessed at:
https://gitlab.cci.drexel.edu/lap368/steiner-triples-and-sat-solvers
Comments