Hackathon: Solver 100x speed 🚀

​$4k prize - 6-10pm, Wed 17-Feb, Stanford (TBD)

​Judged on solver speed, with bonus points for solving complex equations.

​A perfect SMT solver isn't magic—it's the ultimate code hack that transforms bugs and bottlenecks into well-formed, elegant solutions. However, since perfect solvers don't exist, we at atopile built our own.

​While software lives in an ideal world, the real world is fuzzy—you never have exact values, and tolerances always matter. Traditional CAS/SMT solvers struggle with this fuzziness, their performance degrading to O(N!). That's why we created our own solver for the atopile circuit board compiler. If you succeed in improving it, we'll include your work in the atopile compiler (MIT licensed).

​Resources:

• ​https://github.com/atopile/atopile/tree/main/src/faebryk/core/solver

• ​Z3 is Microsoft's SMT solver, used in compilers for typing

• ​https://smt.st/SAT_SMT_by_example.pdf (PDF/book) formal SMT solver docs