Modern SAT solvers: fast, neat and underused – part 2(codingnest.com)

154 pointsby aw16211078 वर्ष पहले15 comments

Modern SAT solvers: fast, neat and underused – part 2

https://codingnest.com/modern-sat-solvers-fast-neat-and-underused-part-2-of-n/

15 comments

orlp8 वर्ष पहले

All 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.

sevensor8 वर्ष पहले

Using Z3 with Python is like having superpowers. I second the recommendation.

CamperBob28 वर्ष पहले

Thanks -- that is a very cool document. I hope he's able to finish it and polish it.

popotamonga8 वर्ष पहले

Thanks this is very very helpful.

dragontamer8 वर्ष पहले

A 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-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...

----------

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.

vinaybn8 वर्ष पहले

This 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

taeric8 वर्ष पहले

For 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

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.

jwilk8 वर्ष पहले

Part 1: https://news.ycombinator.com/item?id=17684502

sushisource8 वर्ष पहले

Why 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?

alexgmcm8 वर्ष पहले

Yeah - 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_Kream8 वर्ष पहले

Rather than encoding this as SAT, would it be easier to use an actual constrain solver environment here? Like MiniZinc or PiCat.

sevensor8 वर्ष पहले

Aren't those modeling languages? I believe they hook up to actual solvers which may or may not be SAT solvers.

Karrot_Kream8 वर्ष पहले

PiCat 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).

sevensor8 वर्ष पहले

I 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.

eggy8 वर्ष पहले

I 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.