Using SAT as a tool for hard polynomial systems

Solutions to equations in group algebras can be found by reduction to (a sequence of) polynomial systems over the field. In general, these systems are heavily overdetermined and if solutions exist, then many variables take the value zero. Modern solvers for Boolean satisfiability (SAT) can be an effective tool for tackling these systems, especially in characteristic 2. I will also explain how they can fit into a toolkit for solving such systems in characteristic 0.