An example: solving SAT by exhaustive search

Haskell example

In this example, we are to solve instances of 3-SAT. We implement an extremely naive methode here, where all the possibilites are explored, for the sake of illustrating how Parry works on the simplest possible example.

We begin by defining the type of jobs, that needs to be in a module common to the client and the server (since jobs are exchanged by the protocol). This file will also contain RSA public and private keys, that will be hardlinked in the program in our example. See Parry's documentation for a way to generate these. Our representation of a job is simply a prefix, which is an integer with n variables already assigned, where n is the position field of the job. In a file called "Common.hs", write the following:

{-#LANGUAGE DeriveGeneric #-}
module Common where
import Crypto.Types.PubKey.RSA
import GHC.Generics
import Data.Binary


data Job=Job { formula::[[Int]], prefix::Int, position::Int, k::Int }
         deriving (Show,Generic,Ord,Eq)

instance Binary Job

public=private_pub private
private=PrivateKey {private_pub = PublicKey {public_size = 256, public_n = 26048661925464402170803203610009492013690419591728024787638194564400900719109440870194421082385509302417324704598278477102988354712408153243010562791006435595770242530620859582280682319681067258467485190309027894881059938779109721236356570836774201977748490631415863164162747338210209429162502181276913806057088932879487465910192878799165995512946948978117366132190353122580051612458321765648812202672124476925818598081937527021587384375421578433156492512568380532637820215103756144364766455220621168986700521489333731760463830967194746225311959229698572016704055298441065469186370541093712549150705225053343429989063, public_e = 65537}, private_d = 566785051279616666853309860809520356615690958356411848988694408484301759699865155269500350389577433590904451359646384612491590915359171559951371935547479700925711672012227379409070494344648090553040784310857588508787272421670361207913765811880922410550823926032607853153120797477573868898267056937316006033796912405918757504105658955224829110691503030613343453555839005320645194614214105909102061846483087982754723500200536470550916984755534124638727518668913573602283597358665203684213692329262339200943763192227358271358429394781604604935233696003718583395719820290015003488725204816980188877505951514454819215377, private_p = 0, private_q = 0, private_dP = 0, private_dQ = 0, private_qinv = 0}

Our next step is to write a client. Our client is really simple: when it receives a job, if asked to share it, it returns a list of two jobs, one with the (position j)th variable set to 0, the other with that variable set to 1. Else, it just tries all possible assignments of the remaining variables. Parry's job is to interrupt that exhaustive search of all posibilities when needed, and reshare the jobs with other machines.

In a file called "Client.hs", write the following:

{-#OPTIONS -fno-warn-orphans#-}
import Data.Bits
import Parry.Client
import Common

eval l var=
  foldl (\y clause->
          y && foldl (\x i->
                       if i.&.1==0 then
                         x || testBit var (i`shiftR`1)
                         x || (not $ testBit var (i`shiftR`1))
                     ) False clause
        ) True l

instance Client Job where
  isResult j=eval (formula j) (prefix j)

atomicWork share j=
  if position j<=0 then [] else
    if share then
      let pos=position j-1 in
      [j { position=pos, prefix=prefix j`clearBit`pos },
       j { position=pos, prefix=prefix j`setBit`pos }]
      let pos=position j in
      map (\x-> j { prefix=x, position=0 }) $
      filter (\x->eval (formula j) (prefix j .|. x))

main::IO ()
main=client (defaultConfig private public) (\u _ v->return $ atomicWork u v)

Note that the representation of 3-SAT formulae is not the most naive one: its type is [[Int]], where the rightmost bit of each integer indicates whether the literal is positive or negative, and the other bits indicate the variable number. This choice was made to minimize the size of this example, and to allow the generation of random instances easily.

Finally, we can write the server, which is not much more than an initial job, an instance of Parry.Protocol.Exhaustive to tell the server how to keep track of killed jobs. In this example, the server forks a thread with the default web interface before starting the synchronization server.

{-#OPTIONS -fno-warn-orphans#-}
{-#LANGUAGE MultiParamTypeClasses,FlexibleInstances#-}
import Parry.Server
import Common
import Control.Concurrent
import Parry.WebUI
import qualified Data.ByteString.Char8 as B
import Data.ByteString.Lazy.Builder

initial=Job {

instance Exhaustive Job where
  depth j=variables-position j
  kill j=j { k=k j+1 }

instance Result Job [(String,Job)] where
  addResult h r j=(h,j):r

instance Html [(String,Job)] where
  toHtml x=byteString $ B.pack $ show x
instance Html Job where
  toHtml x=byteString $ B.pack $ show x

main::IO ()
  state<-initState [initial] ([]::[(String,Job)])
  modifyMVar_ state $ \st->
    return $ st { authorizedKeys=public:(authorizedKeys st) }
  _<-forkIO $ webUI 8000 state
  server defaultConfig state

Then compile and launch everything by doing the following:

ghc -O2 Server
ghc -O2 Client

Launch clients by running ./Client, and watch your jobs on the web interface: http://localhost:8000.

Notice that, against all good practices of classical software engineering, we used orphan instances. This is extremely evil, because you could define different instances of the same typeclass and find yourself with unsolvable typing errors. However, it reduces the size of the executables by a small amount with no bad consequence (except violation of principles), which probably means less cache misses, and GHC will have an easier time optimizing the code. What else?

Similarly, Parry is designed to optimize network communications, but storing fixed parameters inside the jobs (like we did here) is a bad idea, for similar reasons.

OCaml example

The OCaml version works almost in the same way. The complete example above translates to the following in OCaml:

In file, write the following:
type job={formula:int list list;prefix:int;position:int}
let variables=30
let sharable _=true
type result=(string*job) list
let timeout=1800.
let ping=600.

let add_result a b c=(a,c)::b
let depth j=variables-j.position
let signature_size=1 lsl 10

let html_job buf j=
  Buffer.add_string buf
  (Printf.sprintf "{ prefix=%d, position=%d }" j.prefix j.position)

let html_result buf r=
  List.iter (fun (host,x)->
    Buffer.add_string buf "<p>Host: ";
    Buffer.add_string buf host;
    Buffer.add_string buf "<br/><br/>";
    html_job buf x;
    Buffer.add_string buf "</p>";
  ) r
In file, write the following:
module Pats=Parry_server.Server(Job)
open Parry_server
open Parry_common
open Job

let initial={

let st=Pats.initial_state [initial] []
let key=
  let open Cryptokit.RSA in
  {Parry_common.blank_key with size=(String.length Key.n) lsl 3; n=Key.n;e=Key.e }

let _=
  Pats.add_key st key;
  let _=Thread.create (fun ()->Pats.webui 8000 st) () in
  Pats.server st
In file, write the following:
open Key
open Job
module Example=Parry_client.Client(Job)
open Example

let eval l var=
  List.fold_left (fun y clause->
    y && List.fold_left (fun x i->
      if i land 1=0 then
        x || (var land (1 lsl (i lsr 1)) = 1)
        x || (var land (1 lsl (i lsr 1)) = 0)
    ) false clause
  ) true l

let key=
  let open Cryptokit.RSA in
  {Parry_common.blank_key with size=(String.length Key.n) lsl 3; n=Key.n;e=Key.e;d=Key.d }

let _=
    { server=(Unix.gethostbyname "localhost").Unix.h_addr_list.(0);
      key=key }
    (fun save j->
      let rec explore results jobs=match jobs with
        | h::s->
            save results jobs;
            if h.position=0 then
              explore (if eval h.formula h.prefix then h::results else results) s
              explore results (
                { j with position=j.position-1 }
                ::{ j with position=j.position-1; prefix=j.prefix lxor (1 lsl (j.position-1)) }
                 :: jobs
      explore [] [j]
Then compile with:
ocamlfind ocamlopt -package cryptokit,Parry.client -linkpkg -unsafe
ocamlfind ocamlopt -package cryptokit,Parry.server -linkpkg -thread -unsafe
Of course, the -unsafe option causes no problem in a proven program. Moreover, the keys can be generated by the following program:
open Cryptokit.RSA
let _=
  let key=new_key 1024 in
  let f=open_out "" in
  Printf.fprintf f "let n=%S and e=%S and d=%S\n"
    key.n key.e key.d

About public keys

In our example, designed to run on a single machine, public and private keys are stored in the binaries. This means that if you send your binaries over a cleartext network, the private key will be publicly readable. Unfortunately, machines with no ssh servers seldom offer you other options.

A more reasonable way to do this, is to generate keys on the client machines, hardcoding them in the binaries as we do in this example, and then send the public keys only to the central server, for instance by email. In this way, your private keys will never transit through the network. In OCaml, this means transmitting the n and e fields of the key records. In Haskell, the public and private keys used in module Crypto.Types.PubKey.RSA are already separated.

However, beware when transmitting public keys! If the email you send is not signed, you must check that the public keys sent and received are the same. A good way to do this is to describe your key in person to the person running the server. A faster way (and almost as secure), is that both compute a SHA1 hash of the key, and then check in person that these are the same.
Never trust written information in chat messages, emails or webpages (not even this one :-). Trust phone calls only when you have no other option.

In the example above, there is only one way to add public keys. In a large scale application, you might want to replace the following line of the server code:

  modifyMVar_ state $ \st->
    return $ st { authorizedKeys=public:(authorizedKeys st) }

by a thread that periodically reads a file with public keys, or some other interface of your choice.