BASES HACKSPACE x ATOPILE: SMT-SOLVER HACKATHON

​Don't know what any of those words up above on the title mean? No worries, we'll teach you all about them at 6pm, before our hackathon starts!!

Dive into the worlds of SMT solvers & learn from mentors from Atopile - a YC-backed startup that makes tools to design electronics circuit boards with code. ​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!),and you'll have the opportunity to tackle this problem head-on.

This light hackathon sprint will enable you to sharpen and leverage skills you've learned from classes such as CS103 and more in order to sharpen technical skills that many don't know about, making you a strong coder (and logician) with exclusive & special skills. You'll be contributing to an open-source repository, and be judged on solver speed, with bonus points for solving complex equations.

More importantly, you'll have the opportunity to network with individuals from YC-backed startups & learn more about the world of hardware.

Or, just show up for the food & people!!

Rules and scoring: https://github.com/atopile/atopile/blob/temp/hackathon_solver/docs/hackathon/README.md

​Resources:

• ​Solver README: https://github.com/atopile/atopile/tree/temp/hackathon_solver/src/faebryk/core/solver

• ​Repo SetUp Instructions: https://docs.atopile.io/dev/guides/installation/

• ​​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

• ​https://www.youtube.com/watch?v=EacYNe7moSs&ab_channel=GuidedHacking (YouTube intro to SMT solvers)