Socrates deemed writing a 'pharmakon,' a word that can simultaneously mean both a remedy and a poison.

Jev-in-the-Loop. Makes sense.

Sounds like the next shitty Vercel ad at re:Invent.

Hook it up to CRISPR.

Confirmed that when you interrupt it, it shuts up immediately. Ya know, like a tool that is useful instead of a friend that burns tokens for no reason.

I can just barely recommend it. The physics is great but for a 3 hour AMA it's about 51% politics and basketball.

In all honesty I think this is an unfair characterization. I've listened to his podcast for a fair number of years and I think you're exaggerating quite a bit.

Mostly the episodes are specific topics with a guest who's area of research/specialty is the topic and which stay pretty well on-topic.

Most of the AMA episodes are in the area's where Carroll specialize: physics and philosophy of science. It -occasionally- veers off into politics or basketball, but it's nowhere close to 51% politics and basketball. I think the most recent AMA did have more basketball than usual, and admittedly more than I like. And I am not a fan of his politics nor do I consider his political positions especially thoughtful or insightful. But those diversions are more occasional distractions than some majority of the AMA content. And in a 3+ hour Q&A format its not surprising that he's asked about those areas where his regular listeners know that he has a particular interest or position.

Ironically, this is trivial to build with LLMs.

You should take your ad viewing elsewhere in protest.

Yep. Straight to the pie hole.

I know nothing about z3 but it's from Microsoft. Would Google's OR-Tools component CP-SAT also be useful for something like this?

z3 is also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster. it is a great library that lets you solve pretty complicated DP problems with a few dozen lines of code.

Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.

In general that's true, but to reason about boolean circuits like in this challenge we only need a SAT solver. Z3 is just used for it's convenient API.