{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
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
#if MIN_VERSION_megaparsec(6,0,0)
import Data.Void
#endif
import System.Directory
import System.IO
import System.IO.Temp
import System.Process
import Text.Megaparsec hiding (try)
#if MIN_VERSION_megaparsec(6,0,0)
import Text.Megaparsec.Char
#else
import Text.Megaparsec.String
#endif
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
#if MIN_VERSION_megaparsec(6,0,0)
solution :: MonadParsec Void String m => Int -> m (Integer, SAT.Model)
#else
solution :: Int -> Parser (Integer, SAT.Model)
#endif
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