{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO
-- Copyright   :  (c) Masahiro Sakai 2012-2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Pseudo-Boolean Optimization (PBO) Solver
--
-----------------------------------------------------------------------------
module ToySolver.SAT.PBO
  (
  -- * The @Optimizer@ type
    Optimizer
  , newOptimizer
  , newOptimizer2

  -- * Solving
  , optimize
  , addSolution

  -- * Extract results
  , getBestSolution
  , getBestValue
  , getBestModel
  , isUnsat
  , isOptimum
  , isFinished

  -- * Configulation
  , Method (..)
  , showMethod
  , parseMethod
  , getMethod
  , setMethod
  , defaultEnableObjFunVarsHeuristics
  , getEnableObjFunVarsHeuristics
  , setEnableObjFunVarsHeuristics
  , defaultTrialLimitConf
  , getTrialLimitConf
  , setTrialLimitConf
  , setOnUpdateBestSolution
  , setOnUpdateLowerBound
  , setLogger
  ) where

import Control.Concurrent.STM
import Control.Exception
import Control.Monad
import Data.Array.IArray
import Data.Char
import Data.Default.Class
import Data.IORef
import qualified Data.Set as Set
import qualified Data.Map as Map
import Text.Printf
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.PBO.Context as C
import qualified ToySolver.SAT.PBO.BC as BC
import qualified ToySolver.SAT.PBO.BCD as BCD
import qualified ToySolver.SAT.PBO.BCD2 as BCD2
import qualified ToySolver.SAT.PBO.UnsatBased as UnsatBased
import qualified ToySolver.SAT.PBO.MSU4 as MSU4

-- | Optimization method
--
-- The default value can be obtained by 'def'.
data Method
  = LinearSearch
  | BinarySearch
  | AdaptiveSearch
  | UnsatBased
  | MSU4
  | BC
  | BCD
  | BCD2
  deriving (Method -> Method -> Bool
(Method -> Method -> Bool)
-> (Method -> Method -> Bool) -> Eq Method
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Method -> Method -> Bool
$c/= :: Method -> Method -> Bool
== :: Method -> Method -> Bool
$c== :: Method -> Method -> Bool
Eq, Eq Method
Eq Method
-> (Method -> Method -> Ordering)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Method)
-> (Method -> Method -> Method)
-> Ord Method
Method -> Method -> Bool
Method -> Method -> Ordering
Method -> Method -> Method
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Method -> Method -> Method
$cmin :: Method -> Method -> Method
max :: Method -> Method -> Method
$cmax :: Method -> Method -> Method
>= :: Method -> Method -> Bool
$c>= :: Method -> Method -> Bool
> :: Method -> Method -> Bool
$c> :: Method -> Method -> Bool
<= :: Method -> Method -> Bool
$c<= :: Method -> Method -> Bool
< :: Method -> Method -> Bool
$c< :: Method -> Method -> Bool
compare :: Method -> Method -> Ordering
$ccompare :: Method -> Method -> Ordering
$cp1Ord :: Eq Method
Ord, Int -> Method -> ShowS
[Method] -> ShowS
Method -> String
(Int -> Method -> ShowS)
-> (Method -> String) -> ([Method] -> ShowS) -> Show Method
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Method] -> ShowS
$cshowList :: [Method] -> ShowS
show :: Method -> String
$cshow :: Method -> String
showsPrec :: Int -> Method -> ShowS
$cshowsPrec :: Int -> Method -> ShowS
Show, Int -> Method
Method -> Int
Method -> [Method]
Method -> Method
Method -> Method -> [Method]
Method -> Method -> Method -> [Method]
(Method -> Method)
-> (Method -> Method)
-> (Int -> Method)
-> (Method -> Int)
-> (Method -> [Method])
-> (Method -> Method -> [Method])
-> (Method -> Method -> [Method])
-> (Method -> Method -> Method -> [Method])
-> Enum Method
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Method -> Method -> Method -> [Method]
$cenumFromThenTo :: Method -> Method -> Method -> [Method]
enumFromTo :: Method -> Method -> [Method]
$cenumFromTo :: Method -> Method -> [Method]
enumFromThen :: Method -> Method -> [Method]
$cenumFromThen :: Method -> Method -> [Method]
enumFrom :: Method -> [Method]
$cenumFrom :: Method -> [Method]
fromEnum :: Method -> Int
$cfromEnum :: Method -> Int
toEnum :: Int -> Method
$ctoEnum :: Int -> Method
pred :: Method -> Method
$cpred :: Method -> Method
succ :: Method -> Method
$csucc :: Method -> Method
Enum, Method
Method -> Method -> Bounded Method
forall a. a -> a -> Bounded a
maxBound :: Method
$cmaxBound :: Method
minBound :: Method
$cminBound :: Method
Bounded)

