{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
----------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Solver.SLS.UBCSAT
-- Copyright   :  (c) Masahiro Sakai 2017
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
----------------------------------------------------------------------
module ToySolver.SAT.Solver.SLS.UBCSAT
  ( ubcsatBest
  , ubcsatBestFeasible
  , ubcsatMany
  , Options (..)
  ) where

import Control.Exception
import Control.Monad
import Data.Array.IArray
import Data.Char
import Data.Default
import Data.Either
import Data.Function
import Data.List
import Data.Void
import System.Directory
import System.IO
import System.IO.Temp
import System.Process
import Text.Megaparsec hiding (try)
import Text.Megaparsec.Char

import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

data Options
  = Options
  { Options -> FilePath
optCommand :: FilePath
  , Options -> Maybe FilePath
optTempDir :: Maybe FilePath
  , Options -> WCNF
optProblem :: CNF.WCNF
  , Options -> Maybe FilePath
optProblemFile :: Maybe FilePath
  , Options -> [Lit]
optVarInit :: [SAT.Lit]
  }

instance Default Options where
  def :: Options
def = Options :: FilePath
-> Maybe FilePath -> WCNF -> Maybe FilePath -> [Lit] -> Options
Options
        { optCommand :: FilePath
optCommand = FilePath
"ubcsat"
        , optTempDir :: Maybe FilePath
optTempDir = Maybe FilePath
forall a. Maybe a
Nothing
        , optProblem :: WCNF
optProblem =
            WCNF :: Lit -> Lit -> Weight -> [WeightedClause] -> WCNF
CNF.WCNF
            { wcnfNumVars :: Lit
CNF.wcnfNumVars    = Lit
0
            , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = Lit
0
            , wcnfTopCost :: Weight
CNF.wcnfTopCost    = Weight
1
            , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses    = []
            }
        , optProblemFile :: Maybe FilePath
optProblemFile   = Maybe FilePath
forall a. Maybe a
Nothing
        , optVarInit :: [Lit]
optVarInit = []
        }

ubcsatBestFeasible :: Options -> IO (Maybe (Integer, SAT.Model))
ubcsatBestFeasible :: Options -> IO (Maybe (Weight, Model))
ubcsatBestFeasible Options
opt = do
  Maybe (Weight, Model)
ret <- Options -> IO (Maybe (Weight, Model))
ubcsatBest Options
opt
  case Maybe (Weight, Model)
ret of
    Maybe (Weight, Model)
Nothing -> Maybe (Weight, Model) -> IO (Maybe (Weight, Model))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Weight, Model)
forall a. Maybe a
Nothing
    Just (Weight
obj,Model
_) ->
      if Weight
obj Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
< WCNF -> Weight
CNF.wcnfTopCost (Options -> WCNF
optProblem Options
opt) then
        Maybe (Weight, Model) -> IO (Maybe (Weight, Model))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Weight, Model)
ret
      else
        Maybe (Weight, Model) -> IO (Maybe (Weight, Model))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Weight, Model)
forall a. Maybe a
Nothing

ubcsatBest :: Options -> IO (Maybe (Integer, SAT.Model))
ubcsatBest :: Options -> IO (Maybe (Weight, Model))
ubcsatBest Options
opt = do
  [(Weight, Model)]
sols <- Options -> IO [(Weight, Model)]
ubcsatMany Options
opt
  case [(Weight, Model)]
sols of
    [] -> Maybe (Weight, Model) -> IO (Maybe (Weight, Model))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Weight, Model)
forall a. Maybe a
Nothing
    [(Weight, Model)]
_ -> Maybe (Weight, Model) -> IO (Maybe (Weight, Model))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Weight, Model) -> IO (Maybe (Weight, Model)))
-> Maybe (Weight, Model) -> IO (Maybe (Weight, Model))
forall a b. (a -> b) -> a -> b
$ (Weight, Model) -> Maybe (Weight, Model)
forall a. a -> Maybe a
Just ((Weight, Model) -> Maybe (Weight, Model))
-> (Weight, Model) -> Maybe (Weight, Model)
forall a b. (a -> b) -> a -> b
$ ((Weight, Model) -> (Weight, Model) -> Ordering)
-> [(Weight, Model)] -> (Weight, Model)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (Weight -> Weight -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Weight -> Weight -> Ordering)
-> ((Weight, Model) -> Weight)
-> (Weight, Model)
-> (Weight, Model)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Weight, Model) -> Weight
forall a b. (a, b) -> a
fst) [(Weight, Model)]
sols

ubcsatMany :: Options -> IO [(Integer, SAT.Model)]
ubcsatMany :: Options -> IO [(Weight, Model)]
ubcsatMany Options
opt = do
  FilePath
dir <- case Options -> Maybe FilePath
optTempDir Options
opt of
           Just FilePath
dir -> FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
dir
           Maybe FilePath
Nothing -> IO FilePath
getTemporaryDirectory

  let f :: FilePath -> IO [(Weight, Model)]
