{-# 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
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
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
Ord, Int -> Method -> ShowS
[Method] -> ShowS
Method -> String
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]
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
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 forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"linear"   -> forall a. a -> Maybe a
Just Method
LinearSearch
    String
"binary"   -> forall a. a -> Maybe a
Just Method
BinarySearch
    String
"adaptive" -> forall a. a -> Maybe a
Just Method
AdaptiveSearch
    String
"unsat"    -> forall a. a -> Maybe a
Just Method
UnsatBased
    String
"msu4"     -> forall a. a -> Maybe a
Just Method
MSU4
    String
"bc"       -> forall a. a -> Maybe a
Just Method
BC
    String
"bcd"      -> forall a. a -> Maybe a
Just Method
BCD
    String
"bcd2"     -> forall a. a -> Maybe a
Just Method
BCD2
    String
_ -> 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 -> 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   <- forall a. a -> IO (IORef a)
newIORef forall a. Default a => a
def
  IORef Bool
heuristicsRef <- forall a. a -> IO (IORef a)
newIORef Bool
defaultEnableObjFunVarsHeuristics
  IORef Int
trialLimitRef <- forall a. a -> IO (IORef a)
newIORef Int
defaultTrialLimitConf
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    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 = 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Bool
b ->
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Model
m -> do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m) 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 -> forall cxt. Context cxt => cxt -> Solver -> IO ()
UnsatBased.solve SimpleContext
cxt Solver
solver
    Method
MSU4 -> forall cxt. Context cxt => cxt -> Solver -> IO ()
MSU4.solve SimpleContext
cxt Solver
solver
    Method
BC   -> forall cxt. Context cxt => cxt -> Solver -> IO ()
BC.solve SimpleContext
cxt Solver
solver
    Method
BCD  -> forall cxt. Context cxt => cxt -> Solver -> IO ()
BCD.solve SimpleContext
cxt Solver
solver
    Method
BCD2 -> do
      let opt2 :: Options
opt2 = forall a. Default a => a
def
      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 forall a b. (a -> b) -> a -> b
$ \Config
config -> Config
config{ configEnableBackwardSubsumptionRemoval :: Bool
SAT.configEnableBackwardSubsumptionRemoval = Bool
True }

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

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

      case Method
strategy of
        Method
LinearSearch   -> forall cxt. Context cxt => cxt -> Solver -> IO ()
linSearch SimpleContext
cxt Solver
solver
        Method
BinarySearch   -> forall cxt. Context cxt => cxt -> Solver -> IO ()
binSearch SimpleContext
cxt Solver
solver
        Method
AdaptiveSearch -> do
          Int
lim <- Optimizer -> IO Int
getTrialLimitConf Optimizer
opt
          forall cxt. Context cxt => cxt -> Solver -> Int -> IO ()
adaptiveSearch SimpleContext
cxt Solver
solver Int
lim
        Method
_              -> 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ 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 = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ 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 = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ 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 = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ 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 = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ 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 = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM Bool
C.isFinished (Optimizer -> SimpleContext
optContext Optimizer
opt)


linSearch :: C.Context cxt => cxt -> SAT.Solver -> IO ()
linSearch :: forall cxt. Context cxt => cxt -> Solver -> IO ()
linSearch cxt
cxt Solver
solver = IO ()
loop
  where
    obj :: PBLinSum
obj = 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 = forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
        let ub :: Integer
ub = Integer
val forall a. Num a => a -> a -> a
- Integer
1
        forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
        forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub
        IO ()
loop
      else do
        forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
        forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

    loop :: Rational -> IO ()
    loop :: Rational -> IO ()
loop Rational
fraction = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
      Integer
ub <- forall a. Context a => a -> STM Integer
C.getSearchUpperBound cxt
cxt
      Integer
lb <- forall a. Context a => a -> STM Integer
C.getLowerBound cxt
cxt
      if Integer
ub forall a. Ord a => a -> a -> Bool
< Integer
lb then
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
      else
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
          let interval :: Integer
interval = Integer
ub forall a. Num a => a -> a -> a
- Integer
lb
              mid :: Integer
mid = Integer
ub forall a. Num a => a -> a -> a
- forall a b. (RealFrac a, Integral b) => a -> b
floor (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
interval forall a. Num a => a -> a -> a
* Rational
fraction)
          if Integer
ub forall a. Eq a => a -> a -> Bool
== Integer
mid then do
            forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt forall a b. (a -> b) -> a -> b
$ 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 = forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
              let ub' :: Integer
ub' = Integer
v forall a. Num a => a -> a -> a
- Integer
1
              forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
              forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub'
              let fraction' :: Rational
fraction' = forall a. Ord a => a -> a -> a
min Rational
0.5 (Rational
fraction forall a. Num a => a -> a -> a
+ Rational
0.1)
              Rational -> IO ()
loop Rational
fraction'
            else
              forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
          else do
            forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Adaptive Search: %d <= obj <= %d; guessing obj <= %d" Integer
lb Integer
ub Integer
mid
            Int
sel <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Solver
solver
            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 forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Int
trialLimitConf
            Either BudgetExceeded Bool
ret' <- forall e a. Exception e => IO a -> IO (Either e a)
try 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 forall a. Maybe a
Nothing
            case Either BudgetExceeded Bool
ret' of
              Left BudgetExceeded
SAT.BudgetExceeded -> do
                let fraction' :: Rational
fraction' = forall a. Ord a => a -> a -> a
max Rational
0 (Rational
fraction forall a. Num a => a -> a -> a
- Rational
0.05)
                Rational -> IO ()
loop Rational
fraction'
              Right Bool
ret -> do
                let fraction' :: Rational
fraction' = forall a. Ord a => a -> a -> a
min Rational
0.5 (Rational
fraction 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 = forall a. Context a => a -> Model -> Integer
C.evalObjectiveFunction cxt
cxt Model
m
                  let ub' :: Integer
ub' = Integer
v forall a. Num a => a -> a -> a
- Integer
1
                  forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Adaptive Search: updating upper bound: %d -> %d" Integer
ub Integer
ub'
                  forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
                  -- old upper bound constraints will be removed by backward subsumption removal
                  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver [Int
sel]
                  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
                  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver [-Int
sel]
                  let lb' :: Integer
lb' = Integer
mid forall a. Num a => a -> a -> a
+ Integer
1
                  forall a. Context a => a -> String -> IO ()
C.logMessage cxt
cxt forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Adaptive Search: updating lower bound: %d -> %d" Integer
lb Integer
lb'
                  forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
lb'
                  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
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ PBLinSum
obj forall a b. (a -> b) -> a -> b
$ \(Integer
c,Int
l) -> do
    let p :: Bool
p = if Integer
c 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 = forall a. Ord a => [a] -> Set a
Set.fromList [forall a. Num a => a -> a
abs Integer
c | (Integer
c,Int
_) <- PBLinSum
obj]
      ws :: Map Integer Int
ws = forall k a. Eq k => [(k, a)] -> Map k a
Map.fromAscList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Set a -> [a]
Set.toAscList Set Integer
cs) [Int
1..]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ PBLinSum
obj forall a b. (a -> b) -> a -> b
$ \(Integer
c,Int
l) -> do
    let w :: Int
w = Map Integer Int
ws forall k a. Ord k => Map k a -> k -> a
Map.! forall a. Num a => a -> a
abs Integer
c
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
w forall a b. (a -> b) -> a -> b
$ Solver -> Int -> IO ()
SAT.varBumpActivity Solver
solver (Int -> Int
SAT.litVar Int
l)