5 ms·

What do you use it for?

• LeonRobrotsky 12y ago
  Making vague but supportive comments on HN.
  • pavpanchekha 12y ago
    I had a long day at work, and didn't see this. I posted another comment (couldn't edit; too late). You may be sure that I am MS shill, cleverly astroturfing their now-free product.
    • LeonRobrotsky 12y ago
      Sorry- my remark wasn't intended as a shill accusation, but re-reading it now, I see it. It was tongue-in-cheek, I enjoyed the positivity in your original comment.
• ufo 12y ago
  SAT solvers and SMT solvers are greeat for the kind of problems where your first thought would be to use brute force or backtracking. They use some really clever implementation tricks and heuristics that are likely to beat any of your algorithms that you write from scratch. One of the more famous places where these constraint solvers are used is to deal with dependency management in package systems. For example, zeroinstall uses a SAT solver to resolve dependency conflicts. http://0install.net/solver.html http://0install.net/solver.html A sillier example is the time I used a sat solver to find the solutions for a flash puzzle game. The part I'm proudest of is that the sat solver could handle the highly symmetric cases that stumped the hand-written backtracking algorithms. And if I had used an SMT solver instead of SAT I would not have had to convert everything all the way doen to boolean formulas. https://github.com/hugomg/hexiom https://github.com/hugomg/hexiom In the readme I explain a bit why the sat solver helped.
  • david-given 12y ago
    Hmm. Would a SAT solver be useful for compiler technologies? A compiler is basically solving the problem of: here is a sequence of things I want done; here is a description of what the machine can do; find a combination of the latter which achieves the former. The details are the tricky bit, particularly for unpleasantly asymmetric instruction sets like the old 8-bit architectures. It would be so nice if I could just throw a description of the problem at some sort of machine reasoning system and have it Just Work...
    • TheLoneWolfling 12y ago
      There are superoptimizers that do exactly that. But current SAT solvers aren't powerful enough to do so at much more than a few tens of instructions long. Still useful though.
    • bronxbomber92 12y ago
      Check out Alive http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 https://github.com/nunoplopes/alive https://github.com/nunoplopes/alive http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170
    • tikhonj 12y ago
      Yes, although it's hard to make it scale in every case. What you're talking about sounds like the field of program synthesis[1], which uses SMT solvers (among other technologies) to generate code to some specification. I worked on a system[2] that used this sort of technique to optimize code for a weird architecture (GreenArrays' Forth-based chip[3]) and it was certainly much easier to implement than a classical optimizing compiler. Perhaps the most relevant example project here would be Rosette[4], which is basically a framework for easily writing synthesizers for different tasks. It would let you implement a description of your machine in Scheme (ie write a simple interpreter) and automatically generate a synthesizer for it that could compile programs in your language to formulas in a solver of some sort. [1]: http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-overview-notes.pdf http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-... [2]: http://jelv.is/chlorophyll.pdf http://jelv.is/chlorophyll.pdf [3]: http://www.greenarraychips.com/ http://www.greenarraychips.com/ [4]: http://homes.cs.washington.edu/~emina/rosette/ http://homes.cs.washington.edu/~emina/rosette/