instance Default Method where
  def :: Method
def = Method
LinearSearch

showMethod :: Method -> String
showMethod :: Method -> String
showMethod Method
m =
  case Method
m of
    Method
LinearSearch -> String
"linear"
    Method
BinarySearch -> String
"binary"
    Method
AdaptiveSearch -> String
"adaptive"
    Method
UnsatBased -> String
"unsat-based"
    Method
MSU4 -> String
"msu4"
    Method
BC -> String
"bc"
    Method
BCD -> String
"bcd"
    Method
BCD2 -> String
"bcd2"

parseMethod :: String -> Maybe Method
parseMethod :: String -> Maybe Method
parseMethod String
s =
  case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"linear"   -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
LinearSearch
    String
"binary"   -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
BinarySearch
    String
"adaptive" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
AdaptiveSearch
    String
"unsat"    -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
UnsatBased
    String
"msu4"     -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
MSU4
    String
"bc"       -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
BC
    String
"bcd"      -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
BCD
    String
"bcd2"     -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
BCD2
    String
_ -> Maybe Method
forall a. Maybe a
Nothing

data Optimizer
  = Optimizer
  { Optimizer -> SimpleContext
optContext :: C.SimpleContext
  , Optimizer -> Solver
optSolver  :: SAT.Solver
  , Optimizer -> IORef Method
optMethodRef :: IORef Method
  , Optimizer -> IORef Bool
optEnableObjFunVarsHeuristicsRef :: IORef Bool
  , Optimizer -> IORef Int
optTrialLimitConfRef :: IORef Int
  }

newOptimizer :: SAT.Solver -> SAT.PBLinSum -> IO Optimizer
newOptimizer :: Solver -> PBLinSum -> IO Optimizer
newOptimizer Solver
solver PBLinSum
obj = Solver -> PBLinSum -> (Model -> Integer) -> IO Optimizer
newOptimizer2 Solver
solver PBLinSum
obj (\Model
m -> Model -> PBLinSum -> Integer
forall m. IModel m => m -> PBLinSum -> Integer
SAT.evalPBLinSum Model
m PBLinSum
obj)

newOptimizer2 :: SAT.Solver -> SAT.PBLinSum -> (SAT.Model -> Integer) -> IO Optimizer
newOptimizer2 :: Solver -> PBLinSum -> (Model -> Integer) -> IO Optimizer
newOptimizer2 Solver
solver PBLinSum
obj Model -> Integer
obj2 = do
  SimpleContext
cxt <- PBLinSum -> (Model -> Integer) -> IO SimpleContext
C.newSimpleContext2 PBLinSum
obj Model -> Integer
obj2
  IORef Method
strategyRef   <- Method -> IO (IORef Method)
forall a. a -> IO (IORef a)
newIORef Method
forall a. Default a => a
def
  IORef Bool
heuristicsRef <- Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
defaultEnableObjFunVarsHeuristics
  IORef Int
trialLimitRef <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
defaultTrialLimitConf
  Optimizer -> IO Optimizer
forall (m :: * -> *) a. Monad m => a -> m a
return (Optimizer -> IO Optimizer) -> Optimizer -> IO Optimizer
forall a b. (a -> b) -> a -> b
$
    Optimizer :: SimpleContext
