1. 9

I just got started on writing a SAT solver (this is not working ATM) and while I’ve been finding some resources, I feel like I’m missing something … does anyone have some beginner pointers on SAT solver implementation? I was looking for something like pseudocode, algorithm visualization (like this http://www.cs.usfca.edu/~galles/visualization/Algorithms.html, for instance), anything.

Also if anyone knows about how can they be applied in a compiler (typesystem, optimization, …), feedback is also welcomed.


  2. 9

    I know that you know about some of these things already, but I’m going to mention them in an attempt to try to be complete about the things I’m aware of:

    Minisat is a great starting point and is pretty comprehensible. 0install has implemented something based on Minisat in both Python and OCaml and both implementations seemed pretty easy going from what I recall.

    MIT had a summer school about this a couple of years ago. See http://people.csail.mit.edu/vganesh/summerschool/ and https://wikis.mit.edu/confluence/display/satsmtschool11/SATSMT+Summer+School+2011;jsessionid=EC50861C5F5FF7B2693D04E69AF0C090. Some people blogged about this … http://dontstuffbeansupyournose.com/2011/06/20/smt-solvers-summerschool-at-mit/ and http://seanhn.wordpress.com/2011/06/13/satsmt-summer-school-2011-summary/ (make sure you notice he has a bunch of other posts, not just that one). (It is also worth noting that that last blog has posts on other interesting topics as well…)

    A bit older, but the University of Oregon had a summer school in 2008 which had some lectures on the topic as well: https://www.cs.uoregon.edu/research/summerschool/summer08/curriculum.html

    There was a question on Stack Overflow which asked something similar and got a single response: http://stackoverflow.com/questions/18816983/the-usage-of-constraint-solvers-in-programming-languages-and-compilers

    Galois had an interesting post on this topic a couple of years ago as well: https://galois.com/blog/2011/01/merging-smt-solvers-and-programming-languages/ … Here’s a presentation from one of the Galois folk: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/28/slides/don.pdf

    Then there’s the work on Souper: https://github.com/google/souper … and superoptimizers in general: http://blog.regehr.org/archives/1109 and http://blog.regehr.org/archives/1146 and http://blog.regehr.org/archives/923

    One thing that I know nothing about is making the jump from a SAT solver to an SMT solver … I’d love to hear / learn more about that.

    http://cl-informatik.uibk.ac.at/software/minismt/ looks potentially interesting to look at.

    On the type system side of things, looking at refinement types is pretty interesting. Liquid Types are pretty cool looking: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/http://goto.ucsd.edu/~rjhala/liquid/abstract_refinement_types.pdf

    http://prosecco.gforge.inria.fr/personal/hritcu/publications/dminor-icfp2010.pdf looks like an interesting paper (Semantic subtyping with an SMT solver). http://research.microsoft.com/en-us/um/redmond/events/smt08/bobot.pdf looks interesting as well (Implementing Polymorphism in SMT Solvers).

    There’s also work showing Scala + Z3: http://lara.epfl.ch/~kuncak/papers/KoeksalETAL11ScalaZ3.pdf

    And SBV: http://leventerkok.github.io/sbv/

    http://cvc4.cs.nyu.edu/web/ looks like something worth looking at … and is not prohibitively licensed.

    And finally … https://github.com/tomprimozic/type-systems/tree/master/refined_types shows some stuff in terms of integrating a type system with an SMT solver.

    1. 1

      Thanks for the pointers; the solver is now working but it’s excruciatingly slow for big problems.

    2. 2

      Have you considered not writing one? Real world solvers have a fair amount of trickery involved.

      Perhaps have a look at http://www.satcompetition.org and read some of the papers behind them.