What is SAT and what it is good for?

Question

Recently I saw a Reddit article on using SAT for solving a puzzle [1]. This got me very curios about this "SAT" thing. I read the Wikipedia article but I would like to ask someone of you to explain it for me in more layman terms.

What is SAT and what is it good for? Can it be used to traverse a tree structure? For parsing texts? For line breaking [2]? For bin packing [3]? Is it a kind of optimization technique?

On related note, I read that NP vs P is about choosing which numbers of a set sum to zero vs checking whether some numbers sum to zero - is SAT somehow related to this?

[1] http://www.reddit.com/r/programming/comments/pxpzd/solving_hexiom_really_fast_with_a_sat_solver/

[2] http://en.wikipedia.org/wiki/Line_wrap

[3] http://en.wikipedia.org/wiki/Bin_packing_problem

Answer 1

SAT is very important because it is NP-Complete. To understand what this means you need a clear notion of Complexity classes. Here is a short rundown:

• P is the class of all problems which can be solved in polynomial time (i.e. fast).

• NP is the class of all problem for which a solution can be verified in polynomial time. This means veryfing a given solution is fast, but finding one is usually slow (most often exponential time). Unless the problem is in the P part of NP of course (as pointed out below P is part of NP, as you can easily verify).

Then there is the set of NP-Complete problems. This set contains all problem which are so generic, you can solve these Problems instead of another one from NP (this is called reducing a problem onto another). This means you can transform a problem from one domain into another NP-Complete problem, have it derive an answer and transform the answer back.

Often however it can be proven that a problem is NP-Complete, but the transformations are unclear for another given problem.

SAT is so nice, because it is NP-Complete, i.e. you can solve it instead of any other problem in NP, and also the reductions are not so hard to do. TSP is another NP-Complete problem, but the transformations are most often much more difficult.

So, yes, SAT can be used for all these problems you are mentioning. Often however this is not feasible. Where it is feasible is, when no other fast algorithm is known, such as the puzzle you mention. In this case you do not have to develop an algorithm for the puzzle, but can use any of the highly optimized SAT-Solvers out there and you will end up with a reasonable fast algorithm for your puzzle.

Traversing a tree structure is so simple for example, that any transformation from and to SAT will most likely be much more complex than just writing the traversal directly.

Answer 2

To make a long story short, a SAT solver is something you give a boolean formula to, and it tells you whether it can find a value for the different variables such that the formula is true.

Example

suppose that a, b and c are boolean variables, and you want to know if these variables can be assigned a value that somehow makes the formula (¬a ∨ b) ∧ (¬b ∨ c). You send this formula to the SAT solver, and it will return you true. SAT solvers also often give you a valid assignment. In this case this assignment might be a: false, b:false, c:false.

What can it be used for ?

I would not use it to traverse trees nor to parse text or to break lines. However, you could use it when traversing a tree to check if some constraints on the tree are satisified. You can certainly use it for bin packing, even though some specialized CSP solvers will probably perform better on this kind of problems.

SAT solvers are becoming much more common these days, especially in software like package managers. Eclipse embeds SAT4j to manage dependencies among its plugins. Other applications of SAT typically include model checking, planning applications, configurators, scheduling, and many others.