How to *prove* you have the best design/match strategy

Have you ever wanted to know if your robot design was the best possible robot design? What about your match strategy?

Well, using Z3 (an open source theorem prover/SMT solver from Microsoft) and some code to say what best means and what’s possible, you can. In this paper, I show how you can find optimal robot designs and alliance strategies with examples from the 2019 FRC game.

using-z3-in-frc.pdf (724.5 KB)

Special thanks to @Brian_Maher for reviewing this and for the conversations that inspired this paper.


Very very nifty. This is an awesome share, I hadn’t heard of z3.

My “5 mintutes of research” take - the answers will (of course) be only as good as the estimates and assumptions going in.

Still, answering questions like “how long to build an intake that looks like X ?” is an easier question to answer than “Is X better?”. I see value from that perspective.

In terms of match strategy, my brain is already churning… especially if you had real-time match data from scouts or zebra (plus good segmentation) or something like that… I see great potential for a live tool that spits out concrete match strategies optimizing for different goals.



However, I think you can still get a lot of value if you just use Z3 as a constraint solver to verify that your subsystems satisfy robot rules (like not using too many PDP slots). I’ve had a few close calls when integrating things late in the build.

I actually think this is harder to some extent. It’s not clear to me how to best model time to location as a distribution instead of just a static number. My examples explicitly excluded defense (and implicitly excluded robots breaking) for this reason.

If you have any ideas on how to improve in this area, please reach out.

The original goal of this research was actually to combine the robot design and match strategy models, such that your robot design optimizer was maximizing points scored across an alliance.

One of Z3’s limitations is that it does not like working with exponential functions. Unfortunately, if you want to optimize the sprint distance to a particular location with FRC motors, physics gives you an exponential function to solve. I tried a few Taylor series approximations but the approximation error became high very quickly.

It also blows up the search space by a lot.