Our great sponsors
-
Performant, definitely. I think people see SAT and assume it must take exponential time on everything but you'd really be surprised at the size of the problems modern SMT solvers can churn through. Not really so consistent but that comes with the territory - you might run into performance "cliffs" where minor changes to your formula leads to big, big changes in runtime. Charting out the limits of the solver for your problem is part of the dev process for these projects. Here is an example of a performance cliff I encountered on this project, for example. Thankfully Nikolaj and the rest of the Z3 team is quite responsive, so if it's an easy fix it will probably be done quickly.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.