6 ms·
Modern SAT solvers: fast, neat and underused – part 2
- nightcracker 8y agoAll I can do is recommend people to try out the z3 solver, especially through the Python API. There's no better resource than https://yurichev.com/writings/SAT_SMT_by_example.pdf https://yurichev.com/writings/SAT_SMT_by_example.pdf.
- CamperBob2 8y agoThanks -- that is a very cool document. I hope he's able to finish it and polish it.
- popotamonga 8y agoThanks this is very very helpful.
- sevensor 8y agoUsing Z3 with Python is like having superpowers. I second the recommendation.
- jwilk 8y agoPart 1: https://news.ycombinator.com/item?id=17684502 https://news.ycombinator.com/item?id=17684502
- dragontamer 8y agoA closely related technique to SAT solvers is the "Constraint Satisfaction Problem" which I've been looking into recently. Constraint Programming and SAT are BOTH NP-complete problems, and as such, they are mathematically equivalent. However, its sometimes more "obvious" to write problems in one form vs the other. For example, Sudoku is simply written 27 constraints: * All Different (X11, X12, X13, X14, X15, X16, X17, X18, X19) * All Different (X21, X22, X23, X24, X25, X26, X27, X28, X29) ... * All Different (X11, X21, X31, X41, X51, X61, X71, X81, X91) ... * All Different (X11, X12, X13, X21, X22, X23, X31, X32, X34) ... etc. etc. Then define each "X" variable as "between 1 and 9" and bam, you're done with defining the problem in terms of "Constraints". Representing Sudoku as a SAT problem is possible of course, but its just... harder. It just feels more humanly natural to represent Sudoku in terms of constraints. Or maybe not. Read "Part 1" if you want to see how the original blogger solved it in terms of 3-SAT (https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/ https://codingnest.com/modern-sat-solvers-fast-neat-underuse...) ---------- Here's an article from IBM hyping up their "CPLEX" Constraint solver for Sudoku for example: https://www.ibm.com/developerworks/community/blogs/jfp/entry/solving_the_hardest_sudoku?lang=en https://www.ibm.com/developerworks/community/blogs/jfp/entry... ---------- Anyway, just plugging in a similarly fast, neat, and underused (and mathematically equivalent) solver to what the blogpost talks about. I personally don't know too much about SAT-solvers or their algorithms, aside from "They're same same, but different" to Constraint Programming.
- taeric 8y agoFor those having fun with the rabbit hole that is solving sudoku and similar problems with a computer, I highly recommend taking a look at Knuth's Dancing Links. I had fun with the idea here: http://taeric.github.io/Sudoku.html http://taeric.github.io/Sudoku.html His latest book which is due out this year goes into quite a lot of depth specifically on sudoku. The one he released last year using SAT solvers has a few fun exercises. In particular, he uses a SAT solver to construct sudoku boards that have a unique solution, but do not have any forced moves on the board.
- vinaybn 8y agoThis is a great related talk that explores how puzzles can be solved using SAT solvers, constraint solvers and dancing links: https://www.youtube.com/watch?v=TA9DBG8x-ys https://www.youtube.com/watch?v=TA9DBG8x-ys
- sushisource 8y agoWhy would MKS with 4k keys matter? Is that really a real thing that people do? Seems nuts vs just using an electronic system at that point. Alternatively - can MKS be applied to cool permissions problems not involving physical keys?
- alexgmcm 8y agoYeah - that seems crazy as surely you would have a very limited number of solutions given manufacturing constraints. So then if a key gets stolen and you have to replace the system it could be literally impossible to do.
- Karrot_Kream 8y agoRather than encoding this as SAT, would it be easier to use an actual constrain solver environment here? Like MiniZinc or PiCat.
- sevensor 8y agoAren't those modeling languages? I believe they hook up to actual solvers which may or may not be SAT solvers.
- Karrot_Kream 8y agoPiCat seamlessly integrates with solvers. MiniZinc does need a solver capable of processing it, but it's fairly easy to do so. I just thought this kind of problem was a bit easier to describe more generally in a constraint form than SAT (which takes a bit of effort).
- sevensor 8y agoI see your point -- CNF as a modeling language leaves a lot to be desired. What I like about this article is that it uses CNF anyway and takes you through the hard work you'd have to do to express a problem that way. I didn't know about the Tseytin transformation, for instance, so I'd given up on using CNF because of the exponential blowup in my constraints. I probably still won't be using SAT solvers directly, but it's nice to learn how they work. It's like knowing an assembly language for constraint satisfaction.
- eggy 8y agoI have been delving into Fstar [1] which has an SMT backend and provides a means of program verification. Fstar programs can then be code extracted to OCaml or Fsharp. I think the combination of SAT solving, and a formal language like F* that can create executable OCaml or Fsharp code will be very useful in creating a pragmatic path to verified programs. [1] https://www.fstar-lang.org/ Edit: I wanted to add that I prefer the Lisp syntax of SMT to the python, but that's based upon personal bias. However, a Lisp-like syntax was chosen due to the ease of parsing Lisp s-expressions.