-> Solver -> IORef Method -> IORef Bool -> IORef Int -> Optimizer
Optimizer
    { optContext :: SimpleContext
optContext = SimpleContext
cxt
    , optSolver :: Solver
optSolver = Solver
solver
    , optMethodRef :: IORef Method
optMethodRef = IORef Method
strategyRef
    , optEnableObjFunVarsHeuristicsRef :: IORef Bool
optEnableObjFunVarsHeuristicsRef = IORef Bool
heuristicsRef
    , optTrialLimitConfRef :: IORef Int
optTrialLimitConfRef = IORef Int
trialLimitRef
    }

optimize :: Optimizer -> IO ()
optimize :: Optimizer -> IO ()
optimize Optimizer
opt = do
  let cxt :: SimpleContext
cxt = Optimizer -> SimpleContext
optContext Optimizer
opt
  let obj :: PBLinSum
obj = SimpleContext -> PBLinSum
forall a. Context a => a -> PBLinSum
C.getObjectiveFunction SimpleContext
cxt
  let solver :: Solver
solver = Optimizer -> Solver
optSolver Optimizer
opt

  Optimizer -> IO Bool
getEnableObjFunVarsHeuristics Optimizer
opt IO Bool -> (Bool -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
b ->
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Solver -> PBLinSum -> IO ()
tweakParams Solver
solver PBLinSum
obj

  Maybe Model
m <- Optimizer -> IO (Maybe Model)
getBestModel Optimizer
opt
  case Maybe Model
m of
    Maybe Model
Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Model
m -> do
      [(Int, Bool)] -> ((Int, Bool) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m) (((Int, Bool) -> IO ()) -> IO ())
-> ((Int, Bool) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
v, Bool
val) -> do
        Solver -> Int -> Bool -> IO ()
SAT.setVarPolarity Solver
solver Int
v Bool
val

  Method
strategy <- Optimizer -> IO Method
getMethod Optimizer
opt
  case Method
strategy of
    Method
UnsatBased -> SimpleContext -> Solver -> IO ()
forall cxt. Context cxt => cxt -> Solver -> IO ()
UnsatBased.solve SimpleContext
cxt Solver
solver
    Method
MSU4 -> SimpleContext -> Solver -> IO ()
forall cxt. Context cxt => cxt -> Solver -> IO ()
MSU4.solve SimpleContext
cxt Solver
solver
    Method
BC   -> SimpleContext -> Solver -> IO ()
forall cxt. Context cxt => cxt -> Solver -> IO ()
BC.solve SimpleContext
cxt Solver
solver
    Method
BCD  -> SimpleContext -> Solver -> IO ()
forall cxt. Context cxt => cxt -> Solver -> IO ()
BCD.solve SimpleContext
cxt Solver
solver
    Method
BCD2 -> do
      let opt2 :: Options
opt2 = Options
forall a. Default a => a
def
      SimpleContext -> Solver -> Options -> IO ()
forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
BCD2.solve SimpleContext
cxt Solver
solver Options
opt2
    Method
_ -> do
      Solver -> (Config -> Config) -> IO ()
SAT.modifyConfig Solver
solver ((Config -> Config) -> IO ()) -> (Config -> Config) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Config
config -> Config
config{ configEnableBackwardSubsumptionRemoval :: Bool
SAT.configEnableBackwardSubsumptionRemoval = Bool
True }

      IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
        Maybe Integer
ret <- SimpleContext -> STM (Maybe Integer)
forall a. Context a => a -> STM (Maybe Integer)
C.getBestValue SimpleContext
cxt
        case Maybe Integer
ret of
          Just Integer
_ -> IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Maybe Integer
Nothing -> IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ do
            Bool
result <- Solver -> IO Bool
SAT.solve Solver
solver
            if Bool -> Bool
not Bool
result then
              SimpleContext -> IO ()
forall a. Context a => a -> IO ()
C.setFinished SimpleContext
cxt
            else do
              Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
              SimpleContext -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution SimpleContext
cxt Model
m

      IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
        Maybe Integer
ret <- SimpleContext -> STM (Maybe Integer)
forall a. Context a => a -> STM (Maybe Integer)
C.getBestValue SimpleContext
cxt
        case Maybe Integer
ret of
          Maybe Integer
Nothing  -> IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Just Integer
val -> IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ do
            let ub :: Integer
ub = Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
            Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub

      case Method
strategy of
        Method
LinearSearch   -> SimpleContext -> Solver -> IO ()
forall cxt. Context cxt => cxt -> Solver -> IO ()
linSearch SimpleContext
cxt Solver
solver
        Method
BinarySearch   -> SimpleContext -> Solver -> IO ()
forall cxt. Context cxt => cxt -> Solver -> IO ()
binSearch SimpleContext
cxt Solver
solver
        Method
AdaptiveSearch -> do
          Int
lim <- Optimizer -> IO Int
getTrialLimitConf Optimizer
opt
          SimpleContext -> Solver -> Int -> IO ()
forall cxt. Context cxt => cxt -> Solver -> Int -> IO ()
adaptiveSearch SimpleContext
cxt Solver
solver Int
lim
        Method
_              -> String -> IO ()
forall a. HasCallStack => String -> a
error String
"ToySolver.SAT.PBO.minimize: should not happen"

getMethod :: Optimizer -> IO Method
getMethod :: Optimizer -> IO Method
getMethod Optimizer
opt = IORef Method -> IO Method
forall a. IORef a -> IO a
readIORef (Optimizer -> IORef Method
optMethodRef Optimizer
opt)

setMethod :: Optimizer -> Method -> IO ()
setMethod :: Optimizer -> Method -> IO ()
setMethod Optimizer
opt Method
val = IORef Method -> Method -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Optimizer -> IORef Method
optMethodRef Optimizer
opt) Method
val

