probsat.hs

module Main where

import Control.Monad
import Data.Char
import Data.Default.Class
import Data.Monoid
import qualified Data.Vector.Unboxed as VU
import Options.Applicative
import System.Clock
import System.IO
import qualified System.Random.MWC as Rand
import Text.Printf

import qualified ToySolver.FileFormat as FF
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Solver.SLS.ProbSAT as ProbSAT
import ToySolver.SAT.Printer (maxsatPrintModel)

data Options = Options
  { optAlgorithm :: String
  , optFileName :: FilePath
  , optOptions :: ProbSAT.Options
  , optRandomSeed :: Maybe Rand.Seed
  , optProbSATFunc :: String
  , optProbSATCB :: Double
  , optProbSATCM :: Double
  , optWalkSATP :: Double
  } deriving (Eq, Show)

optionsParser :: Parser Options
optionsParser = Options
  <$> algOption
  <*> fileInput
  <*> solverOptions
  <*> randomSeedOption
  <*> func
  <*> cb
  <*> cm
  <*> p
  where
    fileInput :: Parser FilePath
    fileInput = argument str (metavar "FILE")

    algOption :: Parser String
    algOption = strOption
      $  long "alg"
      <> metavar "ALGORITHM"
      <> help "Algorithm: walksat, probsat"
      <> value "probsat"
      <> showDefaultWith id

    solverOptions :: Parser ProbSAT.Options
    solverOptions = ProbSAT.Options
      <$> targetOption
      <*> maxTriesOption
      <*> maxFlipsOption
      <*> pickClauseWeightedOption

    randomSeedOption :: Parser (Maybe Rand.Seed)
    randomSeedOption = optional $
      (fmap (Rand.toSeed . VU.fromList . map read . words)) $
      strOption $
        mconcat
        [ long "random-seed"
        , metavar "\"INT ..\""
        , help "random seed"
        ]

    targetOption :: Parser Integer
    targetOption = option auto
      $  long "target"
      <> help "target objective value"
      <> showDefault
      <> metavar "INT"
      <> value (ProbSAT.optTarget def)

    maxTriesOption :: Parser Int
    maxTriesOption = option auto
      $  long "max-tries"
      <> help "maximum number of tries"
      <> showDefault
      <> metavar "INT"
      <> value (ProbSAT.optMaxTries def)

    maxFlipsOption :: Parser Int
    maxFlipsOption = option auto
      $  long "max-flips"
      <> help "maximum number of flips per try"
      <> showDefault
      <> metavar "INT"
      <> value (ProbSAT.optMaxFlips def)

    pickClauseWeightedOption :: Parser Bool
    pickClauseWeightedOption = switch
      $  short 'w'
      <> long "weighted"
      <> help "enable weighted clause selection"
      <> showDefault

    func :: Parser String
    func = strOption
      $  long "probsat-func"
      <> help "function type: exp, poly"
      <> showDefaultWith id
      <> metavar "FUNC"
      <> value "exp"

    cb :: Parser Double
    cb = option auto
      $  long "probsat-cb"
      <> help "c_b parameter"
      <> showDefault
      <> metavar "REAL"
      <> value 3.6

    cm :: Parser Double
    cm = option auto
      $  long "probsat-cm"
      <> help "c_m parameter"
      <> showDefault
      <> metavar "REAL"
      <> value 0.5

    p :: Parser Double
    p = option auto
      $  long "walksat-p"
      <> help "p parameter"
      <> showDefault
      <> metavar "REAL"
      <> value 0.1

parserInfo :: ParserInfo Options
parserInfo = info (helper <*> optionsParser)
  $  fullDesc
  <> header "probsat - an example program of ToySolver.SAT.SLS.ProbSAT"

main :: IO ()
main = do
  opt <- execParser parserInfo
  wcnf <- FF.readFile (optFileName opt)
  solver <- ProbSAT.newSolverWeighted wcnf
  gen <-
    case optRandomSeed opt of
      Nothing -> Rand.createSystemRandom
      Just seed -> Rand.restore seed
  seed <- Rand.save gen
  putStrLn $ "c use --random-seed=" ++ show (unwords . map show . VU.toList . Rand.fromSeed $ seed) ++ " option to reproduce the execution"
  ProbSAT.setRandomGen solver gen
  let callbacks =
        def
        { ProbSAT.cbOnUpdateBestSolution = \_solver obj _sol -> printf "o %d\n" obj
        }
  case map toLower (optAlgorithm opt) of
    "walksat" -> do
      let p = optWalkSATP opt
      ProbSAT.walksat solver (optOptions opt) callbacks p
    "probsat" -> do
      let cb = optProbSATCB opt
          cm = optProbSATCM opt
      seq cb $ seq cm $ return ()
      case map toLower (optProbSATFunc opt) of
        "exp" -> do
          let f make break = cm**make / cb**break
          ProbSAT.probsat solver (optOptions opt) callbacks f
        "poly" -> do
          let eps = 1
              f make break = make**cm / (eps + break**cb)
          ProbSAT.probsat solver (optOptions opt) callbacks f
        _ -> error ("unknown function type: " ++ optProbSATFunc opt)
    _ -> error ("unknown algorithm name: " ++ optAlgorithm opt)
  (obj,sol) <- ProbSAT.getBestSolution solver
  stat <- ProbSAT.getStatistics solver
  printf "c TotalCPUTime = %fs\n" (fromIntegral (toNanoSecs (ProbSAT.statTotalCPUTime stat)) / 10^(9::Int) :: Double)
  printf "c FlipsPerSecond = %f\n" (ProbSAT.statFlipsPerSecond stat)
  when (obj == 0) $ do
    putStrLn "s OPTIMUM FOUND"
  maxsatPrintModel stdout sol (CNF.wcnfNumVars wcnf)