packages feed

toysolver-0.6.0: src/ToySolver/SAT/MessagePassing/SurveyPropagation/OpenCL.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables, BangPatterns, TemplateHaskell #-}
{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MessagePassing.SurveyPropagation.OpenCL
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable (ScopedTypeVariables, BangPatterns, TypeFamilies)
--
-- References:
--
-- * Alfredo Braunstein, Marc Mézard and Riccardo Zecchina.
--   Survey Propagation: An Algorithm for Satisfiability,
--   <http://arxiv.org/abs/cs/0212002>
--
-- * Corrie Scalisi. Visualizing Survey Propagation in 3-SAT Factor Graphs,
--   <http://classes.soe.ucsc.edu/cmps290c/Winter06/proj/corriereport.pdf>.
--
-----------------------------------------------------------------------------
module ToySolver.SAT.MessagePassing.SurveyPropagation.OpenCL
  (
  -- * The Solver type
    Solver
  , newSolver
  , deleteSolver

  -- * Problem information
  , getNVars
  , getNConstraints

  -- * Parameters
  , getTolerance
  , setTolerance
  , getIterationLimit
  , setIterationLimit

  -- * Computing marginal distributions
  , initializeRandom
  , initializeRandomDirichlet
  , propagate
  , getVarProb

  -- * Solving
  , fixLit
  , unfixLit
  ) where

import Control.Exception
import Control.Loop
import Control.Monad
import Control.Parallel.OpenCL
import Data.Bits
import Data.Int
import Data.IORef
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as VM
import qualified Data.Vector.Storable as VS
import qualified Data.Vector.Storable.Mutable as VSM
import Data.Vector.Generic ((!))
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Generic.Mutable as VGM
import Foreign( castPtr, nullPtr, sizeOf )
import Foreign.C.Types( CFloat )
import Language.Haskell.TH (runIO, litE, stringL)
import Language.Haskell.TH.Syntax (addDependentFile)
import qualified Numeric.Log as L
import System.IO
import qualified System.Random.MWC as Rand
import qualified System.Random.MWC.Distributions as Rand
import Text.Printf

import qualified ToySolver.SAT.Types as SAT

data Solver
  = Solver
  { svOutputMessage :: !(String -> IO ())

  , svContext :: !CLContext
  , svDevice  :: !CLDeviceID
  , svQueue   :: !CLCommandQueue
  , svUpdateEdgeProb   :: !CLKernel
  , svUpdateEdgeSurvey :: !CLKernel
  , svComputeVarProb   :: !CLKernel

  , svVarEdges       :: !(VSM.IOVector CLint)
  , svVarEdgesWeight :: !(VSM.IOVector CFloat)
  , svVarOffset      :: !(VSM.IOVector CLint)
  , svVarLength      :: !(VSM.IOVector CLint)
  , svVarFixed       :: !(VSM.IOVector Int8)
  , svVarProb        :: !(VSM.IOVector (L.Log CFloat))
  , svClauseOffset   :: !(VSM.IOVector CLint)
  , svClauseLength   :: !(VSM.IOVector CLint)
  , svEdgeSurvey     :: !(VSM.IOVector (L.Log CFloat)) -- η_{a → i}
  , svEdgeProbU      :: !(VSM.IOVector (L.Log CFloat)) -- Π^u_{i → a} / (Π^u_{i → a} + Π^s_{i → a} + Π^0_{i → a})

  , svTolRef :: !(IORef Double)
  , svIterLimRef :: !(IORef (Maybe Int))
  }

newSolver :: (String -> IO ()) -> CLContext -> CLDeviceID -> Int -> [(Double, SAT.PackedClause)] -> IO Solver
newSolver outputMessage context dev nv clauses = do
  _ <- clRetainContext context
  queue <- clCreateCommandQueue context dev []

  let num_clauses = length clauses
      num_edges = sum [VG.length c | (_,c) <- clauses]

  (varEdgesTmp :: VM.IOVector [(Int,Bool,Double)]) <- VGM.replicate nv []
  clauseOffset <- VGM.new num_clauses
  clauseLength <- VGM.new num_clauses

  ref <- newIORef 0
  forM_ (zip [0..] clauses) $ \(i,(w,c)) -> do
    VGM.write clauseOffset i =<< liftM fromIntegral (readIORef ref)
    VGM.write clauseLength i (fromIntegral (VG.length c))
    forM_ (SAT.unpackClause c) $ \lit -> do
      e <- readIORef ref
      modifyIORef' ref (+1)
#if MIN_VERSION_vector(0,11,0)
      VGM.modify varEdgesTmp ((e,lit>0,w) :) (abs lit - 1)
#else
      VGM.write varEdgesTmp (abs lit - 1) =<< liftM ((e,lit>0,w) :) (VGM.read varEdgesTmp (abs lit - 1))
#endif

  varOffset <- VGM.new nv
  varLength <- VGM.new nv
  varFixed  <- VGM.new nv
  varEdges <- VGM.new num_edges
  varEdgesWeight   <- VGM.new num_edges
  let loop !i !offset
        | i >= nv   = return ()
        | otherwise = do
            xs <- VGM.read (varEdgesTmp) i
            let len = length xs
            VGM.write varOffset i (fromIntegral offset)
            VGM.write varLength i (fromIntegral len)
            VGM.write varFixed i 0
            forM_ (zip [offset..] (reverse xs)) $ \(j, (e,polarity,w)) -> do
              VGM.write varEdges j $ (fromIntegral e `shiftL` 1) .|. (if polarity then 1 else 0)
              VGM.write varEdgesWeight j (realToFrac w)
            loop (i+1) (offset + len)
  loop 0 0

  -- Initialize all surveys with non-zero values.
  -- If we initialize to zero, following trivial solution exists:
  -- 
  -- η_{a→i} = 0 for all i and a.
  -- 
  -- Π^0_{i→a} = 1, Π^u_{i→a} = Π^s_{i→a} = 0 for all i and a,
  -- 
  -- \^{Π}^{0}_i = 1, \^{Π}^{+}_i = \^{Π}^{-}_i = 0
  -- 
  edgeSurvey  <- VGM.replicate num_edges (L.Exp (log 0.5))
  edgeProbU   <- VGM.new num_edges

  varProb <- VGM.new (nv*2)

  tolRef <- newIORef 0.01
  maxIterRef <- newIORef (Just 1000)

  -- Compile
  let byteSize :: forall a. VSM.Storable a => VSM.IOVector a -> Int
      byteSize v = VGM.length v * sizeOf (undefined :: a)
  (maxConstantBufferSize :: Int) <- fromIntegral <$> clGetDeviceMaxConstantBufferSize dev
  let reqConstantBufferSize =
        byteSize varEdges + byteSize varEdgesWeight +
        byteSize varOffset + byteSize varLength +
        byteSize clauseOffset + byteSize clauseLength
  let flags =
        ["-DUSE_CONSTANT_BUFFER" | maxConstantBufferSize >= reqConstantBufferSize]
  -- programSource <- openBinaryFile "sp.cl" ReadMode >>= hGetContents
  let programSource = $(runIO (do{ h <- openFile "src/ToySolver/SAT/MessagePassing/SurveyPropagation/sp.cl" ReadMode; hSetEncoding h utf8; hGetContents h }) >>= \s -> addDependentFile "src/ToySolver/SAT/MessagePassing/SurveyPropagation/sp.cl" >> litE (stringL s))
  outputMessage $ "Compiling kernels with options: " ++ unwords flags
  program <- clCreateProgramWithSource context programSource
  finally (clBuildProgram program [dev] (unwords flags))
          (outputMessage =<< clGetProgramBuildLog program dev)
  update_edge_prob   <- clCreateKernel program "update_edge_prob"
  update_edge_survey <- clCreateKernel program "update_edge_survey"
  compute_var_prob   <- clCreateKernel program "compute_var_prob"

  return $
    Solver
    { svOutputMessage = outputMessage

    , svContext = context
    , svDevice  = dev
    , svQueue   = queue
    , svUpdateEdgeProb   = update_edge_prob
    , svUpdateEdgeSurvey = update_edge_survey
    , svComputeVarProb   = compute_var_prob

    , svVarEdges       = varEdges
    , svVarEdgesWeight = varEdgesWeight
    , svVarOffset      = varOffset
    , svVarLength      = varLength
    , svVarFixed       = varFixed
    , svVarProb        = varProb
    , svClauseOffset   = clauseOffset
    , svClauseLength   = clauseLength
    , svEdgeSurvey     = edgeSurvey
    , svEdgeProbU      = edgeProbU

    , svTolRef = tolRef
    , svIterLimRef = maxIterRef
    }

deleteSolver :: Solver -> IO ()
deleteSolver solver = do
  _ <- clReleaseKernel (svUpdateEdgeProb solver)
  _ <- clReleaseKernel (svUpdateEdgeSurvey solver)
  _ <- clReleaseKernel (svComputeVarProb solver)
  _ <- clReleaseCommandQueue (svQueue solver)
  _ <- clReleaseContext (svContext solver)
  return ()

initializeRandom :: Solver -> Rand.GenIO -> IO ()
initializeRandom solver gen = do
  n <- getNConstraints solver
  numLoop 0 (n-1) $ \i -> do
    off <- fromIntegral <$> VGM.unsafeRead (svClauseOffset solver) i
    len <- fromIntegral <$> VGM.unsafeRead (svClauseLength solver) i
    case len of
      0 -> return ()
      1 -> VGM.unsafeWrite (svEdgeSurvey solver) off (L.Exp 0)
      _ -> do
        let p :: Double
            p = 1 / fromIntegral len
        numLoop 0 (len-1) $ \i -> do
          d <- Rand.uniformR (p*0.5, p*1.5) gen
          VGM.unsafeWrite (svEdgeSurvey solver) (off+i) (L.Exp (realToFrac (log d)))

initializeRandomDirichlet :: Solver -> Rand.GenIO -> IO ()
initializeRandomDirichlet solver gen = do
  n <- getNConstraints solver
  numLoop 0 (n-1) $ \i -> do
    off <- fromIntegral <$> VGM.unsafeRead (svClauseOffset solver) i
    len <- fromIntegral <$> VGM.unsafeRead (svClauseLength solver) i
    case len of
      0 -> return ()
      1 -> VGM.unsafeWrite (svEdgeSurvey solver) off (L.Exp 0)
      _ -> do
        (ps :: V.Vector Double) <- Rand.dirichlet (VG.replicate len 1) gen
        numLoop 0 (len-1) $ \i -> do
          VGM.unsafeWrite (svEdgeSurvey solver) (off+i) (L.Exp (realToFrac (log (ps ! i))))

-- | number of variables of the problem.
getNVars :: Solver -> IO Int
getNVars solver = return $ VGM.length (svVarOffset solver)

-- | number of constraints of the problem.
getNConstraints :: Solver -> IO Int
getNConstraints solver = return $ VGM.length (svClauseOffset solver)

-- | number of edges of the factor graph
getNEdges :: Solver -> IO Int
getNEdges solver = return $ VGM.length (svEdgeSurvey solver)

getTolerance :: Solver -> IO Double
getTolerance solver = readIORef (svTolRef solver)

setTolerance :: Solver -> Double -> IO ()
setTolerance solver !tol = writeIORef (svTolRef solver) tol

getIterationLimit :: Solver -> IO (Maybe Int)
getIterationLimit solver = readIORef (svIterLimRef solver)

setIterationLimit :: Solver -> Maybe Int -> IO ()
setIterationLimit solver val = writeIORef (svIterLimRef solver) val

-- | Get the marginal probability of the variable to be @True@, @False@ and unspecified respectively.
getVarProb :: Solver -> SAT.Var -> IO (Double, Double, Double)
getVarProb solver v = do
  let i = v - 1
  pt <- (exp . realToFrac . L.ln) <$> VGM.read (svVarProb solver) (i*2)
  pf <- (exp . realToFrac . L.ln) <$> VGM.read (svVarProb solver) (i*2+1)
  return (pt, pf, 1 - (pt + pf))

propagate :: Solver -> IO Bool
propagate solver = do
  tol <- getTolerance solver
  lim <- getIterationLimit solver
  nv <- getNVars solver
  nc <- getNConstraints solver
  let ne = VGM.length (svEdgeSurvey solver)

  let context = svContext solver
      dev = svDevice solver
      queue = svQueue solver
  platform <- clGetDevicePlatform dev

  let infos = [CL_PLATFORM_PROFILE, CL_PLATFORM_VERSION, CL_PLATFORM_NAME, CL_PLATFORM_VENDOR, CL_PLATFORM_EXTENSIONS]
  forM_ infos $ \info -> do
    s <- clGetPlatformInfo platform info
    svOutputMessage solver $ show info ++ " = " ++ s
  devname <- clGetDeviceName dev 
  svOutputMessage solver $ "DEVICE = " ++ devname

  (maxComputeUnits :: Int) <- fromIntegral <$> clGetDeviceMaxComputeUnits dev
  (maxWorkGroupSize :: Int) <- fromIntegral <$> clGetDeviceMaxWorkGroupSize dev
  maxWorkItemSizes@(maxWorkItemSize:_) <- fmap fromIntegral <$> clGetDeviceMaxWorkItemSizes dev
  svOutputMessage solver $ "MAX_COMPUTE_UNITS = " ++ show maxComputeUnits
  svOutputMessage solver $ "MAX_WORK_GROUP_SIZE = " ++ show maxWorkGroupSize
  svOutputMessage solver $ "MAX_WORK_ITEM_SIZES = " ++ show maxWorkItemSizes
  (globalMemSize :: Int) <- fromIntegral <$> clGetDeviceGlobalMemSize dev
  (localMemSize :: Int) <- fromIntegral <$> clGetDeviceLocalMemSize dev
  (maxConstantBufferSize :: Int) <- fromIntegral <$> clGetDeviceMaxConstantBufferSize dev
  (maxConstantArgs :: Int) <- fromIntegral <$> clGetDeviceMaxConstantArgs dev
  svOutputMessage solver $ "GLOBAL_MEM_SIZE = " ++ show globalMemSize
  svOutputMessage solver $ "LOCAL_MEM_SIZE = " ++ show localMemSize
  svOutputMessage solver $ "MAX_CONSTANT_BUFFER_SIZE = " ++ show maxConstantBufferSize
  svOutputMessage solver $ "MAX_CONSTANT_ARGS = " ++ show maxConstantArgs

  let defaultNumGroups = maxComputeUnits * 4

  (updateEdgeProb_kernel_workgroup_size :: Int)
      <- fromIntegral <$> clGetKernelWorkGroupSize (svUpdateEdgeProb solver) dev
  let updateEdgeProb_local_size    = min 32 updateEdgeProb_kernel_workgroup_size
      updateEdgeProb_num_groups    = min defaultNumGroups (maxWorkItemSize `div` updateEdgeProb_local_size)
      updateEdgeProb_global_size   = updateEdgeProb_num_groups * updateEdgeProb_local_size
  svOutputMessage solver $
    printf "update_edge_prob kernel: CL_KERNEL_WORK_GROUP_SIZE=%d -> groupSize=%d numGroups=%d globalSize=%d"
      updateEdgeProb_kernel_workgroup_size updateEdgeProb_local_size updateEdgeProb_num_groups updateEdgeProb_global_size

  (updateEdgeSurvey_kernel_workgroup_size :: Int)
      <- fromIntegral <$> clGetKernelWorkGroupSize (svUpdateEdgeSurvey solver) dev
  let updateEdgeSurvey_local_size  = min 32 updateEdgeSurvey_kernel_workgroup_size
      updateEdgeSurvey_num_groups  = min defaultNumGroups (maxWorkItemSize `div` updateEdgeSurvey_local_size)
      updateEdgeSurvey_global_size = updateEdgeSurvey_num_groups * updateEdgeSurvey_local_size
  svOutputMessage solver $
    printf "update_edge_survey kernel: CL_KERNEL_WORK_GROUP_SIZE=%d -> groupSize=%d numGroups=%d globalSize=%d"
      updateEdgeSurvey_kernel_workgroup_size updateEdgeSurvey_local_size updateEdgeSurvey_num_groups updateEdgeSurvey_global_size

  (computeVarProb_kernel_workgroup_size :: Int)
      <- fromIntegral <$> clGetKernelWorkGroupSize (svComputeVarProb solver) dev
  let computeVarProb_local_size    = min 32 computeVarProb_kernel_workgroup_size
      computeVarProb_num_groups    = min defaultNumGroups (maxWorkItemSize `div` computeVarProb_local_size)
      computeVarProb_global_size   = computeVarProb_num_groups * computeVarProb_local_size
  svOutputMessage solver $
    printf "compute_var_prob kernel: CL_KERNEL_WORK_GROUP_SIZE=%d -> groupSize=%d numGroups=%d globalSize=%d"
      computeVarProb_kernel_workgroup_size computeVarProb_local_size computeVarProb_num_groups computeVarProb_global_size

  let createBufferFromVector :: forall a. VSM.Storable a => [CLMemFlag] -> VSM.IOVector a -> IO CLMem
      createBufferFromVector flags v = do
        VSM.unsafeWith v $ \ptr ->
          clCreateBuffer context (CL_MEM_COPY_HOST_PTR : flags)
            (VGM.length v * sizeOf (undefined :: a), castPtr ptr)

      readBufferToVectorAsync :: forall a. VSM.Storable a => CLMem -> VSM.IOVector a -> IO CLEvent
      readBufferToVectorAsync mem vec = do
        VSM.unsafeWith vec $ \ptr -> do
          clEnqueueReadBuffer queue mem False
            0 (VSM.length vec * sizeOf (undefined :: a)) (castPtr ptr) []
      
      readBufferToVector :: forall a. VSM.Storable a => CLMem -> VSM.IOVector a -> IO ()
      readBufferToVector mem vec = do
        VSM.unsafeWith vec $ \ptr -> do
          ev <- clEnqueueReadBuffer queue mem True
            0 (VSM.length vec * sizeOf (undefined :: a)) (castPtr ptr) []
          _ <- clReleaseEvent ev
          return ()

  var_offset         <- createBufferFromVector [CL_MEM_READ_ONLY] $ svVarOffset solver
  var_degree         <- createBufferFromVector [CL_MEM_READ_ONLY] $ svVarLength solver
  var_fixed          <- createBufferFromVector [CL_MEM_READ_ONLY] $ svVarFixed solver
  var_edges          <- createBufferFromVector [CL_MEM_READ_ONLY] $ svVarEdges solver
  var_edges_weight   <- createBufferFromVector [CL_MEM_READ_ONLY] $ svVarEdgesWeight solver
  clause_offset      <- createBufferFromVector [CL_MEM_READ_ONLY] $ svClauseOffset solver
  clause_degree      <- createBufferFromVector [CL_MEM_READ_ONLY] $ svClauseLength solver
  edge_survey        <- createBufferFromVector [CL_MEM_READ_WRITE] $ svEdgeSurvey solver
  edge_prob_u        <- clCreateBuffer context [CL_MEM_READ_WRITE {-, CL_MEM_HOST_NOACCESS -}]
                          (ne * sizeOf (undefined :: CFloat), nullPtr)

  global_buf         <- clCreateBuffer context [CL_MEM_READ_WRITE {-, CL_MEM_HOST_NOACCESS -}]
                          (ne * sizeOf (undefined :: CFloat) * 2, nullPtr)
  var_prob           <- clCreateBuffer context [CL_MEM_WRITE_ONLY {-, CL_MEM_HOST_READONLY -}]
                          (nv * sizeOf (undefined :: CFloat) * 2, nullPtr)
  group_max_delta    <- clCreateBuffer context [CL_MEM_WRITE_ONLY {-, CL_MEM_HOST_READONLY -}]
                          (updateEdgeSurvey_num_groups * sizeOf (undefined :: CFloat), nullPtr)

  clSetKernelArgSto (svUpdateEdgeProb solver) 0 (fromIntegral nv :: CLint)
  clSetKernelArgSto (svUpdateEdgeProb solver) 1 var_offset
  clSetKernelArgSto (svUpdateEdgeProb solver) 2 var_degree
  clSetKernelArgSto (svUpdateEdgeProb solver) 3 var_fixed
  clSetKernelArgSto (svUpdateEdgeProb solver) 4 var_edges
  clSetKernelArgSto (svUpdateEdgeProb solver) 5 var_edges_weight
  clSetKernelArgSto (svUpdateEdgeProb solver) 6 global_buf
  clSetKernelArgSto (svUpdateEdgeProb solver) 7 edge_survey
  clSetKernelArgSto (svUpdateEdgeProb solver) 8 edge_prob_u

  clSetKernelArgSto (svUpdateEdgeSurvey solver) 0 (fromIntegral nc :: CLint)
  clSetKernelArgSto (svUpdateEdgeSurvey solver) 1 clause_offset
  clSetKernelArgSto (svUpdateEdgeSurvey solver) 2 clause_degree
  clSetKernelArgSto (svUpdateEdgeSurvey solver) 3 edge_survey
  clSetKernelArgSto (svUpdateEdgeSurvey solver) 4 edge_prob_u
  clSetKernelArgSto (svUpdateEdgeSurvey solver) 5 global_buf
  clSetKernelArgSto (svUpdateEdgeSurvey solver) 6 group_max_delta
  clSetKernelArg    (svUpdateEdgeSurvey solver) 7 (updateEdgeSurvey_local_size * sizeOf (undefined :: CFloat)) nullPtr -- reduce_buf

  clSetKernelArgSto (svComputeVarProb solver) 0 (fromIntegral nv :: CLint)
  clSetKernelArgSto (svComputeVarProb solver) 1 var_offset
  clSetKernelArgSto (svComputeVarProb solver) 2 var_degree
  clSetKernelArgSto (svComputeVarProb solver) 3 var_prob
  clSetKernelArgSto (svComputeVarProb solver) 4 var_edges
  clSetKernelArgSto (svComputeVarProb solver) 5 var_edges_weight
  clSetKernelArgSto (svComputeVarProb solver) 6 edge_survey
  
  (group_max_delta_vec :: VSM.IOVector CFloat) <- VGM.new updateEdgeSurvey_num_groups

  let loop !i
        | Just l <- lim, i >= l = return (False,i)
        | otherwise = do
            _ <- clReleaseEvent =<< clEnqueueNDRangeKernel queue (svUpdateEdgeProb solver)
                   [updateEdgeProb_global_size] [updateEdgeProb_local_size] []          
            _ <- clReleaseEvent =<< clEnqueueNDRangeKernel queue (svUpdateEdgeSurvey solver)
                   [updateEdgeSurvey_global_size] [updateEdgeSurvey_local_size] []
            readBufferToVector group_max_delta group_max_delta_vec
            !delta <- VG.maximum <$> VS.unsafeFreeze group_max_delta_vec
            if realToFrac delta <= tol then do
              return (True,i)
            else
              loop (i+1)

  (b,_steps) <- loop 0

  _ <- clReleaseEvent =<< readBufferToVectorAsync edge_survey (svEdgeSurvey solver)
  when b $ do
    _ <- clReleaseEvent =<< clEnqueueNDRangeKernel queue (svComputeVarProb solver)
      [computeVarProb_global_size] [computeVarProb_local_size] []
    _ <- clReleaseEvent =<< readBufferToVectorAsync var_prob (svVarProb solver)
    return ()

  _ <- clFinish queue

  _ <- clReleaseMemObject var_offset
  _ <- clReleaseMemObject var_degree
  _ <- clReleaseMemObject var_edges
  _ <- clReleaseMemObject var_edges_weight
  _ <- clReleaseMemObject clause_offset
  _ <- clReleaseMemObject clause_degree
  _ <- clReleaseMemObject edge_survey
  _ <- clReleaseMemObject edge_prob_u
  _ <- clReleaseMemObject global_buf
  _ <- clReleaseMemObject var_prob
  _ <- clReleaseMemObject group_max_delta

  return b

fixLit :: Solver -> SAT.Lit -> IO ()
fixLit solver lit = do
  VGM.unsafeWrite (svVarFixed solver) (abs lit - 1) (if lit > 0 then 1 else -1)

unfixLit :: Solver -> SAT.Lit -> IO ()
unfixLit solver lit = do
  VGM.unsafeWrite (svVarFixed solver) (abs lit - 1) 0