SAT Problem with TensorNetwork

by Volha Okrut

Boolean Logic

Suppose we have a simple CFN expression, a logical expression based on logical AND (called conjunction) and logical OR (disjunctions). Strictly defined, CFN expression is a conjunction (AND) of several disjunctions (OR) of logical literals (Xi).

Let me come up with the following example of CFN expression:

(True AND False) OR (NOT True AND True)

Now let's simplify it:

False OR False

And at the end we get:

False

That's simple!

Now, instead of logical AND I will use ∨ notation, instead of logical OR - ∧. Additionally, if I want to say NOT True I use ¬True. This is just a formality, and yet it allows us to write these expressions in a more clearer and readable form.

Of course, the concept of boolean expressions would be pretty useless if always you had to start with the same positions of True and False. So let me introduce variables (known as literals) into the formula - this allows me to have the same expression evaluating to different end-results. Now instead of our initial formula we have:

(X1 ∨ X2) ∧ (¬X1 ∨ X3)

You can notice that if we place X1 to be True, X2 to be False, and X3 to be True, we would have the same expression as in the begining of the article. If we assign the variables different values, then we of course will get different result.

SAT Problem and real-life example

So what is a SAT Problem? SAT Problem - short from SATISFABILITY problem - concerns with the number of ways in which you can arrange the given literals in order for the whole expression to be evaluated to True.

Let's start by jumping in with an example of a SAT problem. Suppose that you need to go grocery shopping, and need to visit three stores: Costco, Home Depot, and Walmart. Costco is open in the morning and evening, Home Depot is open in the evening only, and Walmart is open in the morning only. You can only be in one place at a time, and shopping at a given store takes up the entire morning or evening. Can you go to all three stores in a day? To a human, it is intuitively obvious that the answer is no. Since Home Depot and Walmart offer us only one time option (evening and morning, respectively), then we have to go there at those times. However, this leaves no time for a Costco trip, so it's evident that this "puzzle" has no solution. Now suppose instead of three stores, you were given three thousand (each with its own schedule), and instead of two times, you were given all the hours of a day? At this point, the problem becomes intractable for a human. Luckily, though, cruching numbers and analyzing thousands of different options are what computers excel at.

So, how could we encode the above problem in a way that a computer could understand?

One solution would be to re-write the problem involving boolean variables, which can either be true or false. For example, using the example of three stores and two times, let's make six variables:

• Ce: Whether we go to Costco in the evening.
• Cm: Whether we go to Costco in the morning.
• He: Whether we go to Home Depot in the evening.
• Hm: Whether we go to Home Depot in the morning.
• We: Whether we go to Walmart in the evening.
• Wm: Whether we go to Walmart in the morning.

Each of these variables if true (or 1) if we visit the store at the corresponding time, and false (or 0) otherwise. Next, we form some constraints on these variables, and express them in a unified form we could feed to a computer.

First, we know that we can only be in one place at a given time. For example, if we are at Costco in the morning (that is, Cm=1 ), then we cannot be at Home Depot or Walmart in the morning (and thus Hm=Wm=0). Using notation introduced above we can express that constrains as:

Cm ∨ ¬Hm ∨ ¬Wm

Of course, we know that at a given time, we could go to Costco, Home Depot, or Walmart, so Cm doesn't have to be true. Thus, the constraint that we only go to one place in the evening can be represented as:

( Ce ∧ ¬He ∧ ¬We ) ∨ ( ¬Ce ∧ He ∧ ¬We ) ∨ ( ¬Ce ∧ ¬He ∧ We )

Similarly, the constraint that we only go to one place in the morning is:

( Cm ∧ ¬Hm ∧ ¬Wm ) ∨ ( ¬Cm ∧ Hm ∧ ¬Wm ) ∨ ( ¬Cm ∧ ¬Hm ∧ Wm )

