Using some examples from Ramsey theory, this article shows how to use Mathematica‘s Boolean computational capability.

Introduction

Mathematica‘s industrial-strength Boolean computation capability is not used as often as it should be. There probably are several reasons for this lack of use, but it is our view that a primary reason is lack of experience in expressing mathematical problems in the form required for Boolean computation. We look at a typical problem that is susceptible to Boolean analysis and show how to translate it so that it can be tested for satisfiability with Mathematica‘s built-in function SatisfiableQ. The problems we investigate come from an area of mathematics called Ramsey theory. Although Ramsey theory has been studied extensively for over 80 years and still provides many challenges, we neglect the theory (for the most part) and instead concentrate on translating the problems so that they are amenable to Boolean computation and then see what can be accomplished by computation alone. Those interested in learning a little more about Ramsey theory can consult [1]; for a standard reference, see [2].

Boolean Representation

We only concern ourselves with Boolean formulas in conjunctive normal form (cnf). A cnf is a conjunction of disjunctions of statements or their negations; the disjuncts are often called clauses.

An example of a cnf is ; letters represent statements and the symbols , , and stand for “or,” “and,” and “not.” A propositional formula is satisfiable if there is an assignment of true and false to its statements that makes the formula true when evaluated using the usual truth table rules.

Before Mathematica can test whether this formula is satisfiable using SatisfiableQ, we must replace , , and by ||, &&, and !. Here is the translation to a Mathematica expression.

It turns out that the formula is satisfiable.

Application to Ramsey Theory

A well-known problem states that at any party with at least six people, there are at least three mutual acquaintances (each knows the other two) or three mutual strangers (each does not know the other two). In the language of graph theory, if the edges of the complete graph on six vertices, are colored red or blue, there must be either a red or a blue triangle.

We translate this into a satisfiability problem in propositional logic and then use SatisfiableQ to prove this result. More precisely, we show that it is not possible to color the edges of either red or blue without forming either a red or blue triangle, by building a cnf whose satisfaction is equivalent to the existence of such a coloring and then showing that this cnf cannot be satisfied.

More generally, Ramsey theory considers problems of this form: given a complete graph and integers , , with , is it possible to color the graph’s edges red or blue without obtaining a red or a blue as a subgraph?

Begin by numbering the vertices of from 1 to 6 and name its edges with ordered pairs of vertex numbers, , . For each such pair, generate two propositional variables, and , which intuitively express coloring the edge red or blue.

The cnf needs two sets of Boolean clauses.

1. For each edge , the clauses and express that the edge is either red or blue, but not both.
2. For each triangle , , , the clauses and express that not all edges of the triangle can be the same color.

If the cnf that is the conjunction of all these clauses is satisfiable, then it is possible to color the edges of red or blue without obtaining either a red or blue triangle. Moreover, any truth value assignment satisfying this cnf would lead immediately to a coloring of the edges by coloring the edge blue exactly when is assigned to be true. Conversely, a red-blue coloring of the edges of with no monochromatic triangle leads directly to a satisfying assignment of ; simply assign to be true if and only if the edge is colored blue, and so on. We will show that the cnf is unsatisfiable.

The function ColorEdges generates the first set of clauses, where the Mathematica expressions and play the role of and . The function states that the edges of are either one or the other of the given colors. It is generalized to three colors in the last section.

Here is the first set of clauses for the party problem.

The function NoCompleteSubgraph can generate the second set of clauses. gives True if does not contain a with all edges of the given color.

The functions ColorEdges and NoCompleteSubgraph can be extended to treat Ramsey problems for complete graphs with any number of colors and complete subgraphs.

The function puts it all together to obtain our test formula.

Here is an example.

The Boolean formula tests the party problem.

Thus, it is not possible to color the edges of red or blue and avoid a monochromatic triangle.

Although RamseyTest is very fast, there are ways to speed it up. (This is unimportant so far but becomes crucial when considering much larger problems!)

Since vertex 1 is connected to five other vertices, at least three of the connecting edges must be the same color; for if there were at most two red and at most two blue edges there would be at most four connecting edges instead of five. Therefore assume that the first three edges are red and not blue; by symmetry, it makes no difference which color we choose. (Replacements by one-element or unit clauses often result in significantly faster running times in automated theorem provers.)

Of course, the length of is , which is .

The edges of can be colored blue or red without any monochromatic triangles. This is easily shown by hand or with the following computation.

In fact, Mathematica can suggest a coloring. First generate the list v of propositional variables in . Then use SatisfiabilityInstances to indicate the coloring.

This draws the suggested edge-colored graph.

It turns out there are always at least two monochromatic triangles in [3, 4]! Since there is at least one monochromatic triangle in , assume it is formed by the edges , , and and, by symmetry, assume that its edges are all red. The next command modifies accordingly. The first replacement drops the uncertainty about the color of those three edges, the second replacement drops the conditions that those edges are not all the same color, and the Append asserts that indeed they are all red. The result False means that it is impossible to deny that there is a second monochromatic triangle, or, more simply, there is a second monochromatic triangle.

