{-# 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 -> String
optCommand :: FilePath
  , Options -> Maybe String
optTempDir :: Maybe FilePath
  , Options -> WCNF
optProblem :: CNF.WCNF
  , Options -> Maybe String
optProblemFile :: Maybe FilePath
  , Options -> [Lit]
optVarInit :: [SAT.Lit]
  }

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

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

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

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

  let f :: String -> IO [(Integer, Model)]
f String
fname
        | [Lit] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Options -> [Lit]
optVarInit Options
opt) = Options -> String -> Maybe String -> IO [(Integer, Model)]
ubcsat' Options
opt String
fname Maybe String
forall a. Maybe a
Nothing
        | Bool
otherwise = do
            String
-> String
-> (String -> Handle -> IO [(Integer, Model)])
-> IO [(Integer, Model)]
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
String -> String -> (String -> Handle -> m a) -> m a
withTempFile String
dir String
".txt" ((String -> Handle -> IO [(Integer, Model)])
 -> IO [(Integer, Model)])
-> (String -> Handle -> IO [(Integer, Model)])
-> IO [(Integer, Model)]
forall a b. (a -> b) -> a -> b
$ \String
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 -> String -> IO ()
hPutStrLn Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ((Lit -> String) -> [Lit] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> String
forall a. Show a => a -> String
show [Lit]
xs)
              Handle -> IO ()
hClose Handle
h
              Options -> String -> Maybe String -> IO [(Integer, Model)]
ubcsat' Options
opt String
fname (String -> Maybe String
forall a. a -> Maybe a
Just String
varInitFile)

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

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

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

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

solution :: MonadParsec Void String m => Int -> m (Integer, SAT.Model)
solution :: forall (m :: * -> *).
MonadParsec Void String m =>
Lit -> m (Integer, Model)
solution Lit
nv = do
  m Char -> m ()
forall (m :: * -> *) a. MonadPlus m => m a -> m ()
skipSome m Char
m (Token String)
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 String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'0' m Char -> m Char -> m Char
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'1'
  m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Integer
obj <- (String -> Integer) -> m String -> m Integer
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Integer
forall a. Read a => String -> a
read (m String -> m Integer) -> m String -> m Integer
forall a b. (a -> b) -> a -> b
$ m Char -> m String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some m Char
m (Token String)
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 String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'0' m Char -> m Bool -> m Bool
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) m Bool -> m Bool -> m Bool
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'1' m Char -> m Bool -> m Bool
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall a. a -> m a
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)
  (Integer, Model) -> m (Integer, Model)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
obj, Model
m)


split :: Int -> [a] -> [[a]]
split :: forall a. 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