{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.SAT.PBO.BCD2
( Options (..)
, solve
) where
import Control.Concurrent.STM
import Control.Monad
import Data.IORef
import Data.Default.Class
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Vector as V
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO.Context as C
import qualified ToySolver.Combinatorial.SubsetSum as SubsetSum
import Text.Printf
data Options
= Options
{ Options -> Bool
optEnableHardening :: Bool
, Options -> Bool
optEnableBiasedSearch :: Bool
, Options -> Bool
optSolvingNormalFirst :: Bool
}
instance Default Options where
def :: Options
def =
Options
{ optEnableHardening :: Bool
optEnableHardening = Bool
True
, optEnableBiasedSearch :: Bool
optEnableBiasedSearch = Bool
True
, optSolvingNormalFirst :: Bool
optSolvingNormalFirst = Bool
True
}
data CoreInfo
= CoreInfo
{ CoreInfo -> LitSet
coreLits :: SAT.LitSet
, CoreInfo -> IORef Integer
coreLBRef :: !(IORef Integer)
, CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors :: !(IORef (Map Integer SAT.Lit))
}
newCoreInfo :: SAT.LitSet -> Integer -> IO CoreInfo
newCoreInfo :: LitSet -> Integer -> IO CoreInfo
newCoreInfo LitSet
lits Integer
lb = do
IORef Integer
lbRef <- forall a. a -> IO (IORef a)
newIORef Integer
lb
IORef (Map Integer Lit)
selsRef <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty
forall (m :: * -> *) a. Monad m => a -> m a
return
CoreInfo
{ coreLits :: LitSet
coreLits = LitSet
lits
, coreLBRef :: IORef Integer
coreLBRef = IORef Integer
lbRef
, coreUBSelectors :: IORef (Map Integer Lit)
coreUBSelectors = IORef (Map Integer Lit)
selsRef
}
deleteCoreInfo :: SAT.Solver -> CoreInfo -> IO ()
deleteCoreInfo :: Solver -> CoreInfo -> IO ()
deleteCoreInfo Solver
solver CoreInfo
core = do
Map Integer Lit
m <- forall a. IORef a -> IO a
readIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [a]
Map.elems Map Integer Lit
m) forall a b. (a -> b) -> a -> b
$ \Lit
sel ->
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [-Lit
sel]
getCoreLB :: CoreInfo -> IO Integer
getCoreLB :: CoreInfo -> IO Integer
getCoreLB = forall a. IORef a -> IO a
readIORef forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreInfo -> IORef Integer
coreLBRef
solve :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
solve :: forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
solve cxt
cxt Solver
solver Options
opt = forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
solveWBO (forall a. Context a => a -> Normalized a
C.normalize cxt
cxt) Solver
solver Options
opt
solveWBO :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
solveWBO :: forall cxt. Context cxt => cxt -> Solver -> Options -> IO ()
solveWBO cxt
cxt Solver
solver Options
opt = 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
"BCD2: Hardening is %s." (if Options -> Bool
optEnableHardening Options
opt then String
"enabled" else String
"disabled")
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
"BCD2: BiasedSearch is %s." (if Options -> Bool
optEnableBiasedSearch Options
opt then String
"enabled" else String
"disabled")
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 }
IORef LitSet
unrelaxedRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ Clause -> LitSet
IntSet.fromList [Lit
lit | (Lit
lit,Integer
_) <- [(Lit, Integer)]
sels]
IORef LitSet
relaxedRef <- forall a. a -> IO (IORef a)
newIORef LitSet
IntSet.empty
IORef LitSet
hardenedRef <- forall a. a -> IO (IORef a)
newIORef LitSet
IntSet.empty
IORef Integer
nsatRef <- forall a. a -> IO (IORef a)
newIORef Integer
1
IORef Integer
nunsatRef <- forall a. a -> IO (IORef a)
newIORef Integer
1
IORef Integer
lastUBRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ PBLinSum -> Integer
SAT.pbLinUpperBound PBLinSum
obj
IORef [CoreInfo]
coresRef <- forall a. a -> IO (IORef a)
newIORef []
let getLB :: IO Integer
getLB = do
[CoreInfo]
xs <- forall a. IORef a -> IO a
readIORef IORef [CoreInfo]
coresRef
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Integer
s CoreInfo
core -> do{ Integer
v <- CoreInfo -> IO Integer
getCoreLB CoreInfo
core; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Integer
s forall a. Num a => a -> a -> a
+ Integer
v }) Integer
0 [CoreInfo]
xs
IORef (LitMap Integer)
deductedWeightRef <- forall a. a -> IO (IORef a)
newIORef LitMap Integer
weights
let deductWeight :: Integer -> CoreInfo -> IO ()
deductWeight Integer
d CoreInfo
core =
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (LitMap Integer)
deductedWeightRef forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall a. Num a => a -> a -> a
(+) forall a b. (a -> b) -> a -> b
$
forall a. (Lit -> a) -> LitSet -> IntMap a
IntMap.fromSet (forall a b. a -> b -> a
const (- Integer
d)) (CoreInfo -> LitSet
coreLits CoreInfo
core)
updateLB :: Integer -> CoreInfo -> IO ()
updateLB Integer
oldLB CoreInfo
core = do
Integer
newLB <- IO Integer
getLB
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
newLB
Integer -> CoreInfo -> IO ()
deductWeight (Integer
newLB forall a. Num a => a -> a -> a
- Integer
oldLB) CoreInfo
core
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Solver
solver (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CoreInfo -> IO Integer
getCoreLB CoreInfo
core
let loop :: IO ()
loop = do
Integer
lb <- IO Integer
getLB
Integer
ub <- do
Integer
ub1 <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM Integer
C.getSearchUpperBound cxt
cxt
let ub2 :: Integer
ub2 = [Integer] -> Integer -> Integer
refineUB (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst PBLinSum
obj) Integer
ub1
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub1 forall a. Eq a => a -> a -> Bool
/= Integer
ub2) forall a b. (a -> b) -> a -> b
$ 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
"BCD2: refineUB: %d -> %d" Integer
ub1 Integer
ub2
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
ub2
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub forall a. Ord a => a -> a -> Bool
< Integer
lb) forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
Bool
fin <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM Bool
C.isFinished cxt
cxt
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
fin forall a b. (a -> b) -> a -> b
$ do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Options -> Bool
optEnableHardening Options
opt) forall a b. (a -> b) -> a -> b
$ do
LitMap Integer
deductedWeight <- forall a. IORef a -> IO a
readIORef IORef (LitMap Integer)
deductedWeightRef
LitSet
hardened <- forall a. IORef a -> IO a
readIORef IORef LitSet
hardenedRef
let lits :: LitSet
lits = forall a. IntMap a -> LitSet
IntMap.keysSet (forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (\Integer
w -> Integer
lb forall a. Num a => a -> a -> a
+ Integer
w forall a. Ord a => a -> a -> Bool
> Integer
ub) LitMap Integer
deductedWeight) LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
hardened
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LitSet -> Bool
IntSet.null LitSet
lits) forall a b. (a -> b) -> a -> b
$ 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
"BCD2: hardening fixes %d literals" (LitSet -> Lit
IntSet.size LitSet
lits)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (LitSet -> Clause
IntSet.toList LitSet
lits) forall a b. (a -> b) -> a -> b
$ \Lit
lit -> forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [Lit
lit]
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
unrelaxedRef (LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
lits)
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
relaxedRef (LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
lits)
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
hardenedRef (LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
lits)
Integer
ub0 <- forall a. IORef a -> IO a
readIORef IORef Integer
lastUBRef
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
ub forall a. Ord a => a -> a -> Bool
< Integer
ub0) forall a b. (a -> b) -> a -> b
$ 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
"BCD2: updating upper bound: %d -> %d" Integer
ub0 Integer
ub
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtMost Solver
solver PBLinSum
obj Integer
ub
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
lastUBRef Integer
ub
[CoreInfo]
cores <- forall a. IORef a -> IO a
readIORef IORef [CoreInfo]
coresRef
LitSet
unrelaxed <- forall a. IORef a -> IO a
readIORef IORef LitSet
unrelaxedRef
LitSet
relaxed <- forall a. IORef a -> IO a
readIORef IORef LitSet
relaxedRef
LitSet
hardened <- forall a. IORef a -> IO a
readIORef IORef LitSet
hardenedRef
Integer
nsat <- forall a. IORef a -> IO a
readIORef IORef Integer
nsatRef
Integer
nunsat <- forall a. IORef a -> IO a
readIORef IORef Integer
nunsatRef
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
"BCD2: %d <= obj <= %d" Integer
lb Integer
ub
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
"BCD2: #cores=%d, #unrelaxed=%d, #relaxed=%d, #hardened=%d"
(forall (t :: * -> *) a. Foldable t => t a -> Lit
length [CoreInfo]
cores) (LitSet -> Lit
IntSet.size LitSet
unrelaxed) (LitSet -> Lit
IntSet.size LitSet
relaxed) (LitSet -> Lit
IntSet.size LitSet
hardened)
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
"BCD2: #sat=%d #unsat=%d bias=%d/%d" Integer
nsat Integer
nunsat Integer
nunsat (Integer
nunsat forall a. Num a => a -> a -> a
+ Integer
nsat)
Maybe Model
lastModel <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM (Maybe Model)
C.getBestModel cxt
cxt
IntMap (CoreInfo, Integer)
sels <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [(Lit, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [CoreInfo]
cores forall a b. (a -> b) -> a -> b
$ \CoreInfo
core -> do
Integer
coreLB <- CoreInfo -> IO Integer
getCoreLB CoreInfo
core
let coreUB :: Integer
coreUB = PBLinSum -> Integer
SAT.pbLinUpperBound (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core)
if Integer
coreUB forall a. Ord a => a -> a -> Bool
< Integer
coreLB 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
"BCD2: coreLB (%d) exceeds coreUB (%d)" Integer
coreLB Integer
coreUB
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver []
Lit
sel <- CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
coreUB
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, (CoreInfo
core, Integer
coreUB))
else do
let estimated :: Integer
estimated =
case Maybe Model
lastModel of
Maybe Model
Nothing -> Integer
coreUB
Just Model
m ->
Integer
coreLB forall a. Ord a => a -> a -> a
`max` forall m. IModel m => m -> PBLinSum -> Integer
SAT.evalPBLinSum Model
m (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core)
mid :: Integer
mid =
if Options -> Bool
optEnableBiasedSearch Options
opt
then Integer
coreLB forall a. Num a => a -> a -> a
+ (Integer
estimated forall a. Num a => a -> a -> a
- Integer
coreLB) forall a. Num a => a -> a -> a
* Integer
nunsat forall a. Integral a => a -> a -> a
`div` (Integer
nunsat forall a. Num a => a -> a -> a
+ Integer
nsat)
else (Integer
coreLB forall a. Num a => a -> a -> a
+ Integer
estimated) forall a. Integral a => a -> a -> a
`div` Integer
2
Lit
sel <- CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
mid
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, (CoreInfo
core,Integer
mid))
Bool
ret <- Solver -> Clause -> IO Bool
SAT.solveWith Solver
solver (forall a. IntMap a -> Clause
IntMap.keys IntMap (CoreInfo, Integer)
sels forall a. [a] -> [a] -> [a]
++ LitSet -> Clause
IntSet.toList LitSet
unrelaxed)
if Bool
ret then do
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Integer
nsatRef (forall a. Num a => a -> a -> a
+Integer
1)
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
SAT.getModel Solver
solver
IO ()
loop
else do
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Integer
nunsatRef (forall a. Num a => a -> a -> a
+Integer
1)
LitSet
failed <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver
case LitSet -> Clause
IntSet.toList LitSet
failed of
[] -> forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
[Lit
sel] | Just (CoreInfo
core,Integer
mid) <- forall a. Lit -> IntMap a -> Maybe a
IntMap.lookup Lit
sel IntMap (CoreInfo, Integer)
sels -> 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
"BCD2: updating lower bound of a core"
let newCoreLB :: Integer
newCoreLB = Integer
mid forall a. Num a => a -> a -> a
+ Integer
1
newCoreLB' :: Integer
newCoreLB' = [Integer] -> Integer -> Integer
refineLB (forall a. IntMap a -> [a]
IntMap.elems (forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys LitMap Integer
weights (CoreInfo -> LitSet
coreLits CoreInfo
core))) Integer
newCoreLB
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
newCoreLB forall a. Eq a => a -> a -> Bool
/= Integer
newCoreLB') forall a b. (a -> b) -> a -> b
$ 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
"BCD2: refineLB: %d -> %d" Integer
newCoreLB Integer
newCoreLB'
forall a. IORef a -> a -> IO ()
writeIORef (CoreInfo -> IORef Integer
coreLBRef CoreInfo
core) Integer
newCoreLB'
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [-Lit
sel]
Integer -> CoreInfo -> IO ()
updateLB Integer
lb CoreInfo
core
IO ()
loop
Clause
_ -> do
let torelax :: LitSet
torelax = LitSet
unrelaxed LitSet -> LitSet -> LitSet
`IntSet.intersection` LitSet
failed
intersected :: [(CoreInfo, Integer)]
intersected = forall a. IntMap a -> [a]
IntMap.elems (forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys IntMap (CoreInfo, Integer)
sels LitSet
failed)
disjoint :: [CoreInfo]
disjoint = [CoreInfo
core | (Lit
sel,(CoreInfo
core,Integer
_)) <- forall a. IntMap a -> [(Lit, a)]
IntMap.toList (forall a. IntMap a -> LitSet -> IntMap a
IntMap.withoutKeys IntMap (CoreInfo, Integer)
sels LitSet
failed)]
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
unrelaxedRef (LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
torelax)
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef LitSet
relaxedRef (LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
torelax)
Integer
delta <- do
[Integer]
xs1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(CoreInfo, Integer)]
intersected forall a b. (a -> b) -> a -> b
$ \(CoreInfo
core,Integer
mid) -> do
Integer
coreLB <- CoreInfo -> IO Integer
getCoreLB CoreInfo
core
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer
mid forall a. Num a => a -> a -> a
- Integer
coreLB forall a. Num a => a -> a -> a
+ Integer
1
let xs2 :: [Integer]
xs2 = [LitMap Integer
weights forall a. IntMap a -> Lit -> a
IntMap.! Lit
lit | Lit
lit <- LitSet -> Clause
IntSet.toList LitSet
torelax]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Integer]
xs1 forall a. [a] -> [a] -> [a]
++ [Integer]
xs2)
let mergedCoreLits :: LitSet
mergedCoreLits = forall (f :: * -> *). Foldable f => f LitSet -> LitSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ LitSet
torelax forall a. a -> [a] -> [a]
: [CoreInfo -> LitSet
coreLits CoreInfo
core | (CoreInfo
core,Integer
_) <- [(CoreInfo, Integer)]
intersected]
Integer
mergedCoreLB <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Integer
delta forall a. Num a => a -> a -> a
+) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CoreInfo -> IO Integer
getCoreLB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(CoreInfo, Integer)]
intersected
let mergedCoreLB' :: Integer
mergedCoreLB' = [Integer] -> Integer -> Integer
refineLB (forall a. IntMap a -> [a]
IntMap.elems (forall a. IntMap a -> LitSet -> IntMap a
IntMap.restrictKeys LitMap Integer
weights LitSet
mergedCoreLits)) Integer
mergedCoreLB
CoreInfo
mergedCore <- LitSet -> Integer -> IO CoreInfo
newCoreInfo LitSet
mergedCoreLits Integer
mergedCoreLB'
forall a. IORef a -> a -> IO ()
writeIORef IORef [CoreInfo]
coresRef (CoreInfo
mergedCore forall a. a -> [a] -> [a]
: [CoreInfo]
disjoint)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(CoreInfo, Integer)]
intersected forall a b. (a -> b) -> a -> b
$ \(CoreInfo
core, Integer
_) -> Solver -> CoreInfo -> IO ()
deleteCoreInfo Solver
solver CoreInfo
core
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CoreInfo, Integer)]
intersected then
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
"BCD2: found a new core of size %d: cost of the new core is >=%d"
(LitSet -> Lit
IntSet.size LitSet
torelax) Integer
mergedCoreLB'
else
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
"BCD2: relaxing %d and merging with %d cores into a new core of size %d: cost of the new core is >=%d"
(LitSet -> Lit
IntSet.size LitSet
torelax) (forall (t :: * -> *) a. Foldable t => t a -> Lit
length [(CoreInfo, Integer)]
intersected) (LitSet -> Lit
IntSet.size LitSet
mergedCoreLits) Integer
mergedCoreLB'
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
mergedCoreLB forall a. Eq a => a -> a -> Bool
/= Integer
mergedCoreLB') forall a b. (a -> b) -> a -> b
$
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
"BCD2: refineLB: %d -> %d" Integer
mergedCoreLB Integer
mergedCoreLB'
Integer -> CoreInfo -> IO ()
updateLB Integer
lb CoreInfo
mergedCore
IO ()
loop
Maybe Model
best <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM (Maybe Model)
C.getBestModel cxt
cxt
case Maybe Model
best of
Maybe Model
Nothing | Options -> Bool
optSolvingNormalFirst Options
opt -> do
Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
if Bool
ret then
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
SAT.getModel Solver
solver
else
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
Maybe Model
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
IO ()
loop
where
obj :: SAT.PBLinSum
obj :: PBLinSum
obj = forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt
sels :: [(SAT.Lit, Integer)]
sels :: [(Lit, Integer)]
sels = [(-Lit
lit, Integer
w) | (Integer
w,Lit
lit) <- PBLinSum
obj]
weights :: SAT.LitMap Integer
weights :: LitMap Integer
weights = forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit, Integer)]
sels
coreCostFun :: CoreInfo -> SAT.PBLinSum
coreCostFun :: CoreInfo -> PBLinSum
coreCostFun CoreInfo
c = [(LitMap Integer
weights forall a. IntMap a -> Lit -> a
IntMap.! Lit
lit, -Lit
lit) | Lit
lit <- LitSet -> Clause
IntSet.toList (CoreInfo -> LitSet
coreLits CoreInfo
c)]
getCoreUBAssumption :: CoreInfo -> Integer -> IO SAT.Lit
getCoreUBAssumption :: CoreInfo -> Integer -> IO Lit
getCoreUBAssumption CoreInfo
core Integer
ub = do
Map Integer Lit
m <- forall a. IORef a -> IO a
readIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core)
case forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup Integer
ub Map Integer Lit
m of
(Map Integer Lit
_, Just Lit
sel, Map Integer Lit
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Lit
sel
(Map Integer Lit
lo, Maybe Lit
Nothing, Map Integer Lit
hi) -> do
Lit
sel <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Lit
sel (CoreInfo -> PBLinSum
coreCostFun CoreInfo
core) Integer
ub
forall a. IORef a -> a -> IO ()
writeIORef (CoreInfo -> IORef (Map Integer Lit)
coreUBSelectors CoreInfo
core) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
ub Lit
sel Map Integer Lit
m)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall k a. Map k a -> Bool
Map.null Map Integer Lit
lo) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [- forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax Map Integer Lit
lo), Lit
sel]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall k a. Map k a -> Bool
Map.null Map Integer Lit
hi) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause Solver
solver [- Lit
sel, forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMin Map Integer Lit
hi)]
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
sel
refineLB
:: [Integer]
-> Integer
-> Integer
refineLB :: [Integer] -> Integer -> Integer
refineLB [Integer]
ws Integer
n =
case forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.minSubsetSum (forall a. [a] -> Vector a
V.fromList [Integer]
ws) Integer
n of
Maybe (Integer, Vector Bool)
Nothing -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
w | Integer
w <- [Integer]
ws, Integer
w forall a. Ord a => a -> a -> Bool
> Integer
0] forall a. Num a => a -> a -> a
+ Integer
1
Just (Integer
obj, Vector Bool
_) -> Integer
obj
refineUB
:: [Integer]
-> Integer
-> Integer
refineUB :: [Integer] -> Integer -> Integer
refineUB [Integer]
ws Integer
n
| Integer
n forall a. Ord a => a -> a -> Bool
< Integer
0 = Integer
n
| Bool
otherwise =
case forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.maxSubsetSum (forall a. [a] -> Vector a
V.fromList [Integer]
ws) Integer
n of
Maybe (Integer, Vector Bool)
Nothing -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
w | Integer
w <- [Integer]
ws, Integer
w forall a. Ord a => a -> a -> Bool
< Integer
0] forall a. Num a => a -> a -> a
- Integer
1
Just (Integer
obj, Vector Bool
_) -> Integer
obj