Accidentally writing a SAT solver
blog.danielh.cc
Accidentally writing a SAT solver
1–10 of 41 posts
Re: Accidentally writing a SAT solver
#2On a related note, anyone have any advice for getting started with something like Z3?
Re: Accidentally writing a SAT solver
#3Interesting post, but I’m not sure this really speaks to what goes into actually writing what would be considered a “fast” SAT solver. It seems more like a post about how SAT pops up in a lot of places if you look at them right. For the state of the art in what constitutes fast solvers, the annual SAT competition papers are quite interesting to read if you’re interested in the techniques people come up with to make them fast. A few years ago I was working through Knuth’s satisfiability book and writing my own solvers, and was always amazed how stunningly fast the SAT competition winners were compared to the ones I’d code up.
Re: Accidentally writing a SAT solver
#4On a related note, anyone have any advice for getting started with something like Z3?
Read up on smt-lib: learning how to encode problems in that is a good way to start. The Python z3 bindings are a good starting point to play with it too.
Re: Accidentally writing a SAT solver
#5On a related note, anyone have any advice for getting started with something like Z3?
https://theory.stanford.edu/~nikolaj/programmingz3.html - This one was useful for me to get started with it a while ago.
Re: Accidentally writing a SAT solver
#6I really like the styling of this blog. It's nice on the eyes, gets out of the way, and the collapsed containers for extra info is a nice touch. There's a bit of layout shift though, but that's about it.
Re: Accidentally writing a SAT solver
#7On a related note, anyone have any advice for getting started with something like Z3?
Re: Accidentally writing a SAT solver
#8I really like the styling of this blog. It's nice on the eyes, gets out of the way, and the collapsed containers for extra info is a nice touch. There's a bit of layout shift though, but that's about it.
I'm on mobile too, I disabled JS in my browser to test it out, the site loads fine and the expanding boxes work too (I think it's the tag).
Re: Accidentally writing a SAT solver
#9[stub for offtopicness]
Backtracking is not a fast SAT solver.
Re: Accidentally writing a SAT solver
#10Interesting post, but I’m not sure this really speaks to what goes into actually writing what would be considered a “fast” SAT solver. It seems more like a post about how SAT pops up in a lot of places if you look at them right. For the state of the art in what constitutes fast solvers, the annual SAT competition papers are quite interesting to read if you’re interested in the techniques people come up with to make t…
SAT turns up everywhere because it's almost universal kind of problem. Since it is NP complete, everything in NP can be transformed into an instance of SAT. Since P is a subset of NP, everything in P can be also be turned into an instance of SAT. Nobody knows if things in PSPACE can be, though.