[HN Gopher] Accidentally writing a fast SAT solver
       ___________________________________________________________________
        
       Accidentally writing a fast SAT solver
        
       Author : max__dev
       Score  : 39 points
       Date   : 2024-11-28 00:18 UTC (7 days ago)
        
 (HTM) web link (blog.danielh.cc)
 (TXT) w3m dump (blog.danielh.cc)
        
       | anonymousDan wrote:
       | On a related note, anyone have any advice for getting started
       | with something like Z3?
        
         | porcoda wrote:
         | 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.
        
         | Jtsummers wrote:
         | https://theory.stanford.edu/~nikolaj/programmingz3.html - This
         | one was useful for me to get started with it a while ago.
        
         | Klaus23 wrote:
         | https://smt.st/SAT_SMT_by_example.pdf
        
       | porcoda wrote:
       | Interesting 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.
        
       | RestartKernel wrote:
       | I 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.
        
         | andai wrote:
         | 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 <details> tag).
        
       | IshKebab wrote:
       | Backtracking is not a fast SAT solver.
        
       ___________________________________________________________________
       (page generated 2024-12-05 23:00 UTC)