# NP is the new P

In school I learned that NP-complete problems are intractably hard, chief among them Boolean satisfiability (SAT). My mind was thoroughly blown when I heard about SAT solvers and their success at a wide variety of real-world problems (1, 2, 3, 4). Apparently NP is the new P.

Setting aside the theory for a moment, what this implies is the feasibility (for some problems) of a new style of programming based on solving logical equations. We can describe a problem in terms of requirements for the solution, and leave the task of actually finding that solution to a highly-tuned general-purpose library.

There are quite a few SAT-solver libraries on Hackage. I tried some of them on some toy projects. I ran into a number of frustrations, as well as some code that just plain didn't work.

So I decided to write my own binding to Yices. Yices is an efficient and flexible solver for "SAT modulo theories" (SMT). This means that it understands not only Boolean logic but also types like integers, bit vectors, functions, etc. Unfortunately it's not open-source, but it does support a variety of interfaces to external code. The raw C API in bindings-yices was a great starting point, and today I'm releasing yices-easy 0.1.

yices-easy is not the first Yices binding on Hackage (1, 2, 3), nor will it be the last. It's not feature-complete, nor heavily optimized. The goal is simply to lower the entry barrier for Haskell developers (in particular, me) to learn about and use this powerful alien technology.

# Latin squares

Let's see an example! A Latin square is an n × n matrix where each row and column is a permutation of `[1..n]`. We can express these constraints directly using Yices's integer variables:

``import Yices.Easyimport Yices.Easy.Sugarimport Yices.Easy.Buildimport Control.Monad ( forM_, liftM2 )import qualified Data.Map as Mcell :: (Int,Int) -> Stringcell (x,y) = concat ["c", show x, "_", show y]query :: Int -> Queryquery n = execBuild \$ do  let cells = liftM2 (,) [1..n] [1..n]  forM_ cells \$ \c -> do    x <- declInt \$ cell c    assert ((x >=. 1) &&. (x <=. fromIntegral n))  forM_ cells \$ \c@(i0,j0) -> do    let notEq c1 = assert (Var (cell c) /=. Var (cell c1))    forM_ [i0+1..n] \$ \i -> notEq (i, j0)    forM_ [j0+1..n] \$ \j -> notEq (i0,j )run :: Int -> IO ()run n = do  Sat model <- solve \$ query n  let soln c = case M.lookup (cell c) model of Just (ValInt k) -> k      line i = forM_ [1..n] \$ \j -> putStr (show (soln (i,j)) ++ " ")  forM_ [1..n] \$ \i -> line i >> putChar '\n'``

Testing it:

``````GHCi> run 9
4 2 6 8 5 1 7 9 3
1 9 7 3 8 6 4 2 5
5 3 9 1 4 7 6 8 2
3 4 5 2 7 9 8 1 6
7 5 8 6 9 2 3 4 1
2 8 1 5 6 4 9 3 7
6 7 4 9 1 3 2 5 8
8 6 2 4 3 5 1 7 9
9 1 3 7 2 8 5 6 4
``````

This takes about 2 to 4 seconds on my laptop. Yices is nondeterministic, so you can get several Latin squares by running the solver repeatedly.

The function `query` builds a Yices `Query`. This is a totally first-order value that you can build and inspect in pure Haskell. We're using some infix syntactic sugar and some monadic bookkeeping, but these are not essential parts of the library. At the core, we just build a Yices syntax tree and hand it off to `solve`, which translates it to Yices's internal data structures and invokes the solver.

Our query consists of two parts. First we declare an integer-valued variable for each cell in the Latin square, and constrain them to take on values from `[1..n]`. Then we constrain each cell to differ from those directly below or to the right. `run` invokes the solver, then produces formatted output.

# Graph coloring

A classic NP-complete problem is graph coloring. Given is a graph of nodes and edges, and a set of k colors. We must pick a color for each node, such that nodes connected by an edge never have the same color. Again, we can express this directly in Yices:

