cr1901

William D. Jones

@cr1901

Yes, I still use the same hard disk platter as a drink coaster. But I need more ISA cards in my collection.

log in
cr1901
@cr1901

New Blog Post: "Using `z3` To Solve Logic Puzzles"

After 3.5 years (!!), I am proud to announce that I've written a new blog post on my site:

"Using z3 To Solve Logic Puzzles"

Cohost is for short-to-medium form writing, as well as being a nice staging area for stuff to go my website. On the other hand, my blog is for longer-form writing, and this particular post went straight to my website instead.

z3 is an SMT solver. An SMT solver is a type software which is optimized for solving SMT/SAT problems. This post also serves as a whirlwind introduction to SAT and SMT problems. So if you've heard about any of those things, but don't know how they work, give my post a read!

I hope you all enjoy, and would love to hear feedback:

You must log in to comment.

in reply to @cr1901's post:

vogon
@vogon

hell yeah, I love this, logic puzzles seem like a legitimately great gateway into theorem proving

also thank you for the pointer to an online logic puzzle site, haven't done one of these in a while

login to reply
cr1901
@cr1901

hell yeah, I love this, logic puzzles seem like a legitimately great gateway into theorem proving

Tyvm :D! Indeed, even if this blog post doesn't do the numbers I'd like (because my communities are especially fragmented since Muskie took over), having written it does unlock other posts I want to write where I can safely assume SMT as a prerequisite.

I mostly use SAT/SMT for proving facts about HDL designs. "How can I represent the concept of time in HDL designs using SAT/SMT?" is probably my next post... whenever that is?

also thank you for the pointer to an online logic puzzle site, haven't done one of these in a while

Have fun! I am not responsible for any deadlines missed from solving logic puzzles :).

login to reply