defaultEnableObjFunVarsHeuristics :: Bool
defaultEnableObjFunVarsHeuristics :: Bool
defaultEnableObjFunVarsHeuristics = Bool
False

getEnableObjFunVarsHeuristics :: Optimizer -> IO Bool
getEnableObjFunVarsHeuristics :: Optimizer -> IO Bool
getEnableObjFunVarsHeuristics Optimizer
opt = IORef Bool -> IO Bool
forall a. IORef a -> IO a
readIORef (Optimizer -> IORef Bool
optEnableObjFunVarsHeuristicsRef Optimizer
opt)

setEnableObjFunVarsHeuristics :: Optimizer -> Bool -> IO ()
setEnableObjFunVarsHeuristics :: Optimizer -> Bool -> IO ()
setEnableObjFunVarsHeuristics Optimizer
opt Bool
val = IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Optimizer -> IORef Bool
optEnableObjFunVarsHeuristicsRef Optimizer
opt) Bool
val

defaultTrialLimitConf :: Int
defaultTrialLimitConf :: Int
defaultTrialLimitConf = Int
1000

getTrialLimitConf :: Optimizer -> IO Int
getTrialLimitConf :: Optimizer -> IO Int
getTrialLimitConf Optimizer
opt = IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef (Optimizer -> IORef Int
optTrialLimitConfRef Optimizer
opt)

setTrialLimitConf :: Optimizer -> Int -> IO ()
setTrialLimitConf :: Optimizer -> Int -> IO ()
setTrialLimitConf Optimizer
opt Int
val = IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Optimizer -> IORef Int
optTrialLimitConfRef Optimizer
opt) Int
val


setOnUpdateBestSolution :: Optimizer -> (SAT.Model -> Integer -> IO ()) -> IO ()
setOnUpdateBestSolution :: Optimizer -> (Model -> Integer -> IO ()) -> IO ()
setOnUpdateBestSolution Optimizer
opt Model -> Integer -> IO ()
cb = SimpleContext -> (Model -> Integer -> IO ()) -> IO ()
C.setOnUpdateBestSolution (Optimizer -> SimpleContext
optContext Optimizer
opt) Model -> Integer -> IO ()
cb

setOnUpdateLowerBound :: Optimizer -> (Integer -> IO ()) -> IO ()
setOnUpdateLowerBound :: Optimizer -> (Integer -> IO ()) -> IO ()
setOnUpdateLowerBound Optimizer
opt Integer -> IO ()
cb = SimpleContext -> (Integer -> IO ()) -> IO ()
C.setOnUpdateLowerBound (Optimizer -> SimpleContext
optContext Optimizer
opt) Integer -> IO ()
cb

