Solving Semidecidable Problems in Group Theory Slides
MODERATOR: This amazing workshop.
It’s my pleasure to introduce Giles Gardam. Giles is not traditionally an expert in any of the areas of this workshop. He is a geometric group theorist, but he’s using our tools to prove amazing things about unit conjectures compared to the conventional view.
GILES GARDAM: Thanks, [? Flores. ?] Yeah, it’s a real thrill to be here. Thanks for the organizers, thanks to SLMath, and thanks to the Simons Institute. My title is “Solving semidecidable problems in group theory.” And “solving” here means not just like solving in the mathematical sense. Solving not just in the traditional sense that we want to answer this mathematical question, but solving in the sense we’re going to use a SAT solver.
But we’ll go through the title backwards. First I’ll tell you about group theory. Then I’ll talk about some semidecidable problems in group theory. And then finally at the end, we’ll talk about feeding them into a SAT solver. The slides are on my website if you want to follow along there.
All right, so it’s the first talk of the day. We’ll warm up fairly slowly. Just recalling some examples of groups you might have seen. A group is, of course, the algebraic object we use to study symmetry. For example, the symmetric group Sym(n) or S(n). That’s all permutations of an n-element set, for example, 1 through to n or the integers. That’s a group under addition. Although for today, I’ll usually stick to multiplicative notation. So rather than thinking of integers as you know them, that will be positive and negative powers of some generator t.
Another example of a group that’s usually infinite, we take the general linear group GLn(K). That’s just all n by n matrices over some field k that are invertible. The group operation here is just multiplication.
If I have a group that I’m interested in and I want to tell you about it, I want to tell you exactly what that group is. There’s one really naive thing I can do, and that’s just tell you exactly what the group operation is, what the group law is for all pairs of elements. So I could just give you the multiplication table for that group. It’s certainly naive, but it just works. For example, if I take the symmetric group S(3) or Sym(3), we’ve got six permutations of our three-element set written here in this sort of cycle notation.
OK, so that’s one way I could tell you about a group. Another way I could tell you about a group would be to tell you about its Cayley graph, which is an object that we really love, especially in my part of group theory, geometric group theory. The Cayley graph has one vertex for each element of the group. I fix some generating set of elements S, and then for each generator, I add an edge from g to g times s. Giving you this graph is really giving you the exact same data as the two columns of the multiplication table. The fact that these two elements generate the group means that everything can be written as words in those generators and their inverses, which is just the same thing as saying that this graph is a connected graph considered as an undirected graph.
So that’s all well and good, but if I want to talk about infinite groups, maybe in a bit of trouble, I probably don’t want to tell you some infinite table. I want some better way of specifying an infinite group. With a finite amount of data, the standard way we do that is to study finitely presented groups. So I can study a group defined by presentation with generators A and relations R. The relations live in what I’ve denoted here F(A), which is the free group generated by those letters A.
I guess probably most people coming from maths have seen the free group. To think about it in more like CS sort of terms, we take all words of finite length on the alphabet and the formal inverses of the letters from that alphabet. We quotient out by this equivalence relation, saying, “I’m allowed to insert or delete a pair of adjacent letters that are inverse to each other.” Under string concatenation, this is now a group.
I can consider the normal subgroup generated by those relations R, which I’ve denoted here as a double angle brackets. So that’s then what’s called a normal subgroup. I can quotient that out, and the corresponding quotient group is my finitely presented group. This is how I formally define it.
We can just think I’ve got these generators from the set A, and everything that’s in the set R is trivial. That’s just like the biggest group with those generators and those relations. We call it a finite presentation of both those sets as finite.
Examples:
- If I take two generators a and b, and I say their commutator is trivial, that’s the same thing as saying a, b = b, a. The generators commute, and I get the free abelian group Z².
- Or I could take one generator and say its 5th power is trivial. Then I’ve got the cyclic group of order 5.
Now I can tell you about lots of the infinite groups that I can define with a finite amount of data. I can ask you algorithmic questions about them. But the bad news is, basically, nothing is decidable. This is really epitomized by the Novikov-Boone theorem saying there exist finitely presented groups for which the word problem is undecidable.
The word problem is asking, given a word in the group, is that actually just the trivial element of the group or not? Basically, you can take any Turing machine and encode it with a finitely presented group and reduce the halting problem to the Turing machine to the word problem for the group. So that’s sort of bad news in terms of decidability.
But the good news is often things are at least semidecidable. For example, the word problem one direction is decidable if the word is trivial; then I can run a very naive algorithm that will eventually produce a proof of that. Because something is trivial if and only if it’s some finite product of conjugates of the relations and their inverses.
We can just sort of enumerate larger and larger expressions. If something is trivial, you’ll eventually be able to prove that. This is really general; it comes up all the time. It’s very, very common that you’re interested in some question about groups. It’s not decidable, but at least it’s semidecidable.
Generally, it’s obviously semidecidable, and it’s a real theorem to show that it’s actually undecidable or an application of somebody else’s theorem. I just told you about the word problem. I wanted to highlight one other example, which is asking, given a finitely presented group, does that have some non-trivial finite quotient?
The fact that this is not decidable is a theorem of Bridson and Wilton, and the reason I highlight that is that this is somehow a little different from typical results of this flavor, because in this case, the direction of the problem we can solve is showing that something is non-trivial. Usually, the things that we can do are prove things are equal or prove things are trivial. And the fact that this is semidecidable is just, well, I can enumerate for increasing values of n all possible ways of mapping my generators to the symmetric group on n letters. I can test if that actually defines a well-defined group homomorphism, just by checking that the relations are satisfied.
So if there is a non-trivial finite quotient, I’ll eventually find it. But Bridson-Wilton show that the other direction is not decidable by appealing to a result of Slobodskoy that universal theory of finite groups is undecidable.
OK, now the last example is the group abelian. This is something that we can decide one direction because my group is abelian if and only if all pairs of generators commute. So I just need to solve, say, n choose 2 if n is the number of generators, n choose 2 instances of the word problem in order to decide if my group is abelian. OK.
So that will decide one direction, but I can’t in general decide that a group is non-abelian. But you can see in this last example, all of the difficulty just comes down to the word problem. That’s really where all the difficulties lie. So I can try and just encapsulate that and say, let’s pretend I have an oracle that solves the word problem for me. Well, now I can decide if a group is abelian because I just have reduced it to the word problem.
Similarly, we can also take problems which are neither semidecidable nor co-semidecidable, throw in a word problem oracle, and then at least get semidecidability.
So for example, asking, Does the group have some non-trivial torsion? So an element that’s non-trivial but has some positive power that is the trivial element. And so Lampe showed that neither direction of this problem is semidecidable.
But if I have an oracle for the word problem, then I can just enumerate words, check if they have some positive power that’s trivial using the easy direction of the word problem. And then I can use the oracle for the word problem to check that something really is non-trivial. OK.
So that’s a bit on generalities around semidecidable problems for group theory. I now come to the specific domain that I’m most interested in, studying group rings.
So this is a very natural algebraic object we get combining a group G and a field K. It also has the structure of a K algebra. So it also gets called the group algebra. But for cultural reasons, I’ll mostly just call it a group ring.
So this is a ring we build by taking all finite formal k-linear sums of group elements. As I said, this is just the vector space over the field k with basis G. But of course, I know how to multiply elements of the group, and I know how to multiply elements of the field. So I just sort of extend things in the natural way and define multiplication using, say, this formula.
And now I have a ring, which contains both my group and my field. OK, so we can really just say if I multiply two things, I just multiply the group elements separately and the field elements separately, use distributivity. Or I could think I’m summing over elements K of this sort of expression in terms of all pairs that multiply to give K in the group.
So if you prefer to think of this as finitely supported functions with convolution, that’s another way of thinking about it.
So a nice example, which will be very illustrative for the things I want to talk about later, is if my group G is just the infinite cyclic group, the integers Z, which I’m going to write as the group with one generator and no relations.
So this consists of all positive and negative powers of t. And now, if I consider key linear sums of those positive and negative powers of t, I’m sort of just obviously writing down. Polynomials in T and t inverse.
And really, this is exactly the ring of polynomials that we get back.
And why is the group ring something that shows up naturally and in lots of places?
Well, one key reason goes back to an observation or a perspective that was promoted by the great Emmy Noether, which is that if I want to study representations of my group on k vector spaces, that’s just the same thing as studying modules over this ring.
Because it’s going to be very important for what we’re doing later, I want to just work through some examples of how arithmetic in the group ring works, even though it’s very basic.
So for example, if I took the group Z mod 5, cyclic group of order 5, so powers of this letter t, and I take coefficients from F2, the field with two elements, then I can multiply these two polynomials and get 1 as the answer.
So you could probably just multiply them out, replace factors of t to the 5 with 1, and check that you get this.
But since it’s a slide, I can also just very quickly do the computation for you.
This is a multiplication table for that group. And saying that this thing is 1 is just saying, well, if I pick the rows corresponding to the first factor of this product, the columns corresponding to the second factor, then I have these nine terms.
And they all pair up to cancel because we’re working over the field with two elements except for one. And that’s what we’re left with at the end.
So there are things that I can multiply and get cancellation and end up with just one from this ring, which, as a formal sum, is the one from the field times the trivial element of the group.
And another example. If I had some non-trivial torsion in my group, so some element g that has finite order n at least 2. So g to the n is the trivial element, and a smaller power of g is trivial.
Then I can factorize 1 minus g to the n, like we did in school. And since g to the n is trivial, that gives me a way of writing 0 as the product of two non-zero things.
So we can see that 1 minus g is then a non-zero zero divisor. So you can see in these finite groups or groups of torsion that I’m talking about here, some sort of interesting things are happening in the group.
And the conjectures that we’re about to get to are basically saying torsion is the only way that these sort of weird, interesting things happen.
OK. So these are generally known as the Kaplansky conjectures. Kaplansky is a well-known name in Berkeley. He was the director of what was then called MSRI from ‘84 to ‘92.
And these conjectures are mostly about torsion-free groups. So torsion-free is just saying there is no non-trivial torsion.
So for me, coming from geometric group theory studying infinite groups, this is a pretty natural constraint to add on my group. It is certainly imposing some condition, but morally, I like to think of it as being not that far from studying all infinite groups.
I guess some people, depending on their field, might object to that. But for me, it’s very close to studying all infinite groups.
So for example, in topology, people like aspherical manifolds and their fundamental groups are always torsion-free.
Or if we study finitely-generated groups defined as matrix groups over the complex numbers, so these aren’t torsion-free.
For example, any permutation matrix is one of these things, and they’re certainly torsion. But all of these groups will have a finite index subgroup, which is torsion-free.
So somehow the torsion is very constrained. We’ve got this bound on index to completely avoid torsion if we want.
So what are the Kaplansky’s conjectures there? Well, for the first instance, there are three statements about the group ring saying if we don’t have torsion, Certain elements can’t possibly occur.
So actually, the first two of these were formulated by Graham Higman in his thesis in 1940. But it’s really Kaplansky’s talks and papers from the ’50s onwards that made these conjectures popular, at least in the West.
So we take any torsion-free group G and any field k, then conjecturally, the group ring has no non-trivial units, no non-zero zero divisors, and no non-trivial idempotents.
So to just unpack exactly what these things are saying one by one:
- A unit is some element x that has a multiplicative inverse y.
- It has to be an inverse on both the left and the right, though usually that doesn’t actually make a difference. Usually, one is sufficient for most normal groups, for most well-behaved groups.
And we certainly have lots of invertible elements, lots of units in the group ring. Because every element of a group is just by itself something that’s invertible, that we can just multiply by its inverse from the group.
And every element of the field that’s not 0 is invertible. If I multiply those things, I get all these expressions k times g. And those are all invertible. And those are the so-called trivial units.
The conjecture says those should be the only units that we have. And there should be no non-zero zero divisors. So if I multiply together two things and get 0, then one of those factors had to be 0 itself already.
An idempotent is just something that squares to itself. In school, we learned how to produce two solutions to the equation x squared equals x. And the group ring shouldn’t have any solutions beyond those trivial solutions, 0 and 1.
OK. So those are the three Kaplansky conjectures for torsion-free groups.
For example, what happens if we’re talking about the group of integers? Well, if I say for the unit conjecture, I want to show that if I multiply together two things which aren’t just some scalar multiple of a power of t, and not just these monomials, then I shouldn’t be able to get 1 as the answer.
The way we would prove this for the Laurent polynomials is to say, well, I know if I take two Laurent polynomials and multiply them, I can just read off from the input polynomials exactly what the highest power and the lowest power of the product will be, because there won’t be any cancellation amongst when I just multiply the coefficients of the highest powers in the two factors.
OK. So that’s one way of proving the unit conjecture for this group. Really, always we have to prove the unit conjecture, just sort of generalizing this idea in some way. We’ll get to that at the very end.
These conjectures come in a family, and they’re actually related to each other. So the unit conjecture, if it holds for a given group and given field, then implies the zero divisor conjecture also holds, and that then implies the idempotent conjecture.
The first implication, the unit conjecture implying the zero divisor conjecture, is a fairly long proof, and it took a while before people realized that that’s actually the case. But I guess, it’s a long proof, but it’s not like a deep result.
The fact that the zero divisor conjecture implies the idempotent conjecture is essentially completely trivial. If I have a non-trivial idempotent, then it itself is just a zero divisor by factorizing the equation we wrote before.
So turning x squared equals x into x times (x - 1) equals 0.
So those are the relations between the conjectures of Kaplansky. They also relate to other conjectures which are very different in flavor from the Kaplansky conjectures in the sense that these Kaplansky conjectures are things which are very easy to state. I hope you understand exactly what they are, what they’re saying. We have some sophisticated conjectures from other parts of maths which imply the Kaplansky conjectures.
If the other conjecture is true for your group, then the corresponding Kaplansky conjecture is true. And I won’t attempt to really tell you what those other things are. But maybe for some people, they’re familiar names.
There’s this t conjecture from global analysis on integrality of L2-Betti numbers, and we have some famous isomorphism conjectures in k-theory. One is the Baum-Connes conjecture, and another one is the Farrell-Jones conjecture. If those are true, then it’d say at least over the complex numbers, the corresponding Kaplansky conjecture is true as well.
OK. So I told you about three conjectures of Kaplansky. There’s actually a bonus fourth one that I’ll now introduce, which is the direct finiteness conjecture. This is different from the other three because we now drop this assumption about the group being torsion-free. This should just be a statement that’s true for all groups.
Generally, we should be suspicious of such statements, but this problem has resisted all attempts so far. It says whenever I take a group ring K[G], then it’s directly finite, which is a sort of funny word that just means everything that’s left invertible in that ring is also right invertible. So if xy equals 1, then yx equals 1.
What does this have to do with finiteness? Well, for example, finite sets are exactly the sets where invertible self-maps—or sorry, injective self-maps—are also surjective and vice versa. This property is true, say, for the ring of endomorphisms of a finite dimensional vector space and characterizes finite dimensional vector spaces amongst vector spaces.
And if my group can, in some sense, be approximated by finite groups, then as a consequence of that, we get that the group ring is strictly finite. The broadest idea of a group being approximated by finite groups we have is something called sofic, which was introduced by Gromov.
I won’t try and tell you what that is, but it’s just saying in some very flexible sense, we can approximate what happens in that group with finite permutation groups. If a group is sofic, then the group ring is directly finite. So that last downward arrow doesn’t require knowing anything about whether it’s torsion or not.
OK. So those conjectures are all things which are still open on the left for all torsion-free groups, on the right for all groups. We don’t know any example of a group that’s non-sofic. So I think of sofic as a real Goldilocks property. It’s strong enough that it has consequences like direct finiteness, but it’s weak enough that no one can show that non-sofic groups exist.
And I think it’s a sort of analytically defined thing in a way. It’s difficult to put your hands on. But if you could show a group ring is not directly finite, then you’d have some very concrete way of proving the group is non-sofic. So that’s why I think this is a very attractive line of attack on that.
Yes.
AUDIENCE: Sorry, what is sofic again?
GILES GARDAM: So it’s a big generalization of other notions of being approximated by finite groups. So for example, if a group is residually finite, if every non-trivial element is also non-trivial in some finite quotient of the group. This is a much more general thing where I’m asking for approximations, where I’m allowed some epsilon of error in what should be a group homomorphism.
There’s now some error and some sort of, say, things that should be equal or only approximately equal. as permutations.
Is there another question?
AUDIENCE: “Is that related to approximate groups?”
GILES GARDAM: Not really. No.
That’s about closure of things which are approximating subgroups in a bigger thing.
OK.
So those are the conjectures. Something that maybe sticks out is that there’s no big sophisticated conjecture that, if it were true, would imply the unit conjecture.
And we now know there’s very good reason that there’s no big, fancy machine we can use to prove the unit conjecture.
And that’s because the unit conjecture is false. It’s also false for very nice groups. So this is my theorem from four years ago.
And I’m including the full theorem statement here, just to emphasize this is completely explicit and concrete. I’m not expecting that by reading these exact expressions, you’ll gain any sort of insight.
So the theorem says there’s this torsion-free group that I’m going to call p. And I can present it in this way.
And there’s other ways of thinking about this group. For example, this group of matrices or a group of transformations of three-space.
And then I define a bunch of things in terms of the generators of the group, write down this expression.
So this p + qa + rb + sab.
That’s just some element of the group ring. And it’s the sum of 21 elements from the group. And it is a non-trivial unit.
Its inverse also is supported on 21 elements. So this is some very surprising, complicated element of the group ring that turns out to be invertible.
And this is the first example we have of a torsion-free group where such things exist. The unit conjecture is false. And this is the first counterexample.
So this theorem gets the— ah, sorry. AUDIENCE: “How did you find it?”
GILES GARDAM: SAT solver.
[LAUGHTER]
AUDIENCE: “That’s funny, yeah.”
GILES GARDAM: Yeah. That’s fine.
Yeah, so all right, this theorem gets a party popper emoji because it’s been verified in Lean.
So Gadgil and Tadipatri did this in ‘22, and the paper appeared in ‘24. And I think some other people also verified this in Lean.
But I don’t believe these other verifications were published. OK.
So a few other observations about this theorem. This group p is incredibly tame. I mean, this was in every sense the easiest group for which this conjecture could have possibly failed.
And it was like on the Wikipedia page for this conjecture, there’s this three-dimensional crystallographic group for which the conjecture is open.
And that’s this group. So it has an index for subgroup. So up to very small-bounded error, if you like, it’s just z cubed, the three abelian group on three generators.
So it’s very close to being as easy and well-behaved mild as infinite groups possibly can be. There’s just a small little twist.
And because of that, it satisfies all of the other conjectures that I wrote on the previous page, but not the unit conjecture. OK.
So maybe that suggests a unit conjecture is very different from the others. I’d argue there are some ways in which the connection between the unit conjecture and the other ones is a bit tighter than it maybe seems.
If you’re interested in that, then come talk to me afterwards. OK.
And, of course, the one thing you might not like about the theorem is that it’s over the field with two elements. Maybe that seems like cheating.
So shortly afterwards, someone called Alan Murray could actually generalize this in a clever way to make it work for overall positive characteristic fields.
And then in ‘23, I was able to show, in fact, It actually works over the complex numbers. This works in characteristic zero. And so in a way, this is sort of a uniform counterexample that works everywhere.
OK. So how do we solve this problem? We need to talk about equations. And what are the equations we need to talk about? So all elements of the group ring have finite support, right? That is, finite formal sums. Everything’s supported at finitely many group elements. So if I’m given two finite sets A and B in my group, I could then say, well, do those sets support a non-trivial unit?
So I could ask for solutions to the equation xy equals 1, where x and y are elements of the group ring whose support is contained in those sets A and B. And now, if I’m asking for this, then in turn, we think back to what the group ring arithmetic is. This is just saying I’ve now got the size of A plus size of B, many variables, and I’m solving a system of product of those two sets, many equations.
OK. So maybe technically if the trivial element of the group is not one of these products, there’s an extra equation. But that extra equation is then just 0 equals 1. So let’s not worry about that.
For example, if I take the integers again and I’m asking—so my sets A and B are both going to be the set {0}, which in multiplicative notation is 1, t, t^2. I’m now just asking to find these two polynomials that multiply to give 1, because we know those things don’t exist. But I just want to illustrate an example: What are the equations we get? I just get this system of equations.
So the second last one is saying the coefficient of t^3 has to be 0 in the product. OK. So when I found my support, I now just have some system of polynomial equations to solve. And that’s something we can do. So sort of an immediate observation that falls out of this is that this problem is co-semidecidable or being a counterexample is semidecidable, if you prefer.
If I’m given a torsion-free group, I need an Oracle for its word problem. Otherwise, I can’t do anything. But if I have the solution to the word problem, then that group being a counterexample is something that is semidecidable. So I can just run an algorithm which will produce non-trivial units if they exist. OK.
So here, I’m phrasing this in the sense that I’m asking a question about the group. And then I’m allowed to pick any field I want. So I guess the thing we have to convince ourselves is that it doesn’t matter that there’s somehow infinitely many fields and many fields are crazy. The key point is just that the Nullstellensatz is basically telling me I can tell whether this solution in some algebraically closed field of a given characteristic just by talking about the ideal that the equations generate.
In particular, if there’s any characteristic p field, allowing also p equals 0, for which we have a non-trivial unit, then it also works for your favorite algebraically closed field of characteristic k. And that’s something we can decide. So if characteristic p.
A small observation, it’s not really important. But we also can just assume that the field has positive characteristic if we like. So if the solution is in characteristic zero, there’s also in positive characteristic. OK.
And so why is it co-semidecidable? Well, I can just exhaust my group by finite candidate support sets. I’ve called them B1, B2, and so on, because a natural way of picking this exhaustion is to take metric balls in the Cayley graph. In other words, for increasing values of some radius r, I consider all elements of the group that are a product of at most r generators and their inverses. In z squared, these balls will be diamond shapes with raggedy edges in the two-dimensional grid. So I’m exhausting the group by these finite sets.
Then I enumerate all pairs of a prime number p and one of these balls. For each of those, I’m left with a polynomial system of equations to solve. I can do that with a Gröbner basis computation, which decides whether the ideal generated by the equations is a proper ideal of the polynomial ring. We’re only interested in non-trivial units, so we need to remove the trivial solutions. There are various ways to do that; it’s not hard, so I’ll just leave it at that.
If you don’t like the fact that we’re talking about Gröbner basis computations, alternatively, you can appeal to the fact that if there is a solution, then there’ll be a solution where the coefficients are in some finite field. So instead of enumerating primes, you can enumerate all finite fields and check by exhaustive enumeration whether there’s a solution to that system.
This is all good and well. Theoretically, if I have access to a group with a solvable word problem and it’s torsion-free, then if it is a counterexample, I can just run this naive algorithm that will eventually produce it. But that’s very far from being able to do in practice. When theory meets practice, we need to solve a system with approximately 200 variables and 600 equations. These are different from polynomial systems people generally study—they’re incredibly overdetermined, with way more equations than variables. It’s like quadratic equations in some sense, but there’s certainly a lot more equations than variables.
Gröbner basis computation is worst-case doubly exponential. Maybe in practice for this problem it behaves more like singly exponential, but with 200 variables, it’s hopeless to approach this with Gröbner basis computation.
At this point, instead of trying to do this theoretical thing where we dovetail through all finite balls and all primes, let’s just stick to talking about F2, the field with two elements. Thinking about this polynomial system, deciding the solvability of that system, given the partial multiplication table for the finite ball, is obviously in NP. Given this finite bit of data that specifies a system of equations, if there’s a solution over F2, I can just substitute it in and verify it. So this is a problem in NP.
It’s a tautology to say I can try to solve this problem by reducing it to my favorite NP-complete problem, but I actually can do this by reducing it to SAT. You can reduce this to SAT in order to solve the system of equations.
I’m not a SAT expert, but I’ll quickly say what SAT is for people who aren’t familiar: Boolean satisfiability, known as SAT. This was the first NP-complete problem—Cook and Levin showed in the early ’70s independently that it is NP-complete. Before this proof, there was no a priori reason why NP-complete problems should exist. SAT asks, given a Boolean formula in propositional logic, can you assign the variables to true or false so that the formula evaluates to true (i.e., is satisfiable)?
SAT solvers generally expect the formula in conjunctive normal form (CNF), which is a big AND of ORs. For example, a CNF expression might have three clauses taken as an AND: the first clause says x or NOT y (so either x is true or y is false), and similarly for the other two. Given a formula in another form, we can transform it to CNF by introducing auxiliary variables in a mechanical process called the SATAND transformation. At the end of the day, the solver expects CNF, and I’ll talk a bit about how we do this exactly.
I said the problem is in NP, so I can reduce it to my favorite NP-complete problem. The first thing is, we’re just talking about solving equations over the field with two elements. I can very naturally translate the field with two elements into Boolean logic: 0 is false, 1 is true, addition is exclusive OR, multiplication is AND. So it’s very natural to translate the system of equations into a Boolean formula, and then put it in CNF.
Let’s see exactly what this looks like in a specific case. Suppose I’m looking for a solution to the equation xy = 1, where x and y are group ring elements supported on a ball Bi. If Bi has n elements, I’ve got 2n variables—defining the coefficients of those n group elements for x and y.
I need to assert that the solution is a non-trivial unit. There are exactly n trivial units supported here, so we need to say that at least two of the variables are non-zero. A convenient way to do this and break some symmetry is to impose that the coefficient of the trivial element is non-zero, and then require that one of the other coefficients is also non-zero. Up to translating in the group (which doesn’t change whether there’s a solution, though it may change the smallest ball the solution is supported on), I can easily assert non-triviality by adding these two clauses.
Now I need to say that these two elements multiply to give 1 in the group ring. To avoid an incredibly huge formula, I first introduce n squared auxiliary variables, say xg, h. Each encodes the product in F2, which is just AND in Boolean logic. I can impose that xp, h is exactly ag AND bh by adding three clauses.
So in conjunctive normal form, I add the three clauses, which are on the first line. But maybe the way to think of it is that it’s saying if the AND is true, so if x is true, that implies a is true, x is true, implies b being true. And conversely, if those things are both true, they imply x.
OK, so now I’ve introduced my variables to store the products of all n squared pairs. And now I just need to assert that if I add up these things in the right way, I always get the right answer.
And so these xg, h variables are partitioned according to what the corresponding product of g and h is in the group. And I’ve just got to impose those equations. So now I actually have to– the xg, h are the things in the quadratic equations.
Now we need to assert the quadratic equations. And so each of them is of the form saying if I sum over all pairs that multiply to give k, then I get this Kronecker delta. So I have to get 0 everywhere except for when k is the trivial element of the group 1.
And in general, I guess I’d need something of exponential size if I didn’t introduce auxiliary variables. So I’m going to introduce some more variables in order to break this potentially big sum up into a smaller sum.
So I guess one of these things would be, say, size n. There’ll be a bunch of size close to n. So certainly, we want to break this up. And then if you like, these auxiliary variables could be, say, storing like the result of some partial sub-sum.
And then I get a bunch of equations that I now need to impose, which are all quite short, and some have say three or four things. And each of them I can then assert exhaustively.
So, for example, if I wanted to say that x plus y plus z is 0 or so the exclusive or of those three things should be false, I can do that by adding these four clauses.
AUDIENCE: Yeah.
GILES GARDAM: And so thinking maybe more mathematically, I’m talking about this three-dimensional vector space over F2. There’s eight elements there. And there’s this codimension one subspace, which is the solutions I want. And I’m just going along and saying there are four things which are not solutions.
And for each of them, I’m going to band them. So the first thing is the same thing as saying, I’m not allowed to take 1, 1, 1 in F2 terms, or I’m not allowed to take true, true, true in terms of Boolean logic.
OK. And that’s all there is to it. This is now a conjunctive normal form expression that tells us whether or not we have a non-trivial unit supported on those things with a non-trivial coefficient of the identity.
AUDIENCE: So where do multiplication tables come in?
GILES GARDAM: So the multiplication table comes in here, where I’m summing up the product variables x,g,h according to what the corresponding product is. So if you like, for each k, then look in this multiplication table where all the places that k occurs, and that tells me which xg,h variables I have to add on.
Yeah, thanks.
AUDIENCE: [INAUDIBLE]
GILES GARDAM: Right. So the most natural, for me, way of doing this is just to take for increasing, say, for increasing values of i, all elements of the group that I can write as a product of at most i copies of the generators and the inverses.
So in this case a, b, a inverse, b inverse. Yeah. So I guess having a more intelligent way of picking them could drastically improve how quickly you can solve this problem. But despite thinking about it quite a lot, I don’t really have drastically better ideas than just taking this naive exhaustion of the group by finite subsets.
OK. So that’s all very well. It worked out. I found this non-trivial unit and got a nice paper. But why did this work? So let’s talk a little bit about hindsight.
Right, so it’s something that is maybe solvable in minutes or hours depending on exactly how you set it up. So it’s not super easy for the SAT solver, but it’s also not super hard. There’s a question.
AUDIENCE: [INAUDIBLE]
GILES GARDAM: Yeah.
AUDIENCE: [INAUDIBLE] point are we using the oracle for the word problem?
GILES GARDAM: Right. In order to be able to say, for example, “What are all the pairs that multiply to give k?” And in fact, even to enumerate these sets Bi, I really need to be solving the word problem. If I’m enumerating all these products, I need to know which of those products are equal to each other.
So yeah, implicitly already when I’m talking about these balls, yeah.
AUDIENCE: So you need to also implement that somehow.
Or maybe we didn’t get to that point yet.
GILES GARDAM: No. I mean, I’ve already sort of asked my oracle, “What is the ball of radius—” in fact, I’m asking for 2 times the radius of the set B because I now want to talk about all products of things in B.
AUDIENCE: I mean, in practice you actually solved and found some specific examples. So you must have somehow coded it up.
GILES GARDAM: Yeah.
AUDIENCE: [INAUDIBLE]
GILES GARDAM: Yeah. And so for this group, it’s so easy. There’s a bunch of different ways you could solve the word problem. For example, you could use its polycyclic structure. You could implement it as a group of matrices. It has an automatic structure. So yeah, there are various different ways of solving the word problem to this group.
AUDIENCE: How did you decide on that particular crystallographic?
GILES GARDAM: It really is the easiest one for which the conjecture could have possibly failed. So in terms of torsion-free crystallographic groups in dimension 2, there’s just Z² and the fundamental group of the Klein bottle.
And in dimension 3, I mean, in every dimension, there’s a finite list. In dimension 3, this is the only one for which the conjecture is not easily seen to be true. So in mathematical terms, that’s because this is a unique three-dimensional crystallographic group, torsion-free, and has first Betti number 0. Or in other words, its abelianization is finite.
OK. So why is this something that worked? And this is really just speculation. I think understanding why SAT problems are hard or easy is very difficult. And I guess if you could really understand why SAT problems are hard or difficult, you’d basically have solved P versus NP. So this is really just wild speculation.
Why did this work? So I think a key point is that this is a very natural encoding. The SAT problem is very close to the original problem domain, talking about these equations over F2.
But maybe that’s still a bit of a cop-out because solving these equations is still—solving quadratic equations of F2 is also an NP-complete problem. I could have gone the other way and taken my favorite subproblem and reduced it to something about polynomial equations.
OK, that’s probably a bad idea. But yeah, I think it’s still important that the problem I end up with is a very natural reflection of the thing that I’m actually interested in. And something that… is important, but is.
Again, in context of this reduction of SAT to this problem, is maybe also a cop-out. Many equations are very short. So some of these equations, I’m adding up lots of things and that may be difficult to manage. But some of them are quite short. Maybe I’m only summing up two or three things.
And this means the SAT solver can very quickly learn, OK, these things were non-zero. So if those variables were true, that would force some other things to be true. And this sort of information propagates around and maybe quickly lead to a contradiction.
So we backtrack or maybe quickly take us towards the solution. So maybe more so than the first two things, the third point is really the key thing. This problem has a very combinatorial flavor. And that’s why this specific set of equations is something that we can really solve. Even if solving quadratic equations in general over F2 is NP-complete.
And by combinatorial, I guess, I’ll come to that in a little bit. But it’s to do with the structure of which variables occur and which equations. And there’s sort of a combinatorial problem that’s related to this problem, which itself is quite difficult to solve.
And solving that problem is quite close to solving this thing. So I guess this is a system of equations, which has, in a way, more combinatorial flavor than just a purely algebraic flavor. And if we compare it to things like Gröbner bases, those algorithms are essentially manipulating the equations; they’re doing some sort of souped-up version of mixing Gaussian elimination and polynomial division, if you like.
And these involve producing very large derived equations. And these sort of intermediate things can be very huge. And that makes solving things by Gröbner basis computation difficult. The SAT solver is not so much reasoning about equations as about the solutions. This is a bit of a lie because of course, that’s always for those familiar with them, a learning clauses as they go along.
But I think this is a key point that we’re really trying to understand what a solution over F2 looks like, rather than reason with the equations in order to say something about all characteristic two fields at once. And finally, the last point, the SAT solver doesn’t really care about how big the solution is. So it’s, again, a bit of a lie.
It’s probably easy to find solutions that have small support. But the key thing is the fact that this set has size 21 is not really relevant, whereas other approaches to try and construct these counterexamples that involve some sort of combinatorial enumeration are just doomed to fail. Because as far as I know, this 21 by 21 solution is the smallest there is.
And the number of possibilities you have for drawing up this 21 by 21 multiplication table and pairing things up is just astronomical. So it’s sort of 21 is too big for other approaches of doing this, but the SAT solver doesn’t really care if the support is size 10, 20, 40, and so on.
OK. That’s a little bit of speculation about why this worked now. But of course, we should keep in mind that SAT solvers seem very magical, but they’re not magic bullets. We can, of course, reduce this polynomial system is, of course, also NP-complete.
And also in a way, we are just factorizing. And of course, you could also take integer factorization and turn it into a SAT problem. And then you shouldn’t expect that suddenly you can factor 100-bit, 200-bit integers using a SAT solver in a matter of minutes. But this thing has this combinatorial flavor. That means we can solve this problem in a reasonable amount of time.
OK, so a little bit more about that combinatorial property. This is the one weird trick that lets you prove the unit conjecture. It’s one of these definitions, which is sort of a bespoke definition designed just to do exactly one thing: to prove this conjecture. It generalizes all previous arguments that people had to prove the conjecture for different groups.
So, a group has the unique product property if, whenever I take two non-empty finite subsets, there’s some element of the group which can be written as a product of things from those two sets in exactly one way—a unique product. It’s a short definition, but I know it’s something that’s always very difficult to parse the first time you see it.
The first observation is that this is only interesting for torsion-free groups. If my group has a non-trivial finite subgroup H, then I let these finite subsets A and B both be the subgroup H, and then every product will occur exactly size of H many times. So this is something that can only be interesting for torsion-free groups.
If you have this property, then, for example, this immediately gives you the zero divisor conjecture in the same way that we’re thinking about why the ring of polynomials satisfies the conjectures by zeroing in on the highest power and the lowest power. If I multiply two non-zero things, then I apply the unique product property to the support sets, and this tells me there’ll be some u whose coefficient is just this product of two things. There’s no addition involved, no possibility for cancellation. So I know if I multiply two non-zero things, I can find some spot where the support—the coefficient—is non-zero. So the product can’t be zero.
In fact, there’s a very nice little argument of Strojnowski saying you always get a second unique product for free, unless both sets are size 1, of course. So you get the more strong unit conjecture as well.
Overcoming this unique product property is already a large part of the challenge of producing non-trivial units, and so on. This is a very combinatorially flavored thing. There are very few groups known that provably don’t have this property and are torsion-free. This is the reason why the group that I used was such a natural thing—it was shown in ‘88 to not have this property. The question of whether it did or didn’t had been around for about 15 years. That was shortly after Ripps and Segev gave the first examples at all of groups that are torsion-free and don’t have this property. That was a very complicated argument using small cancellation theory.
In the end, it turns out there’s actually this very nice group that doesn’t have this property, but there’s still a real shortage of examples. The shortage is such that we don’t know any examples which are really manageable—in a sense, you can actually just write them down, implement them in a computer, and try and generate these equations. All the ones that don’t have this property are known to satisfy the zero divisor conjecture. So if we wanted to, say, make progress on other Kaplansky conjectures, it seems like we’re stuck a bit.
But of course, this unique product property is also something I can try and disprove using SAT. I could take one group which has lots of good theoretical reasons to be interested in and show that this group—I’m just putting it in this presentation to have some way of fitting it on the slide. It’s maybe not the best way to think about the group. But anyway, this group exists. It’s not known to satisfy the zero divisor conjecture, and it doesn’t have the unique product property.
But now these groups, which possibly are candidates for the zero divisor conjecture, are much more complicated than this crystallographic group. And here, you’re inevitably talking about a SAT problem with millions of variables.
So yeah, that’s always super impressive. And even, obviously, this is not a very hard problem relative to the number of variables. But in a matter of hours, you can solve this problem despite the fact that you’re talking about millions of things.
OK. So for people from this pre-processing, it is something like failed literal probing, but we do this at the level of the combinatorial problem before we turn it into SAT and have some slightly more sophisticated reasoning, I guess.
And the pre-processing looks like this. So a black pixel tells me that I in advance some product can’t occur in my counterexample. So I can somehow remove roughly a third of the problem in advance.
OK. So just to finish on some final thoughts, I think there’s certainly more to do with the Kaplansky conjectures. Certainly a lot harder than disproving the unit conjecture, but I think there are things that can be done.
SAT solvers are a powerful tool that cut through superficial difficulty. And this problem of finding the non-trivial unit looks very hard. We’re basically needing to enumerate not what we would naively think is a search space of size 2 to the 100, roughly speaking, but the SAT solver through the fact that this difficulty is only superficial.
And finally, SAT solving is fun. It can be a challenge to take your problem, which you sort of know in theory should be solvable with a SAT solver and actually produce the conjunctive normal form expression in a good way. But it’s always a fun challenge. And so I encourage you to go forth and solve.
[APPLAUSE]
MODERATOR: Are there any questions?
AUDIENCE: [INAUDIBLE]
AUDIENCE: Yeah. Can you take the unique product property has to fail? In your counterexample, are there group elements which can be written as product of many things? Because you also said that most equations are short.
GILES GARDAM: Sorry, could you repeat the last bit of the question?
AUDIENCE: Are there some group elements which can be written as a product of many things so that you get some non-trivial cancellations? Some equation is kind of long. You said many equations are short, but presumably, some equation is quite long then–
GILES GARDAM: Right. So if I just start with the system of equations on this whole set of size 100 or so, then there’ll be some equations which are length 100. For example, evaluating the coefficient of the identity.
Maybe I can ignore that equation, but then there’ll be other ones which are quite long. And when I take the counterexample at the end, these 221 element sets, then the identity occurs 17 times, for whatever reason. The other things that will occur in even number of times.
And I guess a bunch occur exactly twice, four times, maybe up to 8 or 10 or something like that. Does that sort of answer your question?
AUDIENCE: Yeah.
AUDIENCE: [INAUDIBLE]
AUDIENCE: So I have two questions, actually. The first one, I showed you [? UCDCL. ?]
GILES GARDAM: Yeah.
AUDIENCE: Did you also consider local search?
GILES GARDAM: Not in any sort of targeted way.
AUDIENCE: Because in these kinds of examples, that local search can also be extremely effective.
GILES GARDAM: OK.
AUDIENCE: [INAUDIBLE] GILES GARDAM: OK.
AUDIENCE: And the second question I have is so looking back, what could have the communities, the SAT community have done to make your life easier? [Laughter]
GILES GARDAM: That is a question I’ve never been asked before. [Laughter] And a very good question. I feel like in a way I don’t have anything to ask of you. I think the solver was there. The problem was doable in a matter of minutes. I mean, the first time I did this, I was using C3 to simplify the formulation. Since then, I’ve mostly sort of generated the formulas by hand.
Yeah. I guess for other mathematicians, maybe it’d be nice to have tools which are a bit more comfortable to use from inside their existing computer algebra systems. But for me now, I guess I’m not super keen on having such things just because I’ve got by without them.
MODERATOR: Yeah. AUDIENCE: Following up on Ryan’s question, do you use [? Catacomb ?] for this or which particular solver did you use?
GILES GARDAM: So I’ve used various different solvers. I used [INAUDIBLE] Mini SAT for a while because I thought it’s trying to treat exclusive OR or some sort of natural thing. But I think in the end, it didn’t really have any performance benefits over other things. I also used Ling [? a ?] Ling and [? Fling ?] a Ling quite a bit.
AUDIENCE: So you were competing counterexamples. Or what did you say?
GILES GARDAM: Yes.
AUDIENCE: I think the very last one, there was a proof as well.
GILES GARDAM: Well, so I called this a theorem. But this is just saying there exists two sets. One, say, size 24, one, size 28. I think is one example that showed that this thing doesn’t have the property. So it’s, yeah, I guess phrased as a theorem, but it’s morally more like a counterexample.
Yeah.
AUDIENCE: So you could have used some computer algebra systems to help encode your problem more efficiently, sort of plugged into the SAT solver programmatically. This is an answer to Ryan’s question. And there are ways in which you can integrate the domain knowledge into the solver. So your encoding is more efficient, but the solving process can also be significantly more efficient.
AUDIENCE: OK. [Interposing voices]
GILES GARDAM: I’m very interested to talk about that.
AUDIENCE: –some place you had an n squared blowup in the size of your network. Right?
GILES GARDAM: Yeah.
AUDIENCE: Those kind of situations, you can combine the SATs all over. Right?
GILES GARDAM: OK. I’d be very interested to talk more about that.
AUDIENCE: I think it’s a more general question about the history of the unique product property. When he first came up with it, what paper was it in?
GILES GARDAM: Yeah, so I think–
AUDIENCE: For example, [INAUDIBLE] did some stuff, but was it working in one of his papers, or is it–
GILES GARDAM: I’m not sure about that. I mean, the first reference I have is a paper of Burns and Hale. And they were talking about orderable groups in a paper from ‘72. I think maybe it’s sort of used without giving it a name in some other paper from earlier, but I can’t remember the authors. I think probably [? Hickman ?] himself in 1940, who proved the first two conjectures for a class of groups probably maybe had that definition lurking in his mind as well.
Yeah.
AUDIENCE: OK. AUDIENCE: [INAUDIBLE] MODERATOR: Yeah. AUDIENCE: There’s a question about minimality of the example [INAUDIBLE]. I think the slide 9 or something like that [INAUDIBLE].
Yeah, exactly that one. GILES GARDAM: Yeah.
AUDIENCE: In my experience, when you use a SAT solver, there’s almost a suggestion that when you find a counterexample, this might be a minimality there. This is perhaps the most compact or the smallest. Is there also some interest in that?
GILES GARDAM: Yeah. Actually, proving this is minimal is, I think, probably completely beyond what we can do at the moment. But certainly, I believe that it’s minimal, at least for this group. And there’s another group that I have non-trivial units for. And they’re bigger. I guess at some point I took a slightly larger ball and then exhaustively found all solutions there using the SAT solver. And this was the smallest one. Yeah, I have reason to believe that this is the smallest one. But I think actually proving that probably requires going down this line of exhaustive combinatorial enumeration. I think you can do that maybe for things of size 7, but not 21.
AUDIENCE: [INAUDIBLE] thanks. [INAUDIBLE] I was wondering about the [INAUDIBLE] conjecture, [INAUDIBLE] because it would be incredibly surprising that the Farrell-Jones conjecture was not true. So, I mean, I think people really believe in this. And here you kind of have to put it to the example [INAUDIBLE]. I even saw that there was a Wikipedia, but that was like people didn’t know about it.
GILES GARDAM: Yeah.
AUDIENCE: But we don’t really have potential counterexamples to [INAUDIBLE] Farrell-Jones. So I guess it’s a couple of questions. How would one start to look for potential counterexamples? And then have you ever thought about how the [INAUDIBLE] content should be phrased [INAUDIBLE]?
GILES GARDAM: Yeah. So I think really, you can just phrase it in a very similar way. But it’s certainly very hard. I mentioned that we have a lot less groups which are candidates for the zero divisor conjecture and then even less for the idempotent conjecture. I mean, yeah, together, Bauman and Farrell-Jones are known for a really large class of groups, but there still are groups which are open. And it’s, I guess, also conceivable that the idempotent conjecture is just true over the complex numbers, but false in positive characteristic.
Something I didn’t mention is that the direct finiteness conjecture is just true in full generality if the field k has characteristic zero. There’s an analytic argument for that due to Kaplansky.
MODERATOR: Yeah.
AUDIENCE: Yeah, so I guess maybe this is related to the last comment you made. In this case, you’re saying the idempotent conjecture is when k is equal to the complex numbers or the Atiyah conjecture? So in what sense does that specialize? Because a lot of the examples you were doing was when you had k is equal to F2. Can you explain how the arrow [INAUDIBLE]?
GILES GARDAM: Yeah, so [INAUDIBLE] and Atiyah are inherently analytic things which are defined involving complex numbers. It really only makes sense to try and prove this arrow in that direction. For Farrell-Jones, I also added this constraint just because it avoids some technicality that has to do with the sofic question.
AUDIENCE: But if you’re specializing, k could be equal to the complexities, how do you recover F2?
GILES GARDAM: Sorry, so each of these arrows is for a fixed k and a fixed g. If I also know that k is the complex numbers, then I get that.
AUDIENCE: [INAUDIBLE]
GILES GARDAM: Yeah. Yeah, so maybe there are counterexamples to the zero divisor for which Atiyah is true. But actually, a lot of the groups, which we know Atiyah is true. Actually, we know the zero divisor conjecture is true regardless of the characteristic.
MODERATOR: OK, I think we’re out of time for questions, but let’s quote once again.
[APPLAUSE]
[INAUDIBLE] thank you.
[INTERPOSING VOICES]