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?