setLogger :: Optimizer -> (String -> IO ()) -> IO ()
setLogger :: Optimizer -> (String -> IO ()) -> IO ()
setLogger Optimizer
opt String -> IO ()
cb = SimpleContext -> (String -> IO ()) -> IO ()
C.setLogger (Optimizer -> SimpleContext
optContext Optimizer
opt) String -> IO ()
cb


addSolution :: Optimizer -> SAT.Model -> IO ()
addSolution :: Optimizer -> Model -> IO ()
addSolution Optimizer
opt Model
m = SimpleContext -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution (Optimizer -> SimpleContext
optContext Optimizer
opt) Model
m

getBestSolution :: Optimizer -> IO (Maybe (SAT.Model, Integer))
getBestSolution :: Optimizer -> IO (Maybe (Model, Integer))
getBestSolution Optimizer
opt = STM (Maybe (Model, Integer)) -> IO (Maybe (Model, Integer))
forall a. STM a -> IO a
atomically (STM (Maybe (Model, Integer)) -> IO (Maybe (Model, Integer)))
-> STM (Maybe (Model, Integer)) -> IO (Maybe (Model, Integer))
forall a b. (a -> b) -> a -> b
$ SimpleContext -> STM (Maybe (Model, Integer))
forall a. Context a => a -> STM (Maybe (Model, Integer))
C.getBestSolution (Optimizer -> SimpleContext
optContext Optimizer
opt)

