msakai / toysolver / 767

Committed 22 May 2025 12:57PM UTC coverage: 71.847% (-0.06%) from 71.906%

Build # 767

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f4d92f6d1 into c10d256d2

Run Details

11104 of 15455 relevant lines covered (71.85%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

70.43

/src/ToySolver/SAT/PBO/BCD2.hs

{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.BCD2
-- Copyright   :  (c) Masahiro Sakai 2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Reference:
--
-- * Federico Heras, Antonio Morgado, João Marques-Silva,
--   Core-Guided binary search algorithms for maximum satisfiability,
--   Twenty-Fifth AAAI Conference on Artificial Intelligence, 2011.
--   <http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3713>
--
-- * A. Morgado, F. Heras, and J. Marques-Silva,
--   Improvements to Core-Guided binary search for MaxSAT,
--   in Theory and Applications of Satisfiability Testing (SAT 2012),
--   pp. 284-297.
--   <https://doi.org/10.1007/978-3-642-31612-8_22>
--   <http://ulir.ul.ie/handle/10344/2771>
--
-----------------------------------------------------------------------------
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

-- | Options for BCD2 algorithm.
--
-- The default value can be obtained by 'def'.
data Options
  = Options
  { optEnableHardening :: Bool
  , optEnableBiasedSearch :: Bool
  , optSolvingNormalFirst :: Bool
  }

instance Default Options where
  def =
    Options
    { optEnableHardening = True
    , optEnableBiasedSearch = True
    , optSolvingNormalFirst = True
    }

data CoreInfo
  = CoreInfo
  { coreLits :: SAT.LitSet
  , coreLBRef :: !(IORef Integer)
  , coreUBSelectors :: !(IORef (Map Integer SAT.Lit))
  }

newCoreInfo :: SAT.LitSet -> Integer -> IO CoreInfo
newCoreInfo lits lb = do
  lbRef <- newIORef lb
  selsRef <- newIORef Map.empty
  return
    CoreInfo
    { coreLits = lits
    , coreLBRef = lbRef
    , coreUBSelectors = selsRef
    }

deleteCoreInfo :: SAT.Solver -> CoreInfo -> IO ()
deleteCoreInfo solver core = do
  m <- readIORef (coreUBSelectors core)
  -- Delete soft upperbound constraints by fixing selector variables
  forM_ (Map.elems m) $ \sel ->
    SAT.addClause solver [-sel]

getCoreLB :: CoreInfo -> IO Integer
getCoreLB = readIORef . coreLBRef

solve :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
solve cxt solver opt = solveWBO (C.normalize cxt) solver opt

solveWBO :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
solveWBO cxt solver opt = do
  C.logMessage cxt $ printf "BCD2: Hardening is %s." (if optEnableHardening opt then "enabled" else "disabled")
  C.logMessage cxt $ printf "BCD2: BiasedSearch is %s." (if optEnableBiasedSearch opt then "enabled" else "disabled")

  SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }

  unrelaxedRef <- newIORef $ IntSet.fromList [lit | (lit,_) <- sels]
  relaxedRef   <- newIORef IntSet.empty
  hardenedRef  <- newIORef IntSet.empty
  nsatRef   <- newIORef 1
  nunsatRef <- newIORef 1

  lastUBRef <- newIORef $ SAT.pbLinUpperBound obj

  coresRef <- newIORef []
  let getLB = do
        xs <- readIORef coresRef
        foldM (\s core -> do{ v <- getCoreLB core; return $! s + v }) 0 xs

  deductedWeightRef <- newIORef weights
  let deductWeight d core =
        modifyIORef' deductedWeightRef $ IntMap.unionWith (+) $
          IntMap.fromSet (const (- d)) (coreLits core)
      updateLB oldLB core = do
        newLB <- getLB
        C.addLowerBound cxt newLB
        deductWeight (newLB - oldLB) core
        SAT.addPBAtLeast solver (coreCostFun core) =<< getCoreLB core -- redundant, but useful for direct search

  let loop = do
        lb <- getLB
        ub <- do
          ub1 <- atomically $ C.getSearchUpperBound cxt
          -- FIXME: The refinement should be done in Context.addSolution,
          -- for generality and to avoid duplicated computation.
          let ub2 = refineUB (map fst obj) ub1
          when (ub1 /= ub2) $ C.logMessage cxt $ printf "BCD2: refineUB: %d -> %d" ub1 ub2
          return ub2
        when (ub < lb) $ C.setFinished cxt

        fin <- atomically $ C.isFinished cxt
        unless fin $ do

          when (optEnableHardening opt) $ do
            deductedWeight <- readIORef deductedWeightRef
            hardened <- readIORef hardenedRef
            let lits = IntMap.keysSet (IntMap.filter (\w -> lb + w > ub) deductedWeight) `IntSet.difference` hardened
            unless (IntSet.null lits) $ do
              C.logMessage cxt $ printf "BCD2: hardening fixes %d literals" (IntSet.size lits)
              forM_ (IntSet.toList lits) $ \lit -> SAT.addClause solver [lit]
              modifyIORef unrelaxedRef (`IntSet.difference` lits)
              modifyIORef relaxedRef   (`IntSet.difference` lits)
              modifyIORef hardenedRef  (`IntSet.union` lits)

          ub0 <- readIORef lastUBRef
          when (ub < ub0) $ do
            C.logMessage cxt $ printf "BCD2: updating upper bound: %d -> %d" ub0 ub
            SAT.addPBAtMost solver obj ub
            writeIORef lastUBRef ub

          cores     <- readIORef coresRef
          unrelaxed <- readIORef unrelaxedRef
          relaxed   <- readIORef relaxedRef
          hardened  <- readIORef hardenedRef
          nsat   <- readIORef nsatRef
          nunsat <- readIORef nunsatRef
          C.logMessage cxt $ printf "BCD2: %d <= obj <= %d" lb ub
          C.logMessage cxt $ printf "BCD2: #cores=%d, #unrelaxed=%d, #relaxed=%d, #hardened=%d"
            (length cores) (IntSet.size unrelaxed) (IntSet.size relaxed) (IntSet.size hardened)
          C.logMessage cxt $ printf "BCD2: #sat=%d #unsat=%d bias=%d/%d" nsat nunsat nunsat (nunsat + nsat)

          lastModel <- atomically $ C.getBestModel cxt
          sels <- liftM IntMap.fromList $ forM cores $ \core -> do
            coreLB <- getCoreLB core
            let coreUB = SAT.pbLinUpperBound (coreCostFun core)
            if coreUB < coreLB then do
              -- Note: we have detected unsatisfiability
              C.logMessage cxt $ printf "BCD2: coreLB (%d) exceeds coreUB (%d)" coreLB coreUB
              SAT.addClause solver []
              sel <- getCoreUBAssumption core coreUB
              return (sel, (core, coreUB))
            else do
              let estimated =
                    case lastModel of
                      Nothing -> coreUB
                      Just m  ->
                        -- Since we might have added some hard constraints after obtaining @m@,
                        -- it's possible that @coreLB@ is larger than @SAT.evalPBLinSum m (coreCostFun core)@.
                        coreLB `max` SAT.evalPBLinSum m (coreCostFun core)
                  mid =
                    if optEnableBiasedSearch opt
                    then coreLB + (estimated - coreLB) * nunsat `div` (nunsat + nsat)
                    else (coreLB + estimated) `div` 2
              sel <- getCoreUBAssumption core mid
              return (sel, (core,mid))

          ret <- SAT.solveWith solver (IntMap.keys sels ++ IntSet.toList unrelaxed)

          if ret then do
            modifyIORef' nsatRef (+1)
            C.addSolution cxt =<< SAT.getModel solver
            loop
          else do
            modifyIORef' nunsatRef (+1)
            failed <- SAT.getFailedAssumptions solver

            case IntSet.toList failed of
              [] -> C.setFinished cxt
              [sel] | Just (core,mid) <- IntMap.lookup sel sels -> do
                C.logMessage cxt $ printf "BCD2: updating lower bound of a core"
                let newCoreLB  = mid + 1
                    newCoreLB' = refineLB (IntMap.elems (IntMap.restrictKeys weights (coreLits core))) newCoreLB
                when (newCoreLB /= newCoreLB') $ C.logMessage cxt $
                  printf "BCD2: refineLB: %d -> %d" newCoreLB newCoreLB'
                writeIORef (coreLBRef core) newCoreLB'
                SAT.addClause solver [-sel] -- Delete soft upperbound constraint(s) by fixing a selector variable
                updateLB lb core
                loop
              _ -> do
                let torelax     = unrelaxed `IntSet.intersection` failed
                    intersected = IntMap.elems (IntMap.restrictKeys sels failed)
                    disjoint    = [core | (_sel,(core,_)) <- IntMap.toList (IntMap.withoutKeys sels failed)]
                modifyIORef unrelaxedRef (`IntSet.difference` torelax)
                modifyIORef relaxedRef (`IntSet.union` torelax)
                delta <- do
                  xs1 <- forM intersected $ \(core,mid) -> do
                    coreLB <- getCoreLB core
                    return $ mid - coreLB + 1
                  let xs2 = [weights IntMap.! lit | lit <- IntSet.toList torelax]
                  return $! minimum (xs1 ++ xs2)
                let mergedCoreLits = IntSet.unions $ torelax : [coreLits core | (core,_) <- intersected]
                mergedCoreLB <- liftM ((delta +) . sum) $ mapM (getCoreLB . fst) intersected
                let mergedCoreLB' = refineLB (IntMap.elems (IntMap.restrictKeys weights mergedCoreLits)) mergedCoreLB
                mergedCore <- newCoreInfo mergedCoreLits mergedCoreLB'
                writeIORef coresRef (mergedCore : disjoint)
                forM_ intersected $ \(core, _) -> deleteCoreInfo solver core

                if null intersected then
                  C.logMessage cxt $ printf "BCD2: found a new core of size %d: cost of the new core is >=%d"
                    (IntSet.size torelax) mergedCoreLB'
                else
                  C.logMessage cxt $ printf "BCD2: relaxing %d and merging with %d cores into a new core of size %d: cost of the new core is >=%d"
                    (IntSet.size torelax) (length intersected) (IntSet.size mergedCoreLits) mergedCoreLB'
                when (mergedCoreLB /= mergedCoreLB') $
                  C.logMessage cxt $ printf "BCD2: refineLB: %d -> %d" mergedCoreLB mergedCoreLB'
                updateLB lb mergedCore
                loop

  best <- atomically $ C.getBestModel cxt
  case best of
    Nothing | optSolvingNormalFirst opt -> do
      ret <- SAT.solve solver
      if ret then
        C.addSolution cxt =<< SAT.getModel solver
      else
        C.setFinished cxt
    _ -> return ()
  loop

  where
    obj :: SAT.PBLinSum
    obj = C.getObjectiveFunction cxt

    sels :: [(SAT.Lit, Integer)]
    sels = [(-lit, w) | (w,lit) <- obj]

    weights :: SAT.LitMap Integer
    weights = IntMap.fromList sels

    coreCostFun :: CoreInfo -> SAT.PBLinSum
    coreCostFun c = [(weights IntMap.! lit, -lit) | lit <- IntSet.toList (coreLits c)]

    getCoreUBAssumption :: CoreInfo -> Integer -> IO SAT.Lit
    getCoreUBAssumption core ub = do
      m <- readIORef (coreUBSelectors core)
      case Map.splitLookup ub m of
        (_, Just sel, _) -> return sel
        (lo, Nothing, hi)  -> do
          sel <- SAT.newVar solver
          SAT.addPBAtMostSoft solver sel (coreCostFun core) ub
          writeIORef (coreUBSelectors core) (Map.insert ub sel m)
          unless (Map.null lo) $
            SAT.addClause solver [- snd (Map.findMax lo), sel] -- snd (Map.findMax lo) → sel
          unless (Map.null hi) $
            SAT.addClause solver [- sel, snd (Map.findMin hi)] -- sel → Map.findMin hi
          return sel

-- | The smallest integer greater-than or equal-to @n@ that can be obtained by summing a subset of @ws@.
-- Note that the definition is different from the one in Morgado et al.
refineLB
  :: [Integer] -- ^ @ws@
  -> Integer   -- ^ @n@
  -> Integer
refineLB ws n =
  case SubsetSum.minSubsetSum (V.fromList ws) n of
    Nothing -> sum [w | w <- ws, w > 0] + 1
    Just (obj, _) -> obj

-- | The greatest integer lesser-than or equal-to @n@ that can be obtained by summing a subset of @ws@.
refineUB
  :: [Integer] -- ^ @ws@
  -> Integer   -- ^ @n@
  -> Integer
refineUB ws n
  | n < 0 = n
  | otherwise =
      case SubsetSum.maxSubsetSum (V.fromList ws) n of
        Nothing -> sum [w | w <- ws, w < 0] - 1
        Just (obj, _) -> obj

1	{-# LANGUAGE BangPatterns #-}
2	{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
3	{-# OPTIONS_HADDOCK show-extensions #-}
4	-----------------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.SAT.PBO.BCD2
7	-- Copyright : (c) Masahiro Sakai 2014
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : provisional
12	-- Portability : non-portable
13	--
14	-- Reference:
15	--
16	-- * Federico Heras, Antonio Morgado, João Marques-Silva,
17	-- Core-Guided binary search algorithms for maximum satisfiability,
18	-- Twenty-Fifth AAAI Conference on Artificial Intelligence, 2011.
19	-- <http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3713>
20	--
21	-- * A. Morgado, F. Heras, and J. Marques-Silva,
22	-- Improvements to Core-Guided binary search for MaxSAT,
23	-- in Theory and Applications of Satisfiability Testing (SAT 2012),
24	-- pp. 284-297.
25	-- <https://doi.org/10.1007/978-3-642-31612-8_22>
26	-- <http://ulir.ul.ie/handle/10344/2771>
27	--
28	-----------------------------------------------------------------------------
29	module ToySolver.SAT.PBO.BCD2
30	( Options (..)
31	, solve
32	) where
33
34	import Control.Concurrent.STM
35	import Control.Monad
36	import Data.IORef
37	import Data.Default.Class
38	import qualified Data.IntSet as IntSet
39	import qualified Data.IntMap as IntMap
40	import Data.Map (Map)
41	import qualified Data.Map as Map
42	import qualified Data.Vector as V
43	import qualified ToySolver.SAT as SAT
44	import qualified ToySolver.SAT.Types as SAT
45	import qualified ToySolver.SAT.PBO.Context as C
46	import qualified ToySolver.Combinatorial.SubsetSum as SubsetSum
47	import Text.Printf
48
49	-- \| Options for BCD2 algorithm.
50	--
51	-- The default value can be obtained by 'def'.
52	data Options
53	= Options
54	{ optEnableHardening :: Bool	1✔
55	, optEnableBiasedSearch :: Bool	1✔
56	, optSolvingNormalFirst :: Bool	1✔
57	}
58
59	instance Default Options where
60	def =	1✔
61	Options	1✔
62	{ optEnableHardening = True	1✔
63	, optEnableBiasedSearch = True	1✔
64	, optSolvingNormalFirst = True	1✔
65	}
66
67	data CoreInfo
68	= CoreInfo
69	{ coreLits :: SAT.LitSet	1✔
70	, coreLBRef :: !(IORef Integer)	1✔
71	, coreUBSelectors :: !(IORef (Map Integer SAT.Lit))	1✔
72	}
73
74	newCoreInfo :: SAT.LitSet -> Integer -> IO CoreInfo
75	newCoreInfo lits lb = do	1✔
76	lbRef <- newIORef lb	1✔
77	selsRef <- newIORef Map.empty	1✔
78	return	1✔
79	CoreInfo	1✔
80	{ coreLits = lits	1✔
81	, coreLBRef = lbRef	1✔
82	, coreUBSelectors = selsRef	1✔
83	}
84
85	deleteCoreInfo :: SAT.Solver -> CoreInfo -> IO ()
86	deleteCoreInfo solver core = do	×
87	m <- readIORef (coreUBSelectors core)	×
88	-- Delete soft upperbound constraints by fixing selector variables
89	forM_ (Map.elems m) $ \sel ->	×
90	SAT.addClause solver [-sel]	×
91
92	getCoreLB :: CoreInfo -> IO Integer
93	getCoreLB = readIORef . coreLBRef	1✔
94
95	solve :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
96	solve cxt solver opt = solveWBO (C.normalize cxt) solver opt	1✔
97
98	solveWBO :: C.Context cxt => cxt -> SAT.Solver -> Options -> IO ()
99	solveWBO cxt solver opt = do	1✔
100	C.logMessage cxt $ printf "BCD2: Hardening is %s." (if optEnableHardening opt then "enabled" else "disabled")	×
101	C.logMessage cxt $ printf "BCD2: BiasedSearch is %s." (if optEnableBiasedSearch opt then "enabled" else "disabled")	×
102
103	SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }	1✔
104
105	unrelaxedRef <- newIORef $ IntSet.fromList [lit \| (lit,_) <- sels]	1✔
106	relaxedRef <- newIORef IntSet.empty	×
107	hardenedRef <- newIORef IntSet.empty	1✔
108	nsatRef <- newIORef 1	1✔
109	nunsatRef <- newIORef 1	1✔
110
111	lastUBRef <- newIORef $ SAT.pbLinUpperBound obj	1✔
112
113	coresRef <- newIORef []	1✔
114	let getLB = do	1✔
115	xs <- readIORef coresRef	1✔
116	foldM (\s core -> do{ v <- getCoreLB core; return $! s + v }) 0 xs	1✔
117
118	deductedWeightRef <- newIORef weights	1✔
119	let deductWeight d core =	1✔
120	modifyIORef' deductedWeightRef $ IntMap.unionWith (+) $	1✔
121	IntMap.fromSet (const (- d)) (coreLits core)	1✔
122	updateLB oldLB core = do	1✔
123	newLB <- getLB	1✔
124	C.addLowerBound cxt newLB	1✔
125	deductWeight (newLB - oldLB) core	1✔
126	SAT.addPBAtLeast solver (coreCostFun core) =<< getCoreLB core -- redundant, but useful for direct search	1✔
127
128	let loop = do	1✔
129	lb <- getLB	1✔
130	ub <- do	1✔
131	ub1 <- atomically $ C.getSearchUpperBound cxt	1✔
132	-- FIXME: The refinement should be done in Context.addSolution,
133	-- for generality and to avoid duplicated computation.
134	let ub2 = refineUB (map fst obj) ub1	1✔
135	when (ub1 /= ub2) $ C.logMessage cxt $ printf "BCD2: refineUB: %d -> %d" ub1 ub2	×
136	return ub2	1✔
137	when (ub < lb) $ C.setFinished cxt	1✔
138
139	fin <- atomically $ C.isFinished cxt	1✔
140	unless fin $ do	1✔
141
142	when (optEnableHardening opt) $ do	1✔
143	deductedWeight <- readIORef deductedWeightRef	1✔
144	hardened <- readIORef hardenedRef	1✔
145	let lits = IntMap.keysSet (IntMap.filter (\w -> lb + w > ub) deductedWeight) `IntSet.difference` hardened	1✔
146	unless (IntSet.null lits) $ do	1✔
147	C.logMessage cxt $ printf "BCD2: hardening fixes %d literals" (IntSet.size lits)	×
148	forM_ (IntSet.toList lits) $ \lit -> SAT.addClause solver [lit]	1✔
149	modifyIORef unrelaxedRef (`IntSet.difference` lits)	1✔
150	modifyIORef relaxedRef (`IntSet.difference` lits)	×
151	modifyIORef hardenedRef (`IntSet.union` lits)	×
152
153	ub0 <- readIORef lastUBRef	1✔
154	when (ub < ub0) $ do	1✔
155	C.logMessage cxt $ printf "BCD2: updating upper bound: %d -> %d" ub0 ub	×
156	SAT.addPBAtMost solver obj ub	1✔
157	writeIORef lastUBRef ub	1✔
158
159	cores <- readIORef coresRef	1✔
160	unrelaxed <- readIORef unrelaxedRef	1✔
161	relaxed <- readIORef relaxedRef	1✔
162	hardened <- readIORef hardenedRef	1✔
163	nsat <- readIORef nsatRef	1✔
164	nunsat <- readIORef nunsatRef	1✔
165	C.logMessage cxt $ printf "BCD2: %d <= obj <= %d" lb ub	×
166	C.logMessage cxt $ printf "BCD2: #cores=%d, #unrelaxed=%d, #relaxed=%d, #hardened=%d"	×
167	(length cores) (IntSet.size unrelaxed) (IntSet.size relaxed) (IntSet.size hardened)	×
168	C.logMessage cxt $ printf "BCD2: #sat=%d #unsat=%d bias=%d/%d" nsat nunsat nunsat (nunsat + nsat)	×
169
170	lastModel <- atomically $ C.getBestModel cxt	1✔
171	sels <- liftM IntMap.fromList $ forM cores $ \core -> do	1✔
172	coreLB <- getCoreLB core	1✔
173	let coreUB = SAT.pbLinUpperBound (coreCostFun core)	1✔
174	if coreUB < coreLB then do	×
175	-- Note: we have detected unsatisfiability
176	C.logMessage cxt $ printf "BCD2: coreLB (%d) exceeds coreUB (%d)" coreLB coreUB	×
177	SAT.addClause solver []	×
178	sel <- getCoreUBAssumption core coreUB	×
179	return (sel, (core, coreUB))	×
180	else do	1✔
181	let estimated =	1✔
182	case lastModel of	1✔
183	Nothing -> coreUB	×
184	Just m ->
185	-- Since we might have added some hard constraints after obtaining @m@,
186	-- it's possible that @coreLB@ is larger than @SAT.evalPBLinSum m (coreCostFun core)@.
187	coreLB `max` SAT.evalPBLinSum m (coreCostFun core)	1✔
188	mid =	1✔
189	if optEnableBiasedSearch opt	×
190	then coreLB + (estimated - coreLB) * nunsat `div` (nunsat + nsat)	1✔
191	else (coreLB + estimated) `div` 2	×
192	sel <- getCoreUBAssumption core mid	1✔
193	return (sel, (core,mid))	×
194
195	ret <- SAT.solveWith solver (IntMap.keys sels ++ IntSet.toList unrelaxed)	1✔
196
197	if ret then do	1✔
198	modifyIORef' nsatRef (+1)	1✔
199	C.addSolution cxt =<< SAT.getModel solver	1✔
200	loop	1✔
201	else do	1✔
202	modifyIORef' nunsatRef (+1)	1✔
203	failed <- SAT.getFailedAssumptions solver	1✔
204
205	case IntSet.toList failed of	1✔
206	[] -> C.setFinished cxt	1✔
207	[sel] \| Just (core,mid) <- IntMap.lookup sel sels -> do	×
208	C.logMessage cxt $ printf "BCD2: updating lower bound of a core"	×
209	let newCoreLB = mid + 1	×
210	newCoreLB' = refineLB (IntMap.elems (IntMap.restrictKeys weights (coreLits core))) newCoreLB	×
211	when (newCoreLB /= newCoreLB') $ C.logMessage cxt $	×
212	printf "BCD2: refineLB: %d -> %d" newCoreLB newCoreLB'	×
213	writeIORef (coreLBRef core) newCoreLB'	×
214	SAT.addClause solver [-sel] -- Delete soft upperbound constraint(s) by fixing a selector variable	×
215	updateLB lb core	×
216	loop	×
217	_ -> do	1✔
218	let torelax = unrelaxed `IntSet.intersection` failed	1✔
219	intersected = IntMap.elems (IntMap.restrictKeys sels failed)	1✔
220	disjoint = [core \| (_sel,(core,_)) <- IntMap.toList (IntMap.withoutKeys sels failed)]	1✔
221	modifyIORef unrelaxedRef (`IntSet.difference` torelax)	1✔
222	modifyIORef relaxedRef (`IntSet.union` torelax)	×
223	delta <- do	1✔
224	xs1 <- forM intersected $ \(core,mid) -> do	×
225	coreLB <- getCoreLB core	×
226	return $ mid - coreLB + 1	×
227	let xs2 = [weights IntMap.! lit \| lit <- IntSet.toList torelax]	1✔
228	return $! minimum (xs1 ++ xs2)	1✔
229	let mergedCoreLits = IntSet.unions $ torelax : [coreLits core \| (core,_) <- intersected]	×
230	mergedCoreLB <- liftM ((delta +) . sum) $ mapM (getCoreLB . fst) intersected	×
231	let mergedCoreLB' = refineLB (IntMap.elems (IntMap.restrictKeys weights mergedCoreLits)) mergedCoreLB	1✔
232	mergedCore <- newCoreInfo mergedCoreLits mergedCoreLB'	1✔
233	writeIORef coresRef (mergedCore : disjoint)	1✔
234	forM_ intersected $ \(core, _) -> deleteCoreInfo solver core	×
235
236	if null intersected then	×
237	C.logMessage cxt $ printf "BCD2: found a new core of size %d: cost of the new core is >=%d"	×
238	(IntSet.size torelax) mergedCoreLB'	×
239	else
240	C.logMessage cxt $ printf "BCD2: relaxing %d and merging with %d cores into a new core of size %d: cost of the new core is >=%d"	×
241	(IntSet.size torelax) (length intersected) (IntSet.size mergedCoreLits) mergedCoreLB'	×
242	when (mergedCoreLB /= mergedCoreLB') $	1✔
243	C.logMessage cxt $ printf "BCD2: refineLB: %d -> %d" mergedCoreLB mergedCoreLB'	×
244	updateLB lb mergedCore	1✔
245	loop	1✔
246
247	best <- atomically $ C.getBestModel cxt	1✔
248	case best of	1✔
249	Nothing \| optSolvingNormalFirst opt -> do	×
250	ret <- SAT.solve solver	1✔
251	if ret then	1✔
252	C.addSolution cxt =<< SAT.getModel solver	1✔
253	else
254	C.setFinished cxt	1✔
255	_ -> return ()	×
256	loop	1✔
257
258	where
259	obj :: SAT.PBLinSum
260	obj = C.getObjectiveFunction cxt	1✔
261
262	sels :: [(SAT.Lit, Integer)]
263	sels = [(-lit, w) \| (w,lit) <- obj]	1✔
264
265	weights :: SAT.LitMap Integer
266	weights = IntMap.fromList sels	1✔
267
268	coreCostFun :: CoreInfo -> SAT.PBLinSum
269	coreCostFun c = [(weights IntMap.! lit, -lit) \| lit <- IntSet.toList (coreLits c)]	1✔
270
271	getCoreUBAssumption :: CoreInfo -> Integer -> IO SAT.Lit
272	getCoreUBAssumption core ub = do	1✔
273	m <- readIORef (coreUBSelectors core)	1✔
274	case Map.splitLookup ub m of	1✔
275	(_, Just sel, _) -> return sel	1✔
276	(lo, Nothing, hi) -> do	1✔
277	sel <- SAT.newVar solver	1✔
278	SAT.addPBAtMostSoft solver sel (coreCostFun core) ub	1✔
279	writeIORef (coreUBSelectors core) (Map.insert ub sel m)	1✔
280	unless (Map.null lo) $	1✔
281	SAT.addClause solver [- snd (Map.findMax lo), sel] -- snd (Map.findMax lo) → sel	×
282	unless (Map.null hi) $	1✔
283	SAT.addClause solver [- sel, snd (Map.findMin hi)] -- sel → Map.findMin hi	×
284	return sel	1✔
285
286	-- \| The smallest integer greater-than or equal-to @n@ that can be obtained by summing a subset of @ws@.
287	-- Note that the definition is different from the one in Morgado et al.
288	refineLB
289	:: [Integer] -- ^ @ws@
290	-> Integer -- ^ @n@
291	-> Integer
292	refineLB ws n =	1✔
293	case SubsetSum.minSubsetSum (V.fromList ws) n of	1✔
294	Nothing -> sum [w \| w <- ws, w > 0] + 1	×
295	Just (obj, _) -> obj	1✔
296
297	-- \| The greatest integer lesser-than or equal-to @n@ that can be obtained by summing a subset of @ws@.
298	refineUB
299	:: [Integer] -- ^ @ws@
300	-> Integer -- ^ @n@
301	-> Integer
302	refineUB ws n	1✔
303	\| n < 0 = n	1✔
304	\| otherwise =	×
305	case SubsetSum.maxSubsetSum (V.fromList ws) n of	1✔
306	Nothing -> sum [w \| w <- ws, w < 0] - 1	×
307	Just (obj, _) -> obj	1✔

msakai / toysolver / 767

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous