This was my submission to the
CS Club hackathon. This was my first excuse to write what I would call a less than trivial APL program and overall, the experience was enlightening and fun. It took, in total, probably around an hour to write.
SAT Solver in APLThe following is a solution to the SAT problem that determines exhaustively all of the possible solutions to a given problem. This page displays APL characters. Make sure that you are using a font in your web browser that
supports these characters.
Encoding the Problem SpaceA SAT problem can be expressed in Conjuctive normal form, where we have a set of conjuctions of disjunctions:
(X ∨ ... ∨ X) ^ ... ^ (X ∨ ... ∨ X)
We can think of each clause in the conjuction as a set of variables, either negated or not. If we assume that we have D number of variables, then we can encode each clause as a vector of true and false values. This vector contains 2D elements. Each slot in this vector correponds to a possible value of a variable or the negation of a variable X. If that form appears directly in the clause, then the slot corresponding to that vector contains true. Otherwise, it contains false. For example, consider the following clause:
(X ∨ ~ Y)
Assuming that we have three variables X, Y, and Z, then the encoding of this into a vector is as follows:
Z Y X ~Z ~Y ~X
0 0 1 0 1 0
Notice that for each half of the vector corresponding to either the negative or positive values, we list the variables from last to first. You will see why later.
Given this, we can now encode all of the clauses as a N by 2D matrix, where N is the number of clauses, and D is the number of variables that we have. The rows of this matrix correspond to the clauses, and the columns to the variable terms (two per variable, positive and negative).
We will call this Clause matrix C.
Encoding the solutionGiven D variables, we know that there are (2*D)-1 ways to value those variables (* here is used in its dyadic form to represent exponentiation, multiplication is ×). We can think of each possible assignment for a 3 variable problem as follows:
000
001
010
011
100
101
110
111
Notice that this is just the progression of numbers from 0 to ''(2*3)-1''. Let's assume for a moment that we zero index everything:
⎕IO ← 0
We can thus construct the possible solutions in binary using the following expression:
T←(D⍴2)⊤⍳(2*D)
This gives us a D by (2*D) matrix where each column corresponds to a possible solution. However, this does not give us the negative assignments, which are just the complement of the positive ones. We can do that with by concatenating the positive matrix with its complement along the first axis:
V←T⍪~T
Now T is our positive matrix and V is our total solution space with 2D rows.
Computing the solutionsNow we have an N by 2D clause matrix C and a 2D by (2*D) solution matrix V. Since the colunm count of C equals the row count of V, we can perform an inner product computation on these two matrices. For those unfamiliar with inner product, matrix multiplication is an inner product using multiplication and addition:
A+.×B ⍝ Matrix multiplication of A and B
However, instead of multiplying each element in the columns and rows of C and V, we want to compute their logical ^ value. We then replace addition with ∨ and this gives us a result like so:
C∨.^V
The result is a matrix where each element (x,y) indicates whether clause x was satisfied by potential solution y. Then we just need to compress the columns using ^ and we have a vector indicating what solutions satisfied the entire expression. We can then use this matrix to select the solution numbers from our original potential solution pool and encode those as binary. The final matrix has one solution for each column.
Solution SummaryThe resulting function in APLX looks like this:
∇ R ← D SAT C;T
T←(D⍴2)⊤⍳(2*D)
(D⍴2)⊤(^⌿C∨.^T⍪~T)/⍳(2*D)
∇
My Opera