f FilePath
fname
        | [Lit] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Options -> [Lit]
optVarInit Options
opt) = Options -> FilePath -> Maybe FilePath -> IO [(Weight, Model)]
ubcsat' Options
opt FilePath
fname Maybe FilePath
forall a. Maybe a
Nothing
        | Bool
otherwise = do
            FilePath
-> FilePath
-> (FilePath -> Handle -> IO [(Weight, Model)])
-> IO [(Weight, Model)]
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
FilePath -> FilePath -> (FilePath -> Handle -> m a) -> m a
withTempFile FilePath
dir FilePath
".txt" ((FilePath -> Handle -> IO [(Weight, Model)])
 -> IO [(Weight, Model)])
-> (FilePath -> Handle -> IO [(Weight, Model)])
-> IO [(Weight, Model)]
forall a b. (a -> b) -> a -> b
$ \FilePath
varInitFile Handle
h -> do
              Handle -> Bool -> IO ()
hSetBinaryMode Handle
h Bool
True
              Handle -> BufferMode -> IO ()
hSetBuffering Handle
h (Maybe Lit -> BufferMode
BlockBuffering Maybe Lit
forall a. Maybe a
Nothing)
              [[Lit]] -> ([Lit] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Lit -> [Lit] -> [[Lit]]
forall a. Lit -> [a] -> [[a]]
split Lit
10 (Options -> [Lit]
optVarInit Options
opt)) (([Lit] -> IO ()) -> IO ()) -> ([Lit] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \[Lit]
xs -> do
                Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords ((Lit -> FilePath) -> [Lit] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> FilePath
forall a. Show a => a -> FilePath
show [Lit]
xs)
              Handle -> IO ()
hClose Handle
h
              Options -> FilePath -> Maybe FilePath -> IO [(Weight, Model)]
ubcsat' Options
opt FilePath
fname (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
varInitFile)

  case Options -> Maybe FilePath
optProblemFile Options
opt of
    Just FilePath
fname -> FilePath -> IO [(Weight, Model)]
f FilePath
fname
    Maybe FilePath
Nothing -> do
      FilePath
-> FilePath
-> (FilePath -> Handle -> IO [(Weight, Model)])
-> IO [(Weight, Model)]
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
FilePath -> FilePath -> (FilePath -> Handle -> m a) -> m a
withTempFile FilePath
dir FilePath
".wcnf" ((FilePath -> Handle -> IO [(Weight, Model)])
 -> IO [(Weight, Model)])
-> (FilePath -> Handle -> IO [(Weight, Model)])
-> IO [(Weight, Model)]
forall a b. (a -> b) -> a -> b
$ \FilePath
fname Handle
h -> do
        Handle -> IO ()
hClose Handle
h
        FilePath -> WCNF -> IO ()
forall a (m :: * -> *).
(FileFormat a, MonadIO m) =>
FilePath -> a -> m ()
CNF.writeFile FilePath
fname (Options -> WCNF
optProblem Options
opt)
        FilePath -> IO [(Weight, Model)]
f FilePath
fname

ubcsat' :: Options -> FilePath -> Maybe FilePath -> IO [(Integer, SAT.Model)]
ubcsat' :: Options -> FilePath -> Maybe FilePath -> IO [(Weight, Model)]
ubcsat' Options
opt FilePath
fname Maybe FilePath
varInitFile = do
  let wcnf :: WCNF
wcnf = Options -> WCNF
optProblem Options
opt
  let args :: [FilePath]
args =
        [ FilePath
"-w" | FilePath
".wcnf" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower FilePath
fname] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
        [ FilePath
"-alg", FilePath
"irots"
        , FilePath
"-seed", FilePath
"0"
        , FilePath
"-runs", FilePath
"10"
        , FilePath
"-cutoff", Lit -> FilePath
forall a. Show a => a -> FilePath
show (WCNF -> Lit
CNF.wcnfNumVars WCNF
wcnf Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
* Lit
50)
        , FilePath
"-timeout", Lit -> FilePath
forall a. Show a => a -> FilePath
show (Lit
10 :: Int)
        , FilePath
"-gtimeout", Lit -> FilePath
forall a. Show a => a -> FilePath
show (Lit
30 :: Int)
        , FilePath
"-solve"
        , FilePath
"-r", FilePath
"bestsol"
        , FilePath
"-inst", FilePath
fname
        ] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
        (case Maybe FilePath
varInitFile of
           Maybe FilePath
Nothing -> []
           Just FilePath
fname2 -> [FilePath
"-varinitfile", FilePath
fname2])
      stdinStr :: FilePath
stdinStr = FilePath
""

  FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"c Running " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show (Options -> FilePath
optCommand Options
opt) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" with " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. Show a => a -> FilePath
show [FilePath]
args
  Either IOError FilePath
ret <- IO FilePath -> IO (Either IOError FilePath)
forall e a. Exception e => IO a -> IO (Either e a)
try (IO FilePath -> IO (Either IOError FilePath))
-> IO FilePath -> IO (Either IOError FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath] -> FilePath -> IO FilePath
readProcess (Options -> FilePath
optCommand Options
opt) [FilePath]
args FilePath
stdinStr
  case Either IOError FilePath
ret of
    Left (IOError
err :: IOError) -> do
      [FilePath] -> (FilePath -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (FilePath -> [FilePath]
lines (IOError -> FilePath
forall a. Show a => a -> FilePath
show IOError
err)) ((FilePath -> IO ()) -> IO ()) -> (FilePath -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FilePath
l -> do
        FilePath -> IO ()
putStr FilePath
"c " IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FilePath -> IO ()
putStrLn FilePath
l
      [(Weight, Model)] -> IO [(Weight, Model)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Right FilePath
s -> do
      [FilePath] -> (FilePath -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (FilePath -> [FilePath]
lines FilePath
s) ((FilePath -> IO ()) -> IO ()) -> (FilePath -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FilePath
l -> FilePath -> IO ()
putStr FilePath
"c " IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FilePath -> IO ()
putStrLn FilePath
l
      [(Weight, Model)] -> IO [(Weight, Model)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Weight, Model)] -> IO [(Weight, Model)])
-> [(Weight, Model)] -> IO [(Weight, Model)]
forall a b. (a -> b) -> a -> b
$ Lit -> FilePath -> [(Weight, Model)]
scanSolutions (WCNF -> Lit
CNF.wcnfNumVars WCNF
wcnf) FilePath
s

scanSolutions :: Int -> String -> [(Integer, SAT.Model)]
scanSolutions :: Lit -> FilePath -> [(Weight, Model)]
scanSolutions Lit
nv FilePath
s = [Either (ParseErrorBundle FilePath Void) (Weight, Model)]
-> [(Weight, Model)]
forall a b. [Either a b] -> [b]
rights ([Either (ParseErrorBundle FilePath Void) (Weight, Model)]
 -> [(Weight, Model)])
-> [Either (ParseErrorBundle FilePath Void) (Weight, Model)]
-> [(Weight, Model)]
forall a b. (a -> b) -> a -> b
$ (FilePath
 -> Either (ParseErrorBundle FilePath Void) (Weight, Model))
-> [FilePath]
-> [Either (ParseErrorBundle FilePath Void) (Weight, Model)]
forall a b. (a -> b) -> [a] -> [b]
map (Parsec Void FilePath (Weight, Model)
-> FilePath
-> FilePath
-> Either (ParseErrorBundle FilePath Void) (Weight, Model)
forall e s a.
Parsec e s a -> FilePath -> s -> Either (ParseErrorBundle s e) a
parse (Lit -> Parsec Void FilePath (Weight, Model)
forall (m :: * -> *).
MonadParsec Void FilePath m =>
Lit -> m (Weight, Model)
solution Lit
nv) FilePath
"") ([FilePath]
 -> [Either (ParseErrorBundle FilePath Void) (Weight, Model)])
-> [FilePath]
-> [Either (ParseErrorBundle FilePath Void) (Weight, Model)]
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath]
lines FilePath
s

solution :: MonadParsec Void String m => Int -> m (Integer, SAT.Model)
solution :: Lit -> m (Weight, Model)
solution Lit
nv = do
  m Char -> m ()
forall (m :: * -> *) a. MonadPlus m => m a -> m ()
skipSome m Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
digitChar
  m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Char
_ <- Token FilePath -> m (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token FilePath
'0' m Char -> m Char -> m Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token FilePath -> m (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token FilePath
'1'
  m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Weight
obj <- (FilePath -> Weight) -> m FilePath -> m Weight
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FilePath -> Weight
forall a. Read a => FilePath -> a
read (m FilePath -> m Weight) -> m FilePath -> m Weight
forall a b. (a -> b) -> a -> b
$ m Char -> m FilePath
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some m Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
digitChar
  m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  [Bool]
values <- m Bool -> m [Bool]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ((Token FilePath -> m (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token FilePath
'0' m Char -> m Bool -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) m Bool -> m Bool -> m Bool
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token FilePath -> m (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token FilePath
'1' m Char -> m Bool -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True))
  let m :: Model
m = (Lit, Lit) -> [(Lit, Bool)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1, Lit
nv) ([Lit] -> [Bool] -> [(Lit, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Lit
1..] [Bool]
values)
  (Weight, Model) -> m (Weight, Model)
forall (m :: * -> *) a. Monad m => a -> m a
return (Weight
obj, Model
m)


split :: Int -> [a] -> [[a]]
split :: Lit -> [a] -> [[a]]
split Lit
n = [a] -> [[a]]
forall a. [a] -> [[a]]
go
  where
    go :: [a] -> [[a]]
go [] = []
    go [a]
xs =
      case Lit -> [a] -> ([a], [a])
forall a. Lit -> [a] -> ([a], [a])
splitAt Lit
n [a]
xs of
        ([a]
ys, [a]
zs) -> [a]
ys [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> [[a]]
go [a]
zs