Next, we need a constraint that we go to Costco in either the morning or evening, which we can represent as Cm ∨ Ce: either we go to Costco in the morning, or in the evening. We have similar constraints for Walmart and Home Depot, yielding the following constraint to represent that we must go to each store:

( Cm ∨ Ce) ∧ ( Hm ∨ He ) ∧ ( Wm ∨ We )

Thus, the full set of constraints for our problem is

( Cm ∨ Ce) ∧ ( Hm ∨ He ) ∧ ( Wm ∨ We ) ∧ ( Cm ∧ ¬Hm ∧ ¬Wm ) ∨ ( ¬Cm ∧ Hm ∧ ¬Wm ) ∨ ( ¬Cm ∧ ¬Hm ∧ Wm ) ∧ ( Ce ∧ ¬He ∧ ¬We ) ∨ ( ¬Ce ∧ He ∧ ¬We ) ∨ ( ¬Ce ∧ ¬He ∧ We )

To find out whether we can complete our shopping trip, we must find a set of true or false values for all our boolean variables such that the constraints are satisfied. This type of problem is known as the boolean satisfiability problem, often abbreviated to just "SAT". A program that finds solutions to these problems is known as a SAT solver.

SAT Problem

SAT problem has been viewed from many different ways, in this tutorial we will learn how to solve this problem using tensors and TensorNetwork library. To be comfartable with tensors you have to know some basics about Penrose’s Graphical Notation. Check this nice article on Medium that covers this topic extensively.

Suppose we are given four variables: X1, X2, X3, X4. We want to find truth values to all four Xi literals so that the CNF expression is true:

( ¬X1 ∨ ¬X3 ∨ ¬X4 ) ∧ ( X2 ∨ X3 ∨ ¬X4 ) ∧ ( X1 ∨ ¬X2 ∨ X4 ) ∧ ( X1 ∨ X3 ∨ X4 ) ∧ ( ¬X1 ∨ X2 ∨ ¬X3 )

First, we need to define how we encode our input CNF expressions that we want to satisfy:

• Each logical literal is represented as either a positive or negative integer, where i and -i correpond to the logical literals xi and ¬xi, respectively.
• Each clause in the expression, i.e., disjunction of literals, is represented as a tuple of such encoding of literals, e.g., (-1, 2, -3) represents the disjunction ( ¬x1 ∨ x2 ∨ ¬x3 ).
• The entire conjunctive expression is a list of such tuples, e.g., the expression above would have encoding: [(-1, -3, -4), (2, 3, -4), (1, -2, 4), (1, 3, 4), (-1, 2, -3)]

It is worth to say that we can solve two problems here:

1. Find the exact number of all possible solutions to the given SAT problem if these solutions exist.
2. Find all possible solutions to a given SAT problem if these solutions exist.

SAT solver using tensors and TensorNetwork

Finding all possible solutions to the given SAT

First, we create a function

# sat_tn(clauses)

which solves the given 3SAT problem.

We find the maximum indexed logical variable we have, and use that as our count of the number of logical variables. We iterate through each disjunction and calculate absolute value for each variable in the conjunction. The number of logical variables is the maximum element in var_set which is then stored in num_vars:

var_set = set()
for clause in clauses:
    var_set |= {abs(x) for x in clause}
num_vars = max(var_set)

After iterating expression [(-1, -3, -4), (2, 3, -4), (1, -2, 4), (1, 3, 4), (-1, 2, -3)], I should get the following result:

var_set final =  {1, 3, 4, 2}
num_vars =  4

Now, we will build the tensor network. Variable nodes (literals) will be represented as num_vars tensors with the shape(1,2) filled with ones:

node [1 1]

This particular shape of nodes is needed for matrix multiplication. I will explain why we need it in just a moment. Since each of the variable nodes is a vector, each of them will have only one edge, which I will store as unconnected edges (dangling edges) in var_edges:

var_edges.append(new_node[0])