getBestValue :: Optimizer -> IO (Maybe Integer)
getBestValue :: Optimizer -> IO (Maybe Integer)
getBestValue Optimizer
opt = STM (Maybe Integer) -> IO (Maybe Integer)
forall a. STM a -> IO a
atomically (STM (Maybe Integer) -> IO (Maybe Integer))
-> STM (Maybe Integer) -> IO (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ SimpleContext -> STM (Maybe Integer)
forall a. Context a => a -> STM (Maybe Integer)
C.getBestValue (Optimizer -> SimpleContext
optContext Optimizer
opt)

getBestModel :: Optimizer -> IO (Maybe SAT.Model)
getBestModel :: Optimizer -> IO (Maybe Model)
getBestModel Optimizer
opt = STM (Maybe Model) -> IO (Maybe Model)
forall a. STM a -> IO a
atomically (STM (Maybe Model) -> IO (Maybe Model))
-> STM (Maybe Model) -> IO (Maybe Model)
forall a b. (a -> b) -> a -> b
$ SimpleContext -> STM (Maybe Model)
forall a. Context a => a -> STM (Maybe Model)
C.getBestModel (Optimizer -> SimpleContext
optContext Optimizer
opt)

isUnsat :: Optimizer -> IO Bool
isUnsat :: Optimizer -> IO Bool
isUnsat Optimizer
opt = STM Bool -> IO Bool
forall a. STM a -> IO a
atomically (STM Bool -> IO Bool) -> STM Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ SimpleContext -> STM Bool
forall a. Context a => a -> STM Bool
C.isUnsat (Optimizer -> SimpleContext
optContext Optimizer
opt)

isOptimum :: Optimizer -> IO Bool
isOptimum :: Optimizer -> IO Bool
isOptimum Optimizer
opt = STM Bool -> IO Bool
forall a. STM a -> IO a
atomically (STM Bool -> IO Bool) -> STM Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ SimpleContext -> STM Bool
forall a. Context a => a -> STM Bool
C.isOptimum (Optimizer -> SimpleContext
optContext Optimizer
opt)

isFinished :: Optimizer -> IO Bool
isFinished :: Optimizer -> IO Bool
isFinished Optimizer
opt = STM Bool -> IO Bool
forall a. STM a -> IO a
atomically (STM Bool -> IO Bool) -> STM Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ SimpleContext -> STM Bool
forall a. Context a => a -> STM Bool
C.isFinished (Optimizer -> SimpleContext
optContext Optimizer
opt)


linSearch :: C.Context cxt => cxt -> SAT.Solver -> IO ()
linSearch :: cxt -> Solver -> IO ()
linSearch cxt
cxt Solver
solver = IO ()
loop
  where
    obj :: PBLinSum
obj = cxt -> PBLinSum
forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt

    loop :: IO ()
    loop :: IO ()
loop = do
      Bool
result <- Solver -> IO Bool
SAT.solve Solver
solver
      if Bool
result then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        let val :: Integer
val = cxt -> Model -> Integer
forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
        let ub :: Integer
ub = Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
        cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
        Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub
        IO ()
loop
      else do
        cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
        () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

binSearch :: C.Context cxt => cxt -> SAT.Solver -> IO ()
binSearch :: cxt -> Solver -> IO ()
binSearch cxt
cxt Solver
solver = IO ()
loop
  where
    obj :: PBLinSum
obj = cxt -> PBLinSum
forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt

    loop :: IO ()
    loop :: IO ()
loop = IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
      Integer
ub <- cxt -> STM Integer
forall a. Context a => a -> STM Integer
C.getSearchUpperBound cxt
cxt
      Integer
lb <- cxt -> STM Integer
forall a. Context a => a -> STM Integer
C.getLowerBound cxt
cxt
      if Integer
ub Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
lb then do
        IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
      else
        IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ do
          let mid :: Integer
mid = (Integer
lb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
ub) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2
          cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Binary Search: %d <= obj <= %d; guessing obj <= %d" Integer
lb Integer
ub Integer
mid
          Int
sel <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Solver
solver
          Solver -> Int -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Int -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Int
sel PBLinSum
obj Integer
mid
          Bool
ret <- Solver -> [Int] -> IO Bool
SAT.solveWith Solver
solver [Int
sel]
          if Bool
ret then do
            Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
            let v :: Integer
v = cxt -> Model -> Integer
forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
            let ub' :: Integer
ub' = Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
            cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Binary Search: updating upper bound: %d -> %d" Integer
ub Integer
ub'
            cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
            -- old upper bound constraints will be removed by backward subsumption removal
            Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver [Int
sel]
            Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub'
            IO ()
loop
          else do
            -- deleting temporary constraint
            Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver [-Int
sel]
            let lb' :: Integer
lb' = Integer
mid Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
            cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Binary Search: updating lower bound: %d -> %d" Integer
lb Integer
lb'
            cxt -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
lb'
            Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Solver
solver PBLinSum
obj Integer
lb'
            IO ()
loop

-- adaptive search strategy from pbct-0.1.3 <http://www.residual.se/pbct/>
adaptiveSearch :: C.Context cxt => cxt -> SAT.Solver -> Int -> IO ()
adaptiveSearch :: cxt -> Solver -> Int -> IO ()
adaptiveSearch cxt
cxt Solver
solver Int
trialLimitConf = Rational -> IO ()
loop Rational
0
  where
    obj :: PBLinSum
obj = cxt -> PBLinSum
forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt

    loop :: Rational -> IO ()
    loop :: Rational -> IO ()
loop Rational
fraction = IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
      Integer
ub <- cxt -> STM Integer
forall a. Context a => a -> STM Integer
C.getSearchUpperBound cxt
cxt
      Integer
lb <- cxt -> STM Integer
forall a. Context a => a -> STM Integer
C.getLowerBound cxt
cxt
      if Integer
ub Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
lb then
        IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
      else
        IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ do
          let interval :: Integer
interval = Integer
ub Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lb
              mid :: Integer
mid = Integer
ub Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor (Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
interval Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
fraction)
          if Integer
ub Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mid then do
            cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Adaptive Search: %d <= obj <= %d" Integer
lb Integer
ub
            Bool
result <- Solver -> IO Bool
SAT.solve Solver
solver
            if Bool
result then do
              Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
              let v :: Integer
v = cxt -> Model -> Integer
forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
              let ub' :: Integer
ub' = Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
              cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
              Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub'
              let fraction' :: Rational
fraction' = Rational -> Rational -> Rational
forall a. Ord a => a -> a -> a
min Rational
0.5 (Rational
fraction Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
0.1)
              Rational -> IO ()
loop Rational
fraction'
            else
              cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
          else do
            cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Adaptive Search: %d <= obj <= %d; guessing obj <= %d" Integer
lb Integer
ub Integer
mid
            Int
sel <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Solver
solver
            Solver -> Int -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Int -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Int
sel PBLinSum
obj Integer
mid
            Solver -> Maybe Int -> IO ()
SAT.setConfBudget Solver
solver (Maybe Int -> IO ()) -> Maybe Int -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
trialLimitConf
            Either BudgetExceeded Bool
ret' <- IO Bool -> IO (Either BudgetExceeded Bool)
forall e a. Exception e => IO a -> IO (Either e a)
try (IO Bool -> IO (Either BudgetExceeded Bool))
-> IO Bool -> IO (Either BudgetExceeded Bool)
forall a b. (a -> b) -> a -> b
$ Solver -> [Int] -> IO Bool
SAT.solveWith Solver
solver [Int
sel]
            Solver -> Maybe Int -> IO ()
SAT.setConfBudget Solver
solver Maybe Int
forall a. Maybe a
Nothing
            case Either BudgetExceeded Bool
ret' of
              Left BudgetExceeded
SAT.BudgetExceeded -> do
                let fraction' :: Rational
fraction' = Rational -> Rational -> Rational
forall a. Ord a => a -> a -> a
max Rational
0 (Rational
fraction Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
0.05)
                Rational -> IO ()
loop Rational
fraction'
              Right Bool
ret -> do
                let fraction' :: Rational
fraction' = Rational -> Rational -> Rational
forall a. Ord a => a -> a -> a
min Rational
0.5 (Rational
fraction Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
0.1)
                if Bool
ret then do
                  Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
                  let v :: Integer
v = cxt -> Model -> Integer
forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
                  let ub' :: Integer
ub' = Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
                  cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Adaptive Search: updating upper bound: %d -> %d" Integer
ub Integer
ub'
                  cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
                  -- old upper bound constraints will be removed by backward subsumption removal
                  Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver [Int
sel]
                  Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub'
                  Rational -> IO ()
loop Rational
fraction'
                else do
                  -- deleting temporary constraint
                  Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver [-Int
sel]
                  let lb' :: Integer
lb' = Integer
mid Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
                  cxt -> String -> IO ()
forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Adaptive Search: updating lower bound: %d -> %d" Integer
lb Integer
lb'
                  cxt -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
lb'
                  Solver -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Solver
solver PBLinSum
obj Integer
lb'
                  Rational -> IO ()
loop Rational
fraction'

tweakParams :: SAT.Solver -> SAT.PBLinSum -> IO ()
tweakParams :: Solver -> PBLinSum -> IO ()
tweakParams Solver
solver PBLinSum
obj = do
  PBLinSum -> (PBLinTerm -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ PBLinSum
obj ((PBLinTerm -> IO ()) -> IO ()) -> (PBLinTerm -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Integer
c,Int
l) -> do
    let p :: Bool
p = if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Bool -> Bool
not (Int -> Bool
SAT.litPolarity Int
l) else Int -> Bool
SAT.litPolarity Int
l
    Solver -> Int -> Bool -> IO ()
SAT.setVarPolarity Solver
solver (Int -> Int
SAT.litVar Int
l) Bool
p
  let cs :: Set Integer
cs = [Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer -> Integer
forall a. Num a => a -> a
abs Integer
c | (Integer
c,Int
_) <- PBLinSum
obj]
      ws :: Map Integer Int
ws = PBLinSum -> Map Integer Int
forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList (PBLinSum -> Map Integer Int) -> PBLinSum -> Map Integer Int
forall a b. (a -> b) -> a -> b
$ [Integer] -> [Int] -> PBLinSum
forall a b. [a] -> [b] -> [(a, b)]
zip (Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toAscList Set Integer
cs) [Int
1..]
  PBLinSum -> (PBLinTerm -> IO [()]) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ PBLinSum
obj ((PBLinTerm -> IO [()]) -> IO ())
-> (PBLinTerm -> IO [()]) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Integer
c,Int
l) -> do
    let w :: Int
w = Map Integer Int
ws Map Integer Int -> Integer -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! Integer -> Integer
forall a. Num a => a -> a
abs Integer
c
    Int -> IO () -> IO [()]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
w (IO () -> IO [()]) -> IO () -> IO [()]
forall a b. (a -> b) -> a -> b
$ Solver -> Int -> IO ()
SAT.varBumpActivity Solver
solver (Int -> Int
SAT.litVar Int
l)