# 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.Easy`

import Yices.Easy.Sugar

import Yices.Easy.Build

import Control.Monad ( forM_, liftM2 )

import qualified Data.Map as M

cell :: (Int,Int) -> String

cell (x,y) = concat ["c", show x, "_", show y]

query :: Int -> Query

query 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.Easy`

import Yices.Easy.Sugar

import Yices.Easy.Build

import Control.Monad

import System

import Data.List

import qualified Data.Map as M

import qualified Data.GraphViz as G

type Edge = (Ident, Ident)

data Graph = Graph [Ident] [Edge]

parse :: String -> Graph

parse 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 -> Query

query 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 -> String

render (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 i

main :: 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?