Abstract
Decision problems about infinite groups are typically undecidable, but many are semidecidable if given an oracle for the word problem. One such problem is whether a group is a counterexample to the Kaplansky unit conjecture for group rings, a conjecture that was open for 80 years. I will present the mathematical context and content of the unit conjecture and explain how viewing the problem as an instance of the Boolean satisfiability problem (SAT) and applying SAT solvers shows that it is not just solvable in theory but also in practice.