The second step is to create nodes for all clauses. For each clause we will create a tensor of third rank (a 3D matrix) with two fields in each dimenshion as we want as many fields as there are possible solutions (variation of initial literals) to this clause. Each logical variable Xi has two posible literals: itself (Xi), and its negation (¬Xi). Thus for each clause we have 2^3 = 8 solutions and each soltution can be accessed using the coditions of the variables (solution to clause (X1, X2, X3) with X1 = 1, X2 = 0 and X3 = 1 will be found under clause_tensor[1, 0, 1] field and will be 1 (True)). The formula (-np.sign(x) + 1) // 2 gives us 0 or 1 depending on the sign of the variable (its negation).

for clause in clauses:
    a, b, c, = clause
    clause_tensor = np.ones((2, 2, 2), dtype=np.int32)
    clause_tensor[(-np.sign(a) + 1) // 2, (-np.sign(b) + 1) // 2,
                  (-np.sign(c) + 1) // 2] = 0
    clause_node = tn.Node(clause_tensor)

Now, with everything prepare, I can explain you why tensors are such an elegant solution to this problen. As initially we have several expressions that contain only OR operators unified under AND operator, it might be useful to view those operators as logical summation and multiplication respectively. In other words, for logical operator OR, it doesn't matter how many Falses you have - it takes only one True to bring the expression to True (same as summation). On contrary, while you might have all but one Trues in your expression, operator AND will evaluate it to False if there was at least one constituent set to False (same as multiplication).

The same idea will be applied to tensores in the problem. We have constructed 3D matrices to clauses in such a way that they are filled in with 1 for all possible entries except one (think about it: when the clause consists only of logical OR (summation) it is false only with all of its constituents being evaluated to False). Now, if we are able to correctly multiply all the matricies with each other, all of the configuration that have at least one 0 in it will end up being 0 and the only ones left have all of the clauses being True - exactly what we need! The initial vectoes for literals had to be set in such a way in order for matrices to be reduced after being multiplied with them.

Bear with me, the last step is to connect variable to the clause. Operator (^) is used as a shortcut for tn.connect(clause_node, tensor_node) - function for dot product between matrices introduced in Tensor Network library. The result is stored into the first variable.

For now we just have our clause nodes and literal vectores in place. In order to connect them, for every edge of each clause (they all have three edges - by the numbers of literals in the clause) we will create a copy vectore with the same dimension (3D matrix, extending to two fields to each side). The zero numbered edge of the copy_tensor_node we will connect to the one of the edges of the clause matrix. The one numbered edge will be connected to one of the var_edges - so called dangling edges - edges that are not yet connected to any other edge. Finally, the last edge (numbered with two) will take the place of the edge from var_edges that was just paired up with the one numbered edge.

for i, var in enumerate(clause):
      copy_tensor_node = tn.CopyNode(3, 2)
      clause_node[i] ^ copy_tensor_node[0]
      var_edges[abs(var) - 1] ^ copy_tensor_node[1]
      var_edges[abs(var) - 1] = copy_tensor_node[2]

This process will be repeated until all the edges coming from clause tensores have been paired up with a copy tensor node. By the end of this, in var_edges we will have stored all the unconnected edges of this system of multiplied tensors. And that is exactly what will be returened from the function:

return var_edges

Let gather all the said above in to one program and run with the given set of variables.

Find the exact number of all possible solutions to the given SAT

In order to find exact number of all possible solutions to the given SAT problem, we can do full contractions of the adges of the clauses. In other words, we have to calculate a trace of the tensor network we have build in the first part of the tutorial. This is done by essentially creating the same tensor net and then connecting all the dangling edges of the first net to the dangling edges of the second.

Congratulations! You have now learned how to write SAT Solver program with TensorNetwork! Down below you can play with choosing different clauses as your starting points and then seeing with how many ways it can be solved.

References:

1. SAT solver example
2. An exact tensor network for the 3SAT problem
3. Penrose’s Graphical Notation
4. https://github.com/google/TensorNetwork
5. Writing a SAT Solver