``import Yices.Easyimport Yices.Easy.Sugarimport Yices.Easy.Buildimport Control.Monadimport Systemimport Data.Listimport qualified Data.Map      as Mimport qualified Data.GraphViz as Gtype Edge  = (Ident, Ident)data Graph = Graph [Ident] [Edge]parse :: String -> Graphparse g = Graph vs es where  es = map ((\[x,y] -> (x,y)) . words) \$ lines g  vs = nub \$ concat [ [x,y] | (x,y) <- es ]query :: Int -> Graph -> Queryquery n (Graph vs es) = execBuild \$ do  forM_ vs \$ \v -> do    x <- declInt v    assert ((x >=. 0) &&. (x <. fromIntegral n))  forM_ es \$ \(x,y) -> assert (Var x /=. Var y)render :: Graph -> Model -> Stringrender (Graph vs es) m = G.printDotGraph g where  g   = G.DotGraph False False Nothing \$ G.DotStmts gbl [] vss ess  gbl = [G.NodeAttrs [G.Style [G.SItem G.Filled []]]]  vss = [G.DotNode v [G.Color [G.X11Color \$ color v]] | v <- vs]  ess = [G.DotEdge x y False [] | (x,y) <- es]  colors = [G.Red, G.Green, G.Blue, G.Cyan, G.Magenta, G.Yellow, G.White]  color v = case M.lookup v m of Just (ValInt i) -> colors !! fromIntegral imain :: IO ()main = do  [nx,file] <- getArgs  numColors <- readIO nx  graph     <- parse `fmap` readFile file  result    <- solve \$ query numColors graph  case result of    Sat model -> writeFile "out.dot" \$ render graph model    _         -> putStrLn "No solution." >> exitFailure``

Unsurprisingly, most of this code is input / output glue. In `parse` we parse a very simple edge-list format (see below). `query` builds the Yices query and is quite similar to the previous example. (In fact, Latin squares are the colorings of a rook's graph.) `render` uses the graphviz library to build a colorful graph, which we can render with `dot`.

Let's color the Petersen graph:

``````\$ cat petersen.txt
Ao Bo
Bo Co
Co Do
Do Eo
Eo Ao
Ao Ai
Bo Bi
Co Ci
Do Di
Eo Ei
Ai Ci
Bi Di
Ci Ei
Di Ai
Ei Bi
\$ ghc --make -O graph-color.hs
\$ export LD_LIBRARY_PATH=~/local/lib
\$ ./graph-color 2 petersen.txt
No solution.
\$ ./graph-color 3 petersen.txt
\$ dot -Tpng out.dot > out.png
\$ xview out.png
``````

The coloring works! Too bad Graphviz can't recognize the striking symmetry in the Petersen graph.

Note that I had to specify `LD_LIBRARY_PATH` because `libyices.so` is not installed globally on my system. If that's the case for you, you will also need to pass `--extra-include-dirs=PATH` and `--extra-lib-dirs=PATH` options to `cabal` when you install `bindings-yices`, which is used by my library.

# What next?

So that's yices-easy. It's a young library; I need people to bang on it and find bugs. What can you do with an SMT solver?

1. Please update Hackage to reflect that the bindings are BSD3 but that Yices is not.

2. danly:

Is that common practice? For example, I see that most libraries binding to the Windows API are BSD3 and make no mention of the fact that Windows itself is not. Same for the other Yices bindings.

3. FIrst of all, well done making your code BSD3!

Secondly, yes please mention that yices' license makes it just about useless for any interesting work. Heck you can't even distribute it. There's nothing in Microsoft's SDKs as restrictive as this.

4. Keegan, you might like the recent work to apply SAT solving to Debian's package transition process: http://www.joachim-breitner.de/blog/archives/515-SAT-solving-the-testing-transition-problem.html

5. I tried it on my mac but it failed like this:

Prelude Data.List Data.Map System.Directory System.Cmd> :load latin_squares.hs
[1 of 1] Compiling Main ( latin_squares.hs, interpreted )