Modern SAT solvers: fast, neat and underused – part 2 | Hacker News Reader

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

codingnest.com

154 pointsaw162110715 comments

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.

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

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

Thanks this is very very helpful.

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.

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

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.

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

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?

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.

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

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

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

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.

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.

Reply on news.ycombinator.com