toysolver-0.5.0: app/toysat/toysat.hs
{-# LANGUAGE ScopedTypeVariables, CPP #-}
{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
-----------------------------------------------------------------------------
-- |
-- Module : toysat
-- Copyright : (c) Masahiro Sakai 2012-2014
-- License : BSD-style
--
-- Maintainer : masahiro.sakai@gmail.com
-- Stability : experimental
-- Portability : non-portable (ScopedTypeVariables, CPP)
--
-- A toy-level SAT solver based on CDCL.
--
-----------------------------------------------------------------------------
module Main where
import Control.Applicative ((<$>))
import Control.Concurrent (getNumCapabilities)
import Control.Concurrent.Timeout
import Control.Monad
import Control.Exception
import Data.Array.IArray
import Data.Array.IO
import qualified Data.ByteString.Lazy as BS
import Data.Default.Class
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Foldable as F
import qualified Data.Traversable as T
import Data.Char
import Data.IORef
import Data.List
import Data.Maybe
import Data.Ord
import Data.Word
import qualified Data.Vector.Unboxed as V
import Data.Version
import Data.Scientific as Scientific
import Data.Time
import System.IO
import System.Environment
import System.Exit
#if !MIN_VERSION_time(1,5,0)
import System.Locale (defaultTimeLocale)
#endif
import System.Clock
import System.Console.GetOpt
import System.FilePath
import qualified System.Info as SysInfo
import qualified System.Random.MWC as Rand
import Text.Printf
#ifdef __GLASGOW_HASKELL__
import GHC.Environment (getFullArgs)
#endif
#if defined(__GLASGOW_HASKELL__)
import qualified GHC.Stats as Stats
#endif
import qualified Data.PseudoBoolean as PBFile
import qualified Data.PseudoBoolean.Attoparsec as PBFileAttoparsec
import qualified ToySolver.Data.MIP as MIP
import qualified ToySolver.Data.MIP.Solution.Gurobi as GurobiSol
import qualified ToySolver.Converter.GCNF2MaxSAT as GCNF2MaxSAT
import qualified ToySolver.Converter.MaxSAT2WBO as MaxSAT2WBO
import qualified ToySolver.Converter.MIP2PB as MIP2PB
import qualified ToySolver.Converter.PB2SAT as PB2SAT
import qualified ToySolver.Converter.PB2WBO as PB2WBO
import qualified ToySolver.Converter.WBO2MaxSAT as WBO2MaxSAT
import qualified ToySolver.Converter.WBO2PB as WBO2PB
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO as PBO
import qualified ToySolver.SAT.Encoder.Integer as Integer
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
import qualified ToySolver.SAT.MessagePassing.SurveyPropagation as SP
import qualified ToySolver.SAT.MUS as MUS
import qualified ToySolver.SAT.MUS.Enum as MUSEnum
import ToySolver.SAT.Printer
import qualified ToySolver.Text.CNF as CNF
import qualified ToySolver.Text.MaxSAT as MaxSAT
import qualified ToySolver.Text.GCNF as GCNF
import ToySolver.Version
import ToySolver.Internal.Util (showRational, setEncodingChar8)
import qualified UBCSAT
-- ------------------------------------------------------------------------
data Mode = ModeHelp | ModeVersion | ModeSAT | ModeMUS | ModePB | ModeWBO | ModeMaxSAT | ModeMIP
data Options
= Options
{ optMode :: Maybe Mode
, optSATConfig :: SAT.Config
, optRandomSeed :: Maybe Rand.Seed
, optLinearizerPB :: Bool
, optOptMethod :: PBO.Method
, optObjFunVarsHeuristics :: Bool
, optLocalSearchInitial :: Bool
, optMUSMethod :: MUS.Method
, optAllMUSes :: Bool
, optAllMUSMethod :: MUSEnum.Method
, optPrintRational :: Bool
, optTimeout :: Integer
, optWriteFile :: Maybe FilePath
, optUBCSAT :: FilePath
, optInitSP :: Bool
, optTempDir :: Maybe FilePath
, optFileEncoding :: Maybe String
}
instance Default Options where
def =
Options
{ optMode = Nothing
, optSATConfig = def
, optRandomSeed = Nothing
, optLinearizerPB = False
, optOptMethod = def
, optObjFunVarsHeuristics = PBO.defaultEnableObjFunVarsHeuristics
, optLocalSearchInitial = False
, optMUSMethod = MUS.optMethod def
, optAllMUSes = False
, optAllMUSMethod = MUSEnum.optMethod def
, optPrintRational = False
, optTimeout = 0
, optWriteFile = Nothing
, optUBCSAT = "ubcsat"
, optInitSP = False
, optTempDir = Nothing
, optFileEncoding = Nothing
}
options :: [OptDescr (Options -> Options)]
options =
[ Option ['h'] ["help"] (NoArg (\opt -> opt{ optMode = Just ModeHelp })) "show help"
, Option [] ["version"] (NoArg (\opt -> opt{ optMode = Just ModeVersion})) "show version"
, Option [] ["sat"] (NoArg (\opt -> opt{ optMode = Just ModeSAT })) "solve boolean satisfiability problem in .cnf file (default)"
, Option [] ["mus"] (NoArg (\opt -> opt{ optMode = Just ModeMUS })) "solve minimally unsatisfiable subset problem in .gcnf or .cnf file"
, Option [] ["pb"] (NoArg (\opt -> opt{ optMode = Just ModePB })) "solve pseudo boolean problem in .opb file"
, Option [] ["wbo"] (NoArg (\opt -> opt{ optMode = Just ModeWBO })) "solve weighted boolean optimization problem in .wbo file"
, Option [] ["maxsat"] (NoArg (\opt -> opt{ optMode = Just ModeMaxSAT })) "solve MaxSAT problem in .cnf or .wcnf file"
, Option [] ["lp"] (NoArg (\opt -> opt{ optMode = Just ModeMIP })) "solve bounded integer programming problem in .lp or .mps file"
, Option [] ["restart"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configRestartStrategy = parseRestartStrategy val } }) "<str>")
("Restart startegy: " ++ intercalate ", "
[ SAT.showRestartStrategy s ++ (if SAT.configRestartStrategy (optSATConfig def) == s then " (default)" else "")
| s <- [minBound .. maxBound] ])
, Option [] ["restart-first"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configRestartFirst = read val } }) "<int>")
(printf "The initial restart limit. (default %d)" (SAT.configRestartFirst def))
, Option [] ["restart-inc"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configRestartInc = read val } }) "<real>")
(printf "The factor with which the restart limit is multiplied in each restart. (default %f)" (SAT.configRestartInc def))
, Option [] ["learning"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configLearningStrategy = parseLearningStrategy val } }) "<str>")
("Leaning scheme: " ++ intercalate ", "
[ SAT.showLearningStrategy s ++ (if SAT.configLearningStrategy (optSATConfig def) == s then " (default)" else "")
| s <- [minBound .. maxBound] ])
, Option [] ["learnt-size-first"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configLearntSizeFirst = read val } }) "<int>")
"The initial limit for learnt clauses."
, Option [] ["learnt-size-inc"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configLearntSizeInc = read val } }) "<real>")
(printf "The limit for learnt clauses is multiplied with this factor periodically. (default %f)" (SAT.configLearntSizeInc def))
, Option [] ["branch"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configBranchingStrategy = parseBranchingStrategy val } }) "<str>")
("Branching startegy: " ++ intercalate ", "
[ SAT.showBranchingStrategy s ++ (if SAT.configBranchingStrategy (optSATConfig def) == s then " (default)" else "")
| s <- [minBound .. maxBound] ])
, Option [] ["erwa-alpha-first"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configERWAStepSizeFirst = read val } }) "<real>")
(printf "step-size alpha in ERWA and LRB branching heuristic is initialized with this value. (default %f)" (SAT.configERWAStepSizeFirst def))
, Option [] ["erwa-alpha-dec"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configERWAStepSizeDec = read val } }) "<real>")
(printf "step-size alpha in ERWA and LRB branching heuristic is decreased by this value after each conflict. (default %f)" (SAT.configERWAStepSizeDec def))
, Option [] ["erwa-alpha-min"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configERWAStepSizeMin = read val } }) "<real>")
(printf "step-size alpha in ERWA and LRB branching heuristic is decreased until it reach the value. (default %f)" (SAT.configERWAStepSizeMin def))
, Option [] ["ema-decay"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEMADecay = read val } }) "<real>")
(printf "inverse of the variable EMA decay factor used by LRB branching heuristic. (default %f)" (SAT.configEMADecay def))
, Option [] ["ccmin"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configCCMin = read val } }) "<int>")
(printf "Conflict clause minimization (0=none, 1=local, 2=recursive; default %d)" (SAT.configCCMin def))
, Option [] ["enable-phase-saving"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnablePhaseSaving = True } }))
("Enable phase saving" ++ (if SAT.configEnablePhaseSaving def then " (default)" else ""))
, Option [] ["disable-phase-saving"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnablePhaseSaving = False } }))
("Disable phase saving" ++ (if SAT.configEnablePhaseSaving def then "" else " (default)"))
, Option [] ["enable-forward-subsumption-removal"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnableForwardSubsumptionRemoval = True } }))
("Enable forward subumption removal (clauses only)" ++ (if SAT.configEnableForwardSubsumptionRemoval def then " (default)" else ""))
, Option [] ["disable-forward-subsumption-removal"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnableForwardSubsumptionRemoval = False } }))
("Disable forward subsumption removal (clauses only)" ++ (if SAT.configEnableForwardSubsumptionRemoval def then "" else " (default)"))
, Option [] ["enable-backward-subsumption-removal"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnableBackwardSubsumptionRemoval = True } }))
("Enable backward subsumption removal." ++ (if SAT.configEnableBackwardSubsumptionRemoval def then " (default)" else ""))
, Option [] ["disable-backward-subsumption-removal"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnableBackwardSubsumptionRemoval = False } }))
("Disable backward subsumption removal." ++ (if SAT.configEnableBackwardSubsumptionRemoval def then "" else " (default)"))
, Option [] ["random-freq"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configRandomFreq = read val } }) "<0..1>")
(printf "The frequency with which the decision heuristic tries to choose a random variable (default %f)" (SAT.configRandomFreq def))
, Option [] ["random-seed"]
(ReqArg (\val opt -> opt{ optRandomSeed = Just (Rand.toSeed (V.singleton (read val) :: V.Vector Word32)) }) "<int>")
"random seed used by the random variable selection"
, Option [] ["random-gen"]
(ReqArg (\val opt -> opt{ optRandomSeed = Just (Rand.toSeed (V.fromList (map read $ words $ val) :: V.Vector Word32)) }) "<str>")
"another way of specifying random seed used by the random variable selection"
, Option [] ["init-sp"]
(NoArg (\opt -> opt{ optInitSP = True }))
"Use survey propation to compute initial polarity (when possible)"
, Option [] ["linearizer-pb"]
(NoArg (\opt -> opt{ optLinearizerPB = True }))
"Use PB constraint in linearization."
, Option [] ["pb-handler"]
(ReqArg (\val opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configPBHandlerType = parsePBHandler val } }) "<str>")
("PB constraint handler: " ++ intercalate ", "
[ SAT.showPBHandlerType h ++ (if SAT.configPBHandlerType (optSATConfig def) == h then " (default)" else "")
| h <- [minBound .. maxBound] ])
, Option [] ["pb-split-clause-part"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnablePBSplitClausePart = True } }))
("Split clause part of PB constraints." ++ (if SAT.configEnablePBSplitClausePart def then " (default)" else ""))
, Option [] ["no-pb-split-clause-part"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configEnablePBSplitClausePart = False } }))
("Do not split clause part of PB constraints." ++ (if SAT.configEnablePBSplitClausePart def then "" else " (default)"))
, Option [] ["opt-method"]
(ReqArg (\val opt -> opt{ optOptMethod = parseOptMethod val }) "<str>")
("Optimization method: " ++ intercalate ", "
[PBO.showMethod m ++ (if optOptMethod def == m then " (default)" else "") | m <- [minBound .. maxBound]])
, Option [] ["objfun-heuristics"]
(NoArg (\opt -> opt{ optObjFunVarsHeuristics = True }))
"Enable heuristics for polarity/activity of variables in objective function (default)"
, Option [] ["no-objfun-heuristics"]
(NoArg (\opt -> opt{ optObjFunVarsHeuristics = False }))
"Disable heuristics for polarity/activity of variables in objective function"
, Option [] ["ls-initial"]
(NoArg (\opt -> opt{ optLocalSearchInitial = True }))
"Use local search (currently UBCSAT) for finding initial solution"
, Option [] ["all-mus"]
(NoArg (\opt -> opt{ optMode = Just ModeMUS, optAllMUSes = True }))
"enumerate all MUSes"
, Option [] ["mus-method"]
(ReqArg (\val opt -> opt{ optMUSMethod = parseMUSMethod val }) "<str>")
("MUS computation method: " ++ intercalate ", "
[MUS.showMethod m ++ (if optMUSMethod def == m then " (default)" else "") | m <- [minBound .. maxBound]])
, Option [] ["all-mus-method"]
(ReqArg (\val opt -> opt{ optAllMUSMethod = parseAllMUSMethod val }) "<str>")
("MUS enumeration method: " ++ intercalate ", "
[MUSEnum.showMethod m ++ (if optAllMUSMethod def == m then " (default)" else "") | m <- [minBound .. maxBound]])
, Option [] ["print-rational"]
(NoArg (\opt -> opt{ optPrintRational = True }))
"print rational numbers instead of decimals"
, Option ['w'] []
(ReqArg (\val opt -> opt{ optWriteFile = Just val }) "<filename>")
"write model to filename in Gurobi .sol format"
, Option [] ["check-model"]
(NoArg (\opt -> opt{ optSATConfig = (optSATConfig opt){ SAT.configCheckModel = True } }))
"check model for debug"
, Option [] ["timeout"]
(ReqArg (\val opt -> opt{ optTimeout = read val }) "<int>")
"Kill toysat after given number of seconds (default 0 (no limit))"
, Option [] ["with-ubcsat"]
(ReqArg (\val opt -> opt{ optUBCSAT = val }) "<PATH>")
"give the path to the UBCSAT command"
, Option [] ["temp-dir"]
(ReqArg (\val opt -> opt{ optTempDir = Just val }) "<PATH>")
"temporary directory"
, Option [] ["encoding"]
(ReqArg (\val opt -> opt{ optFileEncoding = Just val }) "<ENCODING>")
"file encoding for LP/MPS files"
]
where
parseOptMethod s = fromMaybe (error (printf "unknown optimization method \"%s\"" s)) (PBO.parseMethod s)
parseMUSMethod s = fromMaybe (error (printf "unknown MUS finding method \"%s\"" s)) (MUS.parseMethod s)
parseAllMUSMethod s = fromMaybe (error (printf "unknown MUS enumeration method \"%s\"" s)) (MUSEnum.parseMethod s)
parseRestartStrategy s = fromMaybe (error (printf "unknown restart strategy \"%s\"" s)) (SAT.parseRestartStrategy s)
parseLearningStrategy s = fromMaybe (error (printf "unknown learning strategy \"%s\"" s)) (SAT.parseLearningStrategy s)
parseBranchingStrategy s = fromMaybe (error (printf "unknown branching strategy \"%s\"" s)) (SAT.parseBranchingStrategy s)
parsePBHandler s = fromMaybe (error (printf "unknown PB constraint handler \"%s\"" s)) (SAT.parsePBHandlerType s)
main :: IO ()
main = do
#ifdef FORCE_CHAR8
setEncodingChar8
#endif
startCPU <- getTime ProcessCPUTime
startWC <- getTime Monotonic
args <- getArgs
case getOpt Permute options args of
(_,_,errs@(_:_)) -> do
mapM_ putStrLn errs
exitFailure
(o,args2,[]) -> do
let opt = foldl (flip id) def o
mode =
case optMode opt of
Just m -> m
Nothing ->
case args2 of
[] -> ModeHelp
fname : _ ->
case map toLower (takeExtension fname) of
".cnf" -> ModeSAT
".gcnf" -> ModeMUS
".opb" -> ModePB
".wbo" -> ModeWBO
".wcnf" -> ModeMaxSAT
".lp" -> ModeMIP
".mps" -> ModeMIP
_ -> ModeSAT
case mode of
ModeHelp -> showHelp stdout
ModeVersion -> hPutStrLn stdout (showVersion version)
_ -> do
printSysInfo
#ifdef __GLASGOW_HASKELL__
fullArgs <- getFullArgs
#else
let fullArgs = args
#endif
putCommentLine $ printf "command line = %s" (show fullArgs)
let timelim = optTimeout opt * 10^(6::Int)
ret <- timeout (if timelim > 0 then timelim else (-1)) $ do
solver <- newSolver opt
case mode of
ModeHelp -> showHelp stdout
ModeVersion -> hPutStrLn stdout (showVersion version)
ModeSAT -> mainSAT opt solver args2
ModeMUS -> mainMUS opt solver args2
ModePB -> mainPB opt solver args2
ModeWBO -> mainWBO opt solver args2
ModeMaxSAT -> mainMaxSAT opt solver args2
ModeMIP -> mainMIP opt solver args2
when (isNothing ret) $ do
putCommentLine "TIMEOUT"
endCPU <- getTime ProcessCPUTime
endWC <- getTime Monotonic
putCommentLine $ printf "total CPU time = %.3fs" (durationSecs startCPU endCPU)
putCommentLine $ printf "total wall clock time = %.3fs" (durationSecs startWC endWC)
printGCStat
printGCStat :: IO ()
#if defined(__GLASGOW_HASKELL__)
#if __GLASGOW_HASKELL__ >= 802
printGCStat = do
b <- Stats.getRTSStatsEnabled
when b $ do
stat <- Stats.getRTSStats
putCommentLine "RTSStats:"
putCommentLine $ printf " gcs = %d" $ Stats.gcs stat
putCommentLine $ printf " major_gcs = %d" $ Stats.major_gcs stat
putCommentLine $ printf " allocated_bytes = %d" $ Stats.allocated_bytes stat
putCommentLine $ printf " max_live_bytes = %d" $ Stats.max_live_bytes stat
putCommentLine $ printf " max_large_objects_bytes = %d" $ Stats.max_large_objects_bytes stat
putCommentLine $ printf " max_compact_bytes = %d" $ Stats.max_compact_bytes stat
putCommentLine $ printf " max_slop_bytes = %d" $ Stats.max_slop_bytes stat
putCommentLine $ printf " max_mem_in_use_bytes = %d" $ Stats.max_mem_in_use_bytes stat
putCommentLine $ printf " cumulative_live_bytes = %d" $ Stats.cumulative_live_bytes stat
putCommentLine $ printf " copied_bytes = %d" $ Stats.copied_bytes stat
putCommentLine $ printf " par_copied_bytes = %d" $ Stats.par_copied_bytes stat
putCommentLine $ printf " cumulative_par_max_copied_bytes = %d" $ Stats.cumulative_par_max_copied_bytes stat
putCommentLine $ printf " mutator_cpu_ns = %d" $ Stats.mutator_cpu_ns stat
putCommentLine $ printf " mutator_elapsed_ns = %d" $ Stats.mutator_elapsed_ns stat
putCommentLine $ printf " gc_cpu_ns = %d" $ Stats.gc_cpu_ns stat
putCommentLine $ printf " gc_elapsed_ns = %d" $ Stats.gc_elapsed_ns stat
putCommentLine $ printf " cpu_ns = %d" $ Stats.cpu_ns stat
putCommentLine $ printf " elapsed_ns = %d" $ Stats.elapsed_ns stat
let gc = Stats.gc stat
putCommentLine $ " gc:"
putCommentLine $ printf " gen = %d" $ Stats.gcdetails_gen gc
putCommentLine $ printf " threads = %d" $ Stats.gcdetails_threads gc
putCommentLine $ printf " allocated_bytes = %d" $ Stats.gcdetails_allocated_bytes gc
putCommentLine $ printf " live_bytes = %d" $ Stats.gcdetails_live_bytes gc
putCommentLine $ printf " large_objects_bytes = %d" $ Stats.gcdetails_large_objects_bytes gc
putCommentLine $ printf " compact_bytes = %d" $ Stats.gcdetails_compact_bytes gc
putCommentLine $ printf " slop_bytes = %d" $ Stats.gcdetails_slop_bytes gc
putCommentLine $ printf " mem_in_use_bytes = %d" $ Stats.gcdetails_mem_in_use_bytes gc
putCommentLine $ printf " copied_bytes = %d" $ Stats.gcdetails_copied_bytes gc
putCommentLine $ printf " par_max_copied_bytes = %d" $ Stats.gcdetails_par_max_copied_bytes gc
putCommentLine $ printf " sync_elapsed_ns = %d" $ Stats.gcdetails_sync_elapsed_ns gc
putCommentLine $ printf " cpu_ns = %d" $ Stats.gcdetails_cpu_ns gc
putCommentLine $ printf " elapsed_ns = %d" $ Stats.gcdetails_elapsed_ns gc
#else
printGCStat = do
b <- Stats.getGCStatsEnabled
when b $ do
stat <- Stats.getGCStats
putCommentLine "GCStats:"
putCommentLine $ printf " bytesAllocated = %d" $ Stats.bytesAllocated stat
putCommentLine $ printf " numGcs = %d" $ Stats.numGcs stat
putCommentLine $ printf " maxBytesUsed = %d" $ Stats.maxBytesUsed stat
putCommentLine $ printf " numByteUsageSamples = %d" $ Stats.numByteUsageSamples stat
putCommentLine $ printf " cumulativeBytesUsed = %d" $ Stats.cumulativeBytesUsed stat
putCommentLine $ printf " bytesCopied = %d" $ Stats.bytesCopied stat
putCommentLine $ printf " currentBytesUsed = %d" $ Stats.currentBytesUsed stat
putCommentLine $ printf " currentBytesSlop = %d" $ Stats.currentBytesSlop stat
putCommentLine $ printf " maxBytesSlop = %d" $ Stats.maxBytesSlop stat
putCommentLine $ printf " peakMegabytesAllocated = %d" $ Stats.peakMegabytesAllocated stat
putCommentLine $ printf " mutatorCpuSeconds = %5.2f" $ Stats.mutatorCpuSeconds stat
putCommentLine $ printf " mutatorWallSeconds = %5.2f" $ Stats.mutatorWallSeconds stat
putCommentLine $ printf " gcCpuSeconds = %5.2f" $ Stats.gcCpuSeconds stat
putCommentLine $ printf " gcWallSeconds = %5.2f" $ Stats.gcWallSeconds stat
putCommentLine $ printf " cpuSeconds = %5.2f" $ Stats.cpuSeconds stat
putCommentLine $ printf " wallSeconds = %5.2f" $ Stats.wallSeconds stat
putCommentLine $ printf " parTotBytesCopied = %d" $ Stats.parTotBytesCopied stat
putCommentLine $ printf " parMaxBytesCopied = %d" $ Stats.parMaxBytesCopied stat
#endif
#else
printGCStat = return ()
#endif
showHelp :: Handle -> IO ()
showHelp h = hPutStrLn h (usageInfo header options)
header :: String
header = unlines
[ "Usage:"
, " toysat [OPTION]... [file.cnf|-]"
, " toysat [OPTION]... --mus [file.gcnf|-]"
, " toysat [OPTION]... --pb [file.opb|-]"
, " toysat [OPTION]... --wbo [file.wbo|-]"
, " toysat [OPTION]... --maxsat [file.cnf|file.wcnf|-]"
, " toysat [OPTION]... --lp [file.lp|file.mps|-]"
, ""
, "Options:"
]
printSysInfo :: IO ()
printSysInfo = do
tm <- getZonedTime
putCommentLine $ printf "%s" (formatTime defaultTimeLocale "%FT%X%z" tm)
putCommentLine $ printf "version = %s" (showVersion version)
putCommentLine $ printf "githash = %s" (fromMaybe "<unknown>" gitHash)
putCommentLine $ printf "compilationtime = %s" (show compilationTime)
putCommentLine $ printf "arch = %s" SysInfo.arch
putCommentLine $ printf "os = %s" SysInfo.os
putCommentLine $ printf "compiler = %s %s" SysInfo.compilerName (showVersion SysInfo.compilerVersion)
putCommentLine "packages:"
forM_ packageVersions $ \(package, ver) -> do
putCommentLine $ printf " %s-%s" package ver
putCommentLine :: String -> IO ()
putCommentLine s = do
putStr "c "
putStrLn s
hFlush stdout
putSLine :: String -> IO ()
putSLine s = do
putStr "s "
putStrLn s
hFlush stdout
putOLine :: String -> IO ()
putOLine s = do
putStr "o "
putStrLn s
hFlush stdout
newSolver :: Options -> IO SAT.Solver
newSolver opts = do
solver <- SAT.newSolverWithConfig (optSATConfig opts)
SAT.setLogger solver putCommentLine
case optRandomSeed opts of
Nothing -> SAT.setRandomGen solver =<< Rand.createSystemRandom
Just s -> SAT.setRandomGen solver =<< Rand.initialize (Rand.fromSeed s)
do gen <- SAT.getRandomGen solver
s <- Rand.save gen
putCommentLine $ "use --random-gen=" ++ show (unwords . map show . V.toList . Rand.fromSeed $ s) ++ " option to reproduce the execution"
return solver
-- ------------------------------------------------------------------------
mainSAT :: Options -> SAT.Solver -> [String] -> IO ()
mainSAT opt solver args = do
ret <- case args of
["-"] -> liftM CNF.parseByteString $ BS.hGetContents stdin
[fname] -> CNF.parseFile fname
_ -> showHelp stderr >> exitFailure
case ret of
Left err -> hPrint stderr err >> exitFailure
Right cnf -> do
let fname = case args of
[fname] | or [".cnf" `isSuffixOf` map toLower fname] -> Just fname
_ -> Nothing
solveSAT opt solver cnf fname
solveSAT :: Options -> SAT.Solver -> CNF.CNF -> Maybe FilePath -> IO ()
solveSAT opt solver cnf cnfFileName = do
putCommentLine $ printf "#vars %d" (CNF.numVars cnf)
putCommentLine $ printf "#constraints %d" (CNF.numClauses cnf)
SAT.newVars_ solver (CNF.numVars cnf)
forM_ (CNF.clauses cnf) $ \clause ->
SAT.addClause solver clause
spHighlyBiased <-
if optInitSP opt then do
initPolarityUsingSP solver (CNF.numVars cnf)
(CNF.numVars cnf) [(1, clause) | clause <- CNF.clauses cnf]
else
return IntMap.empty
when (optLocalSearchInitial opt) $ do
fixed <- SAT.getFixedLiterals solver
let var_init1 = IntMap.fromList [(abs lit, lit > 0) | lit <- fixed, abs lit <= CNF.numVars cnf]
var_init2 = IntMap.map (>0) spHighlyBiased
-- note that IntMap.union is left-biased.
var_init = [if b then v else -v | (v, b) <- IntMap.toList (var_init1 `IntMap.union` var_init2)]
let wcnf =
MaxSAT.WCNF
{ MaxSAT.numVars = CNF.numVars cnf
, MaxSAT.numClauses = CNF.numClauses cnf
, MaxSAT.topCost = 1
, MaxSAT.clauses = [(1, clause) | clause <- CNF.clauses cnf]
}
let opt2 =
def
{ UBCSAT.optCommand = optUBCSAT opt
, UBCSAT.optTempDir = optTempDir opt
, UBCSAT.optProblem = wcnf
, UBCSAT.optProblemFile = cnfFileName
, UBCSAT.optVarInit = var_init
}
ret <- UBCSAT.ubcsatBest opt2
case ret of
Nothing -> return ()
Just (_,m) -> do
forM_ (assocs m) $ \(v, val) -> do
SAT.setVarPolarity solver v val
result <- SAT.solve solver
putSLine $ if result then "SATISFIABLE" else "UNSATISFIABLE"
when result $ do
m <- SAT.getModel solver
satPrintModel stdout m (CNF.numVars cnf)
writeSOLFile opt m Nothing (CNF.numVars cnf)
initPolarityUsingSP :: SAT.Solver -> Int -> Int -> [(Double, SAT.Clause)] -> IO (IntMap Double)
initPolarityUsingSP solver nvOrig nv clauses = do
n <- getNumCapabilities
putCommentLine $ "Running survey propgation using " ++ show n ++" threads ..."
startWC <- getTime Monotonic
sp <- SP.newSolver nv clauses
SP.initializeRandom sp =<< SAT.getRandomGen solver
SP.setNThreads sp n
lits <- SAT.getFixedLiterals solver
forM_ lits $ \lit -> do
when (abs lit <= nvOrig) $ SP.fixLit sp lit
b <- SP.propagate sp
endWC <- getTime Monotonic
if b then do
putCommentLine $ printf "Survey propagation converged in %.3fs" (durationSecs startWC endWC)
xs <- liftM catMaybes $ forM [1 .. nvOrig] $ \v -> do
(pt,pf,_)<- SP.getVarProb sp v
let bias = pt - pf
SAT.setVarPolarity solver v (bias >= 0)
if abs bias > 0.3 then
return $ Just (v, bias)
else
return Nothing
forM_ (zip (sortBy (comparing (abs . snd)) xs) [1..]) $ \((v,_),w) -> do
replicateM w $ SAT.varBumpActivity solver v
return $ IntMap.fromList xs
else do
putCommentLine $ printf "Survey propagation did not converge"
return $ IntMap.empty
-- ------------------------------------------------------------------------
mainMUS :: Options -> SAT.Solver -> [String] -> IO ()
mainMUS opt solver args = do
gcnf <- case args of
["-"] -> do
s <- BS.hGetContents stdin
case GCNF.parseByteString s of
Left err -> hPutStrLn stderr err >> exitFailure
Right gcnf -> return gcnf
[fname] -> do
ret <- GCNF.parseFile fname
case ret of
Left err -> hPutStrLn stderr err >> exitFailure
Right gcnf -> return gcnf
_ -> showHelp stderr >> exitFailure
solveMUS opt solver gcnf
solveMUS :: Options -> SAT.Solver -> GCNF.GCNF -> IO ()
solveMUS opt solver gcnf = do
putCommentLine $ printf "#vars %d" (GCNF.numVars gcnf)
putCommentLine $ printf "#constraints %d" (GCNF.numClauses gcnf)
putCommentLine $ printf "#groups %d" (GCNF.lastGroupIndex gcnf)
SAT.resizeVarCapacity solver (GCNF.numVars gcnf + GCNF.lastGroupIndex gcnf)
SAT.newVars_ solver (GCNF.numVars gcnf)
tbl <- forM [1 .. GCNF.lastGroupIndex gcnf] $ \i -> do
sel <- SAT.newVar solver
return (i, sel)
let idx2sel :: Array Int SAT.Var
idx2sel = array (1, GCNF.lastGroupIndex gcnf) tbl
selrng = if null tbl then (0,-1) else (snd $ head tbl, snd $ last tbl)
sel2idx :: Array SAT.Lit Int
sel2idx = array selrng [(sel, idx) | (idx, sel) <- tbl]
(idx2clausesM :: IOArray Int [SAT.Clause]) <- newArray (1, GCNF.lastGroupIndex gcnf) []
forM_ (GCNF.clauses gcnf) $ \(idx, clause) ->
if idx==0
then SAT.addClause solver clause
else do
SAT.addClause solver (- (idx2sel ! idx) : clause)
cs <- readArray idx2clausesM idx
writeArray idx2clausesM idx (clause : cs)
(idx2clauses :: Array Int [SAT.Clause]) <- freeze idx2clausesM
when (optInitSP opt) $ do
let wcnf = GCNF2MaxSAT.convert gcnf
initPolarityUsingSP solver (GCNF.numVars gcnf)
(MaxSAT.numVars wcnf) [(fromIntegral w, clause) | (w, clause) <- MaxSAT.clauses wcnf]
return ()
result <- SAT.solveWith solver (map (idx2sel !) [1..GCNF.lastGroupIndex gcnf])
putSLine $ if result then "SATISFIABLE" else "UNSATISFIABLE"
if result
then do
m <- SAT.getModel solver
satPrintModel stdout m (GCNF.numVars gcnf)
writeSOLFile opt m Nothing (GCNF.numVars gcnf)
else do
if not (optAllMUSes opt)
then do
let opt2 = def
{ MUS.optMethod = optMUSMethod opt
, MUS.optLogger = putCommentLine
, MUS.optShowLit = \lit -> show (sel2idx ! lit)
, MUS.optEvalConstr = \m sel ->
and [SAT.evalClause m c | c <- idx2clauses ! (sel2idx ! sel)]
}
mus <- MUS.findMUSAssumptions solver opt2
let mus2 = sort $ map (sel2idx !) $ IntSet.toList mus
musPrintSol stdout mus2
else do
musCounter <- newIORef 1
mcsCounter <- newIORef 1
let opt2 = def
{ MUSEnum.optMethod = optAllMUSMethod opt
, MUSEnum.optLogger = putCommentLine
, MUSEnum.optShowLit = \lit -> show (sel2idx ! lit)
, MUSEnum.optEvalConstr = \m sel ->
and [SAT.evalClause m c | c <- idx2clauses ! (sel2idx ! sel)]
, MUSEnum.optOnMCSFound = \mcs -> do
i <- readIORef mcsCounter
modifyIORef' mcsCounter (+1)
let mcs2 = sort $ map (sel2idx !) $ IntSet.toList mcs
putCommentLine $ "MCS #" ++ show (i :: Int) ++ ": " ++ intercalate " " (map show mcs2)
, MUSEnum.optOnMUSFound = \mus -> do
i <- readIORef musCounter
modifyIORef' musCounter (+1)
putCommentLine $ "MUS #" ++ show (i :: Int)
let mus2 = sort $ map (sel2idx !) $ IntSet.toList mus
musPrintSol stdout mus2
}
MUSEnum.allMUSAssumptions solver (map snd tbl) opt2
return ()
-- ------------------------------------------------------------------------
mainPB :: Options -> SAT.Solver -> [String] -> IO ()
mainPB opt solver args = do
ret <- case args of
["-"] -> liftM PBFileAttoparsec.parseOPBByteString $ BS.hGetContents stdin
[fname] -> PBFileAttoparsec.parseOPBFile fname
_ -> showHelp stderr >> exitFailure
case ret of
Left err -> hPutStrLn stderr err >> exitFailure
Right formula -> solvePB opt solver formula
solvePB :: Options -> SAT.Solver -> PBFile.Formula -> IO ()
solvePB opt solver formula = do
let nv = PBFile.pbNumVars formula
nc = PBFile.pbNumConstraints formula
putCommentLine $ printf "#vars %d" nv
putCommentLine $ printf "#constraints %d" nc
SAT.newVars_ solver nv
enc <- Tseitin.newEncoderWithPBLin solver
Tseitin.setUsePB enc (optLinearizerPB opt)
pbnlc <- PBNLC.newEncoder solver enc
forM_ (PBFile.pbConstraints formula) $ \(lhs, op, rhs) -> do
case op of
PBFile.Ge -> PBNLC.addPBNLAtLeast pbnlc lhs rhs
PBFile.Eq -> PBNLC.addPBNLExactly pbnlc lhs rhs
spHighlyBiased <-
if optInitSP opt then do
let (cnf, _, _) = PB2SAT.convert formula
initPolarityUsingSP solver nv (CNF.numVars cnf) [(1.0, clause) | clause <- CNF.clauses cnf]
else
return IntMap.empty
initialModel <-
if optLocalSearchInitial opt then do
let (wcnf, _, mtrans) = WBO2MaxSAT.convert $ PB2WBO.convert formula
fixed <- filter (\lit -> abs lit <= nv) <$> SAT.getFixedLiterals solver
let var_init1 = IntMap.fromList [(abs lit, lit > 0) | lit <- fixed, abs lit <= nv]
var_init2 = IntMap.map (>0) spHighlyBiased
-- note that IntMap.union is left-biased.
var_init = [if b then v else -v | (v, b) <- IntMap.toList (var_init1 `IntMap.union` var_init2)]
let opt2 =
def
{ UBCSAT.optCommand = optUBCSAT opt
, UBCSAT.optTempDir = optTempDir opt
, UBCSAT.optProblem = wcnf
, UBCSAT.optVarInit = var_init
}
ret <- UBCSAT.ubcsatBest opt2
case ret of
Nothing -> return Nothing
Just (obj,m) -> do
let m2 = mtrans m
forM_ (assocs m2) $ \(v, val) -> do
SAT.setVarPolarity solver v val
if obj < MaxSAT.topCost wcnf then
return $ Just m2
else
return Nothing
else
return Nothing
case PBFile.pbObjectiveFunction formula of
Nothing -> do
result <- SAT.solve solver
putSLine $ if result then "SATISFIABLE" else "UNSATISFIABLE"
when result $ do
m <- SAT.getModel solver
pbPrintModel stdout m nv
writeSOLFile opt m Nothing nv
Just obj' -> do
obj'' <- PBNLC.linearizePBSumWithPolarity pbnlc Tseitin.polarityNeg obj'
nv' <- SAT.getNVars solver
defs <- Tseitin.getDefinitions enc
let extendModel :: SAT.Model -> SAT.Model
extendModel m = array (1,nv') (assocs a)
where
-- Use BOXED array to tie the knot
a :: Array SAT.Var Bool
a = array (1,nv') $ assocs m ++ [(v, Tseitin.evalFormula a phi) | (v,phi) <- defs]
pbo <- PBO.newOptimizer2 solver obj'' (\m -> SAT.evalPBSum m obj')
setupOptimizer pbo opt
PBO.setOnUpdateBestSolution pbo $ \_ val -> putOLine (show val)
PBO.setOnUpdateLowerBound pbo $ \lb -> do
putCommentLine $ printf "lower bound updated to %d" lb
case initialModel of
Nothing -> return ()
Just m -> PBO.addSolution pbo (extendModel m)
finally (PBO.optimize pbo) $ do
ret <- PBO.getBestSolution pbo
case ret of
Nothing -> do
b <- PBO.isUnsat pbo
if b
then putSLine "UNSATISFIABLE"
else putSLine "UNKNOWN"
Just (m, val) -> do
b <- PBO.isOptimum pbo
if b
then putSLine "OPTIMUM FOUND"
else putSLine "SATISFIABLE"
pbPrintModel stdout m nv
writeSOLFile opt m (Just val) nv
setupOptimizer :: PBO.Optimizer -> Options -> IO ()
setupOptimizer pbo opt = do
PBO.setEnableObjFunVarsHeuristics pbo $ optObjFunVarsHeuristics opt
PBO.setMethod pbo $ optOptMethod opt
PBO.setLogger pbo putCommentLine
-- ------------------------------------------------------------------------
mainWBO :: Options -> SAT.Solver -> [String] -> IO ()
mainWBO opt solver args = do
ret <- case args of
["-"] -> liftM PBFileAttoparsec.parseWBOByteString $ BS.hGetContents stdin
[fname] -> PBFileAttoparsec.parseWBOFile fname
_ -> showHelp stderr >> exitFailure
case ret of
Left err -> hPutStrLn stderr err >> exitFailure
Right formula -> solveWBO opt solver False formula
solveWBO :: Options -> SAT.Solver -> Bool -> PBFile.SoftFormula -> IO ()
solveWBO opt solver isMaxSat formula =
solveWBO' opt solver isMaxSat formula (WBO2MaxSAT.convert formula) Nothing
solveWBO' :: Options -> SAT.Solver -> Bool -> PBFile.SoftFormula -> (MaxSAT.WCNF, SAT.Model -> SAT.Model, SAT.Model -> SAT.Model) -> Maybe FilePath -> IO ()
solveWBO' opt solver isMaxSat formula (wcnf, _, mtrans) wcnfFileName = do
let nv = PBFile.wboNumVars formula
nc = PBFile.wboNumConstraints formula
putCommentLine $ printf "#vars %d" nv
putCommentLine $ printf "#constraints %d" nc
SAT.resizeVarCapacity solver (nv + length [() | (Just _, _) <- PBFile.wboConstraints formula])
enc <- Tseitin.newEncoderWithPBLin solver
Tseitin.setUsePB enc (optLinearizerPB opt)
pbnlc <- PBNLC.newEncoder solver enc
(obj, defsPB) <- WBO2PB.addWBO pbnlc formula
objLin <- PBNLC.linearizePBSumWithPolarity pbnlc Tseitin.polarityNeg obj
spHighlyBiased <-
if optInitSP opt then do
initPolarityUsingSP solver nv (MaxSAT.numVars wcnf) [(fromIntegral w, c) | (w, c) <- MaxSAT.clauses wcnf]
else
return IntMap.empty
initialModel <- liftM (fmap (mtrans . snd)) $
if optLocalSearchInitial opt then do
fixed <- SAT.getFixedLiterals solver
let var_init1 = IntMap.fromList [(abs lit, lit > 0) | lit <- fixed, abs lit <= nv]
var_init2 = IntMap.map (>0) spHighlyBiased
-- note that IntMap.union is left-biased.
var_init = [if b then v else -v | (v, b) <- IntMap.toList (var_init1 `IntMap.union` var_init2)]
let opt2 =
def
{ UBCSAT.optCommand = optUBCSAT opt
, UBCSAT.optTempDir = optTempDir opt
, UBCSAT.optProblem = wcnf
, UBCSAT.optProblemFile = wcnfFileName
, UBCSAT.optVarInit = var_init
}
UBCSAT.ubcsatBestFeasible opt2
else
return Nothing
nv' <- SAT.getNVars solver
defsTseitin <- Tseitin.getDefinitions enc
let extendModel :: SAT.Model -> SAT.Model
extendModel m = array (1,nv') (assocs a)
where
-- Use BOXED array to tie the knot
a :: Array SAT.Var Bool
a = array (1,nv') $
assocs m ++
[(v, Tseitin.evalFormula a phi) | (v, phi) <- defsTseitin] ++
[(v, SAT.evalPBConstraint a constr) | (v, constr) <- defsPB]
let softConstrs = [(c, constr) | (Just c, constr) <- PBFile.wboConstraints formula]
pbo <- PBO.newOptimizer2 solver objLin $ \m ->
sum [if SAT.evalPBConstraint m constr then 0 else w | (w,constr) <- softConstrs]
setupOptimizer pbo opt
PBO.setOnUpdateBestSolution pbo $ \_ val -> putOLine (show val)
PBO.setOnUpdateLowerBound pbo $ \lb -> do
putCommentLine $ printf "lower bound updated to %d" lb
case initialModel of
Nothing -> return ()
Just m -> PBO.addSolution pbo (extendModel m)
finally (PBO.optimize pbo) $ do
ret <- PBO.getBestSolution pbo
case ret of
Nothing -> do
b <- PBO.isUnsat pbo
if b
then putSLine "UNSATISFIABLE"
else putSLine "UNKNOWN"
Just (m, val) -> do
b <- PBO.isOptimum pbo
if b then do
putSLine "OPTIMUM FOUND"
if isMaxSat then
satPrintModel stdout m nv
else
pbPrintModel stdout m nv
writeSOLFile opt m (Just val) nv
else if not isMaxSat then do
putSLine "SATISFIABLE"
pbPrintModel stdout m nv
writeSOLFile opt m (Just val) nv
else
putSLine "UNKNOWN"
-- ------------------------------------------------------------------------
mainMaxSAT :: Options -> SAT.Solver -> [String] -> IO ()
mainMaxSAT opt solver args = do
ret <- case args of
["-"] -> liftM MaxSAT.parseByteString BS.getContents
[fname] -> MaxSAT.parseFile fname
_ -> showHelp stderr >> exitFailure
case ret of
Left err -> hPutStrLn stderr err >> exitFailure
Right wcnf -> do
let fname = case args of
[fname] | or [s `isSuffixOf` map toLower fname | s <- [".cnf", ".wcnf"]] -> Just fname
_ -> Nothing
solveMaxSAT opt solver wcnf fname
solveMaxSAT :: Options -> SAT.Solver -> MaxSAT.WCNF -> Maybe FilePath -> IO ()
solveMaxSAT opt solver wcnf wcnfFileName =
solveWBO' opt solver True (MaxSAT2WBO.convert wcnf) (wcnf, id, id) wcnfFileName
-- ------------------------------------------------------------------------
mainMIP :: Options -> SAT.Solver -> [String] -> IO ()
mainMIP opt solver args = do
mip <-
case args of
[fname@"-"] -> do
F.mapM_ (\s -> hSetEncoding stdin =<< mkTextEncoding s) (optFileEncoding opt)
s <- hGetContents stdin
case MIP.parseLPString def fname s of
Right mip -> return mip
Left err ->
case MIP.parseMPSString def fname s of
Right mip -> return mip
Left err2 -> do
hPrint stderr err
hPrint stderr err2
exitFailure
[fname] -> do
enc <- T.mapM mkTextEncoding (optFileEncoding opt)
MIP.readFile def{ MIP.optFileEncoding = enc } fname
_ -> showHelp stderr >> exitFailure
solveMIP opt solver (fmap toRational mip)
solveMIP :: Options -> SAT.Solver -> MIP.Problem Rational -> IO ()
solveMIP opt solver mip = do
enc <- Tseitin.newEncoderWithPBLin solver
Tseitin.setUsePB enc (optLinearizerPB opt)
pbnlc <- PBNLC.newEncoder solver enc
ret <- MIP2PB.addMIP pbnlc mip
case ret of
Left msg -> do
putCommentLine msg
putSLine "UNKNOWN"
exitFailure
Right (obj, otrans, mtrans) -> do
(linObj, linObjOffset) <- Integer.linearize pbnlc obj
let transformObjVal :: Integer -> Rational
transformObjVal val = otrans (val + linObjOffset)
printModel :: Map MIP.Var Integer -> IO ()
printModel m = do
forM_ (Map.toList m) $ \(v, val) -> do
printf "v %s = %d\n" (MIP.fromVar v) val
hFlush stdout
writeSol :: Map MIP.Var Integer -> Rational -> IO ()
writeSol m val = do
case optWriteFile opt of
Nothing -> return ()
Just fname -> do
let sol = MIP.Solution
{ MIP.solStatus = MIP.StatusUnknown
, MIP.solObjectiveValue = Just $ Scientific.fromFloatDigits (fromRational val :: Double)
, MIP.solVariables = Map.fromList [(v, fromIntegral val) | (v,val) <- Map.toList m]
}
GurobiSol.writeFile fname sol
pbo <- PBO.newOptimizer solver linObj
setupOptimizer pbo opt
PBO.setOnUpdateBestSolution pbo $ \_ val -> do
putOLine $ showRational (optPrintRational opt) (transformObjVal val)
finally (PBO.optimize pbo) $ do
ret <- PBO.getBestSolution pbo
case ret of
Nothing -> do
b <- PBO.isUnsat pbo
if b
then putSLine "UNSATISFIABLE"
else putSLine "UNKNOWN"
Just (m,val) -> do
b <- PBO.isOptimum pbo
if b
then putSLine "OPTIMUM FOUND"
else putSLine "SATISFIABLE"
let m2 = mtrans m
val2 = transformObjVal val
printModel m2
writeSol m2 val2
-- ------------------------------------------------------------------------
writeSOLFile :: Options -> SAT.Model -> Maybe Integer -> Int -> IO ()
writeSOLFile opt m obj nbvar = do
case optWriteFile opt of
Nothing -> return ()
Just fname -> do
let sol = MIP.Solution
{ MIP.solStatus = MIP.StatusUnknown
, MIP.solObjectiveValue = fmap fromIntegral obj
, MIP.solVariables = Map.fromList [(MIP.toVar ("x" ++ show x), if b then 1.0 else 0.0) | (x,b) <- assocs m, x <= nbvar]
}
GurobiSol.writeFile fname sol
durationSecs :: TimeSpec -> TimeSpec -> Double
durationSecs start end = fromIntegral (toNanoSecs (end `diffTimeSpec` start)) / 10^(9::Int)