Ramsey Numbers

The Ramsey number, , is defined to be the least integer such that any red-blue edge coloring of results in either a blue or a red . (The previous section showed that .) Not many Ramsey numbers are precisely known [1, 2].

This confirms the result .

This confirms the result .

The calculation took too long and had to be aborted, but the simple idea to speed up the party problem in the previous section makes it possible to show : in any , at least half the edges from vertex 1 must be the same color; that is, edges must be the same color. Unless there is symmetry (i.e., ), we must consider two separate cases, that this color is blue or red. The function QuickerRamseyTest is the faster version of RamseyTest.

For the symmetric case , only one test suffices for each of and .

There are more than 6000 clauses in the cnf constructed to show that , since there are two clauses needed in to rule out any ‘s being all red or all blue and there are 3060 in (). Also, each of these clauses has six negated propositional letters, one for each edge of the (a has edges). In addition, there are the clauses that require each edge of to be red or blue but not both, has edges, and so on. It seems that Mathematica‘s claim of “industrial strength” Boolean capability is fully justified.

A Three-Color Example

Ramsey theory also considers edge colorings with more than two colors. The classical result for three colors is ; that is, it is not possible to color the edges of with three colors without a monochromatic triangle; however, has such a coloring.

This generalizes ColorEdges from two to three colors so that each edge gets exactly one of three colors.

The generalization of RamseyTest takes an additional argument, , and a third color. It tests whether the edges of can be colored with three colors without a monochromatic , , or .

To speed up the calculation, we make use of the following observation. Vertex 1 of is connected by 16 edges to the remaining vertices. Surely, at least six of these edges must get the same color, say red; for if at most five got the same color, there would be at most 15 edges. This leads to a quicker test formula than RamseyTest.

To check , it suffices to check and .

Here is the with its edges colored red, blue, and green separately and together. There are no monochromatic triangles. Each of the three graphs with one color is known to be isomorphic to the Clebsch graph; [5] shows them with their vertices permuted in all possible ways.

Removing Edges

Suppose we remove an edge from ; will it still be the case that any two-coloring of the edges has a monochromatic triangle? Or, if we remove an edge from , will the resulting graph still have the property that any two-coloring of its edges must yield a monochromatic ? We show that Boolean computation is also well suited to investigate these kinds of problems.

Remove from the clauses that require the edge to be blue or green, but not both, and add a statement to color that edge white. The result is satisfiable, which means that removing just one edge from gives a graph that can be two-colored without monochromatic triangles.

This defines an auxiliary function.

Here is the coloring.

Recall that ; however, removing even one edge from allows a two-coloring without a monochromatic .

Unlike the case of with an edge removed, it is too hard to see that the blue and green edge-colored subgraphs contain no monochromatic . FindClique finds the largest complete subgraph, which in both cases is a triangle, not a .

Conclusion

Mathematica‘s Boolean computation is a useful tool for doing research in mathematics.

Acknowledgments

We thank the editor and referee for their generous help, which greatly improved this work.

References

[1]	E. W. Weisstein. “Ramsey Number” from Wolfram MathWorld—A Wolfram Web Resource. mathworld.wolfram.com/RamseyNumber.html.
[2]	R. L. Graham, B. L. Rothschild, and J. H. Spencer, Ramsey Theory, 2nd ed., New York: Wiley-Interscience, 1990.
[3]	A. W. Goodman, “On Sets of Acquaintances and Strangers at Any Party,” American Mathematical Monthly, 66(9), 1959 pp. 778-783. www.jstor.org/stable/2310464.
[4]	G. Beck. “Among Six People, Either Three Know Each Other or Three Are Strangers to Each Other” from the Wolfram Demonstrations Project—A Wolfram Web Resource. www.demonstrations.wolfram.com/AmongSixPeopleEitherThreeKnowEachOtherOrThreeAreStrangersToE.
[5]	E. Pegg Jr. “Ramsey(3,3,3)>16” from the Wolfram Demonstrations Project—A Wolfram Web Resource. www.demonstrations.wolfram.com/Ramsey33316.
R. Cowen, “Using Boolean Computation to Solve Some Problems from Ramsey Theory,” The Mathematica Journal, 2013. dx.doi.org/doi:10.3888/tmj.15-10.

About the Author

Robert Cowen is a professor of mathematics emeritus at Queens College, CUNY. He uses Mathematica in his own research and has written a textbook with John Kennedy called Discovering Mathematics with Mathematica. His web page can be found at sites.google.com/site/robertcowen.

Robert Cowen
Department of Mathematics
Queens College, CUNY
Flushing, NY 11367
robert.cowen@gmail.com