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

68.57

/src/ToySolver/SAT/PBO.hs

{-# 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 (Eq, Ord, Show, Enum, Bounded)

instance Default Method where
  def = LinearSearch

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

parseMethod :: String -> Maybe Method
parseMethod s =
  case map toLower s of
    "linear"   -> Just LinearSearch
    "binary"   -> Just BinarySearch
    "adaptive" -> Just AdaptiveSearch
    "unsat"    -> Just UnsatBased
    "msu4"     -> Just MSU4
    "bc"       -> Just BC
    "bcd"      -> Just BCD
    "bcd2"     -> Just BCD2
    _ -> Nothing

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

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

newOptimizer2 :: SAT.Solver -> SAT.PBLinSum -> (SAT.Model -> Integer) -> IO Optimizer
newOptimizer2 solver obj obj2 = do
  cxt <- C.newSimpleContext2 obj obj2
  strategyRef   <- newIORef def
  heuristicsRef <- newIORef defaultEnableObjFunVarsHeuristics
  trialLimitRef <- newIORef defaultTrialLimitConf
  return $
    Optimizer
    { optContext = cxt
    , optSolver = solver
    , optMethodRef = strategyRef
    , optEnableObjFunVarsHeuristicsRef = heuristicsRef
    , optTrialLimitConfRef = trialLimitRef
    }

optimize :: Optimizer -> IO ()
optimize opt = do
  let cxt = optContext opt
  let obj = C.getObjectiveFunction cxt
  let solver = optSolver opt

  getEnableObjFunVarsHeuristics opt >>= \b ->
    when b $ tweakParams solver obj

  m <- getBestModel opt
  case m of
    Nothing -> return ()
    Just m -> do
      forM_ (assocs m) $ \(v, val) -> do
        SAT.setVarPolarity solver v val

  strategy <- getMethod opt
  case strategy of
    UnsatBased -> UnsatBased.solve cxt solver
    MSU4 -> MSU4.solve cxt solver
    BC   -> BC.solve cxt solver
    BCD  -> BCD.solve cxt solver
    BCD2 -> do
      let opt2 = def
      BCD2.solve cxt solver opt2
    _ -> do
      SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }

      join $ atomically $ do
        ret <- C.getBestValue cxt
        case ret of
          Just _ -> return $ return ()
          Nothing -> return $ do
            result <- SAT.solve solver
            if not result then
              C.setFinished cxt
            else do
              m <- SAT.getModel solver
              C.addSolution cxt m

      join $ atomically $ do
        ret <- C.getBestValue cxt
        case ret of
          Nothing  -> return $ return ()
          Just val -> return $ do
            let ub = val - 1
            SAT.addPBAtMost solver obj ub

      case strategy of
        LinearSearch   -> linSearch cxt solver
        BinarySearch   -> binSearch cxt solver
        AdaptiveSearch -> do
          lim <- getTrialLimitConf opt
          adaptiveSearch cxt solver lim
        _              -> error "ToySolver.SAT.PBO.minimize: should not happen"

getMethod :: Optimizer -> IO Method
getMethod opt = readIORef (optMethodRef opt)

setMethod :: Optimizer -> Method -> IO ()
setMethod opt val = writeIORef (optMethodRef opt) val

defaultEnableObjFunVarsHeuristics :: Bool
defaultEnableObjFunVarsHeuristics = False

getEnableObjFunVarsHeuristics :: Optimizer -> IO Bool
getEnableObjFunVarsHeuristics opt = readIORef (optEnableObjFunVarsHeuristicsRef opt)

setEnableObjFunVarsHeuristics :: Optimizer -> Bool -> IO ()
setEnableObjFunVarsHeuristics opt val = writeIORef (optEnableObjFunVarsHeuristicsRef opt) val

defaultTrialLimitConf :: Int
defaultTrialLimitConf = 1000

getTrialLimitConf :: Optimizer -> IO Int
getTrialLimitConf opt = readIORef (optTrialLimitConfRef opt)

setTrialLimitConf :: Optimizer -> Int -> IO ()
setTrialLimitConf opt val = writeIORef (optTrialLimitConfRef opt) val


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

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

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


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

getBestSolution :: Optimizer -> IO (Maybe (SAT.Model, Integer))
getBestSolution opt = atomically $ C.getBestSolution (optContext opt)

getBestValue :: Optimizer -> IO (Maybe Integer)
getBestValue opt = atomically $ C.getBestValue (optContext opt)

getBestModel :: Optimizer -> IO (Maybe SAT.Model)
getBestModel opt = atomically $ C.getBestModel (optContext opt)

isUnsat :: Optimizer -> IO Bool
isUnsat opt = atomically $ C.isUnsat (optContext opt)

isOptimum :: Optimizer -> IO Bool
isOptimum opt = atomically $ C.isOptimum (optContext opt)

isFinished :: Optimizer -> IO Bool
isFinished opt = atomically $ C.isFinished (optContext opt)


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

    loop :: IO ()
    loop = do
      result <- SAT.solve solver
      if result then do
        m <- SAT.getModel solver
        let val = C.evalObjectiveFunction cxt m
        let ub = val - 1
        C.addSolution cxt m
        SAT.addPBAtMost solver obj ub
        loop
      else do
        C.setFinished cxt
        return ()

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

    loop :: IO ()
    loop = join $ atomically $ do
      ub <- C.getSearchUpperBound cxt
      lb <- C.getLowerBound cxt
      if ub < lb then do
        return $ C.setFinished cxt
      else
        return $ do
          let mid = (lb + ub) `div` 2
          C.logMessage cxt $ printf "Binary Search: %d <= obj <= %d; guessing obj <= %d" lb ub mid
          sel <- SAT.newVar solver
          SAT.addPBAtMostSoft solver sel obj mid
          ret <- SAT.solveWith solver [sel]
          if ret then do
            m <- SAT.getModel solver
            let v = C.evalObjectiveFunction cxt m
            let ub' = v - 1
            C.logMessage cxt $ printf "Binary Search: updating upper bound: %d -> %d" ub ub'
            C.addSolution cxt m
            -- old upper bound constraints will be removed by backward subsumption removal
            SAT.addClause solver [sel]
            SAT.addPBAtMost solver obj ub'
            loop
          else do
            -- deleting temporary constraint
            SAT.addClause solver [-sel]
            let lb' = mid + 1
            C.logMessage cxt $ printf "Binary Search: updating lower bound: %d -> %d" lb lb'
            C.addLowerBound cxt lb'
            SAT.addPBAtLeast solver obj lb'
            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 trialLimitConf = loop 0
  where
    obj = C.getObjectiveFunction cxt

    loop :: Rational -> IO ()
    loop fraction = join $ atomically $ do
      ub <- C.getSearchUpperBound cxt
      lb <- C.getLowerBound cxt
      if ub < lb then
        return $ C.setFinished cxt
      else
        return $ do
          let interval = ub - lb
              mid = ub - floor (fromIntegral interval * fraction)
          if ub == mid then do
            C.logMessage cxt $ printf "Adaptive Search: %d <= obj <= %d" lb ub
            result <- SAT.solve solver
            if result then do
              m <- SAT.getModel solver
              let v = C.evalObjectiveFunction cxt m
              let ub' = v - 1
              C.addSolution cxt m
              SAT.addPBAtMost solver obj ub'
              let fraction' = min 0.5 (fraction + 0.1)
              loop fraction'
            else
              C.setFinished cxt
          else do
            C.logMessage cxt $ printf "Adaptive Search: %d <= obj <= %d; guessing obj <= %d" lb ub mid
            sel <- SAT.newVar solver
            SAT.addPBAtMostSoft solver sel obj mid
            SAT.setConfBudget solver $ Just trialLimitConf
            ret' <- try $ SAT.solveWith solver [sel]
            SAT.setConfBudget solver Nothing
            case ret' of
              Left SAT.BudgetExceeded -> do
                let fraction' = max 0 (fraction - 0.05)
                loop fraction'
              Right ret -> do
                let fraction' = min 0.5 (fraction + 0.1)
                if ret then do
                  m <- SAT.getModel solver
                  let v = C.evalObjectiveFunction cxt m
                  let ub' = v - 1
                  C.logMessage cxt $ printf "Adaptive Search: updating upper bound: %d -> %d" ub ub'
                  C.addSolution cxt m
                  -- old upper bound constraints will be removed by backward subsumption removal
                  SAT.addClause solver [sel]
                  SAT.addPBAtMost solver obj ub'
                  loop fraction'
                else do
                  -- deleting temporary constraint
                  SAT.addClause solver [-sel]
                  let lb' = mid + 1
                  C.logMessage cxt $ printf "Adaptive Search: updating lower bound: %d -> %d" lb lb'
                  C.addLowerBound cxt lb'
                  SAT.addPBAtLeast solver obj lb'
                  loop fraction'

tweakParams :: SAT.Solver -> SAT.PBLinSum -> IO ()
tweakParams solver obj = do
  forM_ obj $ \(c,l) -> do
    let p = if c > 0 then not (SAT.litPolarity l) else SAT.litPolarity l
    SAT.setVarPolarity solver (SAT.litVar l) p
  let cs = Set.fromList [abs c | (c,_) <- obj]
      ws = Map.fromAscList $ zip (Set.toAscList cs) [1..]
  forM_ obj $ \(c,l) -> do
    let w = ws Map.! abs c
    replicateM w $ SAT.varBumpActivity solver (SAT.litVar l)

1	{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
2	-----------------------------------------------------------------------------
3	-- \|
4	-- Module : ToySolver.SAT.PBO
5	-- Copyright : (c) Masahiro Sakai 2012-2013
6	-- License : BSD-style
7	--
8	-- Maintainer : masahiro.sakai@gmail.com
9	-- Stability : provisional
10	-- Portability : portable
11	--
12	-- Pseudo-Boolean Optimization (PBO) Solver
13	--
14	-----------------------------------------------------------------------------
15	module ToySolver.SAT.PBO
16	(
17	-- * The @Optimizer@ type
18	Optimizer
19	, newOptimizer
20	, newOptimizer2
21
22	-- * Solving
23	, optimize
24	, addSolution
25
26	-- * Extract results
27	, getBestSolution
28	, getBestValue
29	, getBestModel
30	, isUnsat
31	, isOptimum
32	, isFinished
33
34	-- * Configulation
35	, Method (..)
36	, showMethod
37	, parseMethod
38	, getMethod
39	, setMethod
40	, defaultEnableObjFunVarsHeuristics
41	, getEnableObjFunVarsHeuristics
42	, setEnableObjFunVarsHeuristics
43	, defaultTrialLimitConf
44	, getTrialLimitConf
45	, setTrialLimitConf
46	, setOnUpdateBestSolution
47	, setOnUpdateLowerBound
48	, setLogger
49	) where
50
51	import Control.Concurrent.STM
52	import Control.Exception
53	import Control.Monad
54	import Data.Array.IArray
55	import Data.Char
56	import Data.Default.Class
57	import Data.IORef
58	import qualified Data.Set as Set
59	import qualified Data.Map as Map
60	import Text.Printf
61	import qualified ToySolver.SAT as SAT
62	import qualified ToySolver.SAT.PBO.Context as C
63	import qualified ToySolver.SAT.PBO.BC as BC
64	import qualified ToySolver.SAT.PBO.BCD as BCD
65	import qualified ToySolver.SAT.PBO.BCD2 as BCD2
66	import qualified ToySolver.SAT.PBO.UnsatBased as UnsatBased
67	import qualified ToySolver.SAT.PBO.MSU4 as MSU4
68
69	-- \| Optimization method
70	--
71	-- The default value can be obtained by 'def'.
72	data Method
73	= LinearSearch
74	\| BinarySearch
75	\| AdaptiveSearch
76	\| UnsatBased
77	\| MSU4
78	\| BC
79	\| BCD
80	\| BCD2
81	deriving (Eq, Ord, Show, Enum, Bounded)	×
82
83	instance Default Method where
84	def = LinearSearch	×
85
86	showMethod :: Method -> String
87	showMethod m =	×
88	case m of	×
89	LinearSearch -> "linear"	×
90	BinarySearch -> "binary"	×
91	AdaptiveSearch -> "adaptive"	×
92	UnsatBased -> "unsat-based"	×
93	MSU4 -> "msu4"	×
94	BC -> "bc"	×
95	BCD -> "bcd"	×
96	BCD2 -> "bcd2"	×
97
98	parseMethod :: String -> Maybe Method
99	parseMethod s =	×
100	case map toLower s of	×
101	"linear" -> Just LinearSearch	×
102	"binary" -> Just BinarySearch	×
103	"adaptive" -> Just AdaptiveSearch	×
104	"unsat" -> Just UnsatBased	×
105	"msu4" -> Just MSU4	×
106	"bc" -> Just BC	×
107	"bcd" -> Just BCD	×
108	"bcd2" -> Just BCD2	×
109	_ -> Nothing	×
110
111	data Optimizer
112	= Optimizer
113	{ optContext :: C.SimpleContext	1✔
114	, optSolver :: SAT.Solver	1✔
115	, optMethodRef :: IORef Method	1✔
116	, optEnableObjFunVarsHeuristicsRef :: IORef Bool	1✔
117	, optTrialLimitConfRef :: IORef Int	1✔
118	}
119
120	newOptimizer :: SAT.Solver -> SAT.PBLinSum -> IO Optimizer
121	newOptimizer solver obj = newOptimizer2 solver obj (\m -> SAT.evalPBLinSum m obj)	1✔
122
123	newOptimizer2 :: SAT.Solver -> SAT.PBLinSum -> (SAT.Model -> Integer) -> IO Optimizer
124	newOptimizer2 solver obj obj2 = do	1✔
125	cxt <- C.newSimpleContext2 obj obj2	1✔
126	strategyRef <- newIORef def	×
127	heuristicsRef <- newIORef defaultEnableObjFunVarsHeuristics	1✔
128	trialLimitRef <- newIORef defaultTrialLimitConf	1✔
129	return $	1✔
130	Optimizer	1✔
131	{ optContext = cxt	1✔
132	, optSolver = solver	1✔
133	, optMethodRef = strategyRef	1✔
134	, optEnableObjFunVarsHeuristicsRef = heuristicsRef	1✔
135	, optTrialLimitConfRef = trialLimitRef	1✔
136	}
137
138	optimize :: Optimizer -> IO ()
139	optimize opt = do	1✔
140	let cxt = optContext opt	1✔
141	let obj = C.getObjectiveFunction cxt	1✔
142	let solver = optSolver opt	1✔
143
144	getEnableObjFunVarsHeuristics opt >>= \b ->	1✔
145	when b $ tweakParams solver obj	×
146
147	m <- getBestModel opt	1✔
148	case m of	1✔
149	Nothing -> return ()	×
150	Just m -> do	×
151	forM_ (assocs m) $ \(v, val) -> do	×
152	SAT.setVarPolarity solver v val	×
153
154	strategy <- getMethod opt	1✔
155	case strategy of	1✔
156	UnsatBased -> UnsatBased.solve cxt solver	1✔
157	MSU4 -> MSU4.solve cxt solver	1✔
158	BC -> BC.solve cxt solver	1✔
159	BCD -> BCD.solve cxt solver	1✔
160	BCD2 -> do	1✔
161	let opt2 = def	1✔
162	BCD2.solve cxt solver opt2	1✔
163	_ -> do	1✔
164	SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }	1✔
165
166	join $ atomically $ do	1✔
167	ret <- C.getBestValue cxt	1✔
168	case ret of	1✔
169	Just _ -> return $ return ()	×
170	Nothing -> return $ do	1✔
171	result <- SAT.solve solver	1✔
172	if not result then	1✔
173	C.setFinished cxt	1✔
174	else do	1✔
175	m <- SAT.getModel solver	1✔
176	C.addSolution cxt m	1✔
177
178	join $ atomically $ do	1✔
179	ret <- C.getBestValue cxt	1✔
180	case ret of	1✔
181	Nothing -> return $ return ()	×
182	Just val -> return $ do	1✔
183	let ub = val - 1	1✔
184	SAT.addPBAtMost solver obj ub	1✔
185
186	case strategy of	1✔
187	LinearSearch -> linSearch cxt solver	1✔
188	BinarySearch -> binSearch cxt solver	1✔
189	AdaptiveSearch -> do	1✔
190	lim <- getTrialLimitConf opt	1✔
191	adaptiveSearch cxt solver lim	1✔
192	_ -> error "ToySolver.SAT.PBO.minimize: should not happen"	×
193
194	getMethod :: Optimizer -> IO Method
195	getMethod opt = readIORef (optMethodRef opt)	1✔
196
197	setMethod :: Optimizer -> Method -> IO ()
198	setMethod opt val = writeIORef (optMethodRef opt) val	1✔
199
200	defaultEnableObjFunVarsHeuristics :: Bool
201	defaultEnableObjFunVarsHeuristics = False	1✔
202
203	getEnableObjFunVarsHeuristics :: Optimizer -> IO Bool
204	getEnableObjFunVarsHeuristics opt = readIORef (optEnableObjFunVarsHeuristicsRef opt)	1✔
205
206	setEnableObjFunVarsHeuristics :: Optimizer -> Bool -> IO ()
207	setEnableObjFunVarsHeuristics opt val = writeIORef (optEnableObjFunVarsHeuristicsRef opt) val	×
208
209	defaultTrialLimitConf :: Int
210	defaultTrialLimitConf = 1000	1✔
211
212	getTrialLimitConf :: Optimizer -> IO Int
213	getTrialLimitConf opt = readIORef (optTrialLimitConfRef opt)	1✔
214
215	setTrialLimitConf :: Optimizer -> Int -> IO ()
216	setTrialLimitConf opt val = writeIORef (optTrialLimitConfRef opt) val	×
217
218
219	setOnUpdateBestSolution :: Optimizer -> (SAT.Model -> Integer -> IO ()) -> IO ()
220	setOnUpdateBestSolution opt cb = C.setOnUpdateBestSolution (optContext opt) cb	×
221
222	setOnUpdateLowerBound :: Optimizer -> (Integer -> IO ()) -> IO ()
223	setOnUpdateLowerBound opt cb = C.setOnUpdateLowerBound (optContext opt) cb	×
224
225	setLogger :: Optimizer -> (String -> IO ()) -> IO ()
226	setLogger opt cb = C.setLogger (optContext opt) cb	×
227
228
229	addSolution :: Optimizer -> SAT.Model -> IO ()
230	addSolution opt m = C.addSolution (optContext opt) m	×
231
232	getBestSolution :: Optimizer -> IO (Maybe (SAT.Model, Integer))
233	getBestSolution opt = atomically $ C.getBestSolution (optContext opt)	1✔
234
235	getBestValue :: Optimizer -> IO (Maybe Integer)
236	getBestValue opt = atomically $ C.getBestValue (optContext opt)	×
237
238	getBestModel :: Optimizer -> IO (Maybe SAT.Model)
239	getBestModel opt = atomically $ C.getBestModel (optContext opt)	1✔
240
241	isUnsat :: Optimizer -> IO Bool
242	isUnsat opt = atomically $ C.isUnsat (optContext opt)	×
243
244	isOptimum :: Optimizer -> IO Bool
245	isOptimum opt = atomically $ C.isOptimum (optContext opt)	×
246
247	isFinished :: Optimizer -> IO Bool
248	isFinished opt = atomically $ C.isFinished (optContext opt)	×
249
250
251	linSearch :: C.Context cxt => cxt -> SAT.Solver -> IO ()
252	linSearch cxt solver = loop	1✔
253	where
254	obj = C.getObjectiveFunction cxt	1✔
255
256	loop :: IO ()
257	loop = do	1✔
258	result <- SAT.solve solver	1✔
259	if result then do	1✔
260	m <- SAT.getModel solver	1✔
261	let val = C.evalObjectiveFunction cxt m	1✔
262	let ub = val - 1	1✔
263	C.addSolution cxt m	1✔
264	SAT.addPBAtMost solver obj ub	1✔
265	loop	1✔
266	else do	1✔
267	C.setFinished cxt	1✔
268	return ()	×
269
270	binSearch :: C.Context cxt => cxt -> SAT.Solver -> IO ()
271	binSearch cxt solver = loop	1✔
272	where
273	obj = C.getObjectiveFunction cxt	1✔
274
275	loop :: IO ()
276	loop = join $ atomically $ do	1✔
277	ub <- C.getSearchUpperBound cxt	1✔
278	lb <- C.getLowerBound cxt	1✔
279	if ub < lb then do	1✔
280	return $ C.setFinished cxt	1✔
281	else
282	return $ do	1✔
283	let mid = (lb + ub) `div` 2	1✔
284	C.logMessage cxt $ printf "Binary Search: %d <= obj <= %d; guessing obj <= %d" lb ub mid	×
285	sel <- SAT.newVar solver	1✔
286	SAT.addPBAtMostSoft solver sel obj mid	1✔
287	ret <- SAT.solveWith solver [sel]	1✔
288	if ret then do	1✔
289	m <- SAT.getModel solver	1✔
290	let v = C.evalObjectiveFunction cxt m	1✔
291	let ub' = v - 1	1✔
292	C.logMessage cxt $ printf "Binary Search: updating upper bound: %d -> %d" ub ub'	×
293	C.addSolution cxt m	1✔
294	-- old upper bound constraints will be removed by backward subsumption removal
295	SAT.addClause solver [sel]	1✔
296	SAT.addPBAtMost solver obj ub'	1✔
297	loop	1✔
298	else do	1✔
299	-- deleting temporary constraint
300	SAT.addClause solver [-sel]	×
301	let lb' = mid + 1	1✔
302	C.logMessage cxt $ printf "Binary Search: updating lower bound: %d -> %d" lb lb'	×
303	C.addLowerBound cxt lb'	1✔
304	SAT.addPBAtLeast solver obj lb'	×
305	loop	1✔
306
307	-- adaptive search strategy from pbct-0.1.3 <http://www.residual.se/pbct/>
308	adaptiveSearch :: C.Context cxt => cxt -> SAT.Solver -> Int -> IO ()
309	adaptiveSearch cxt solver trialLimitConf = loop 0	1✔
310	where
311	obj = C.getObjectiveFunction cxt	1✔
312
313	loop :: Rational -> IO ()
314	loop fraction = join $ atomically $ do	1✔
315	ub <- C.getSearchUpperBound cxt	1✔
316	lb <- C.getLowerBound cxt	1✔
317	if ub < lb then	1✔
318	return $ C.setFinished cxt	1✔
319	else
320	return $ do	1✔
321	let interval = ub - lb	1✔
322	mid = ub - floor (fromIntegral interval * fraction)	1✔
323	if ub == mid then do	1✔
324	C.logMessage cxt $ printf "Adaptive Search: %d <= obj <= %d" lb ub	×
325	result <- SAT.solve solver	1✔
326	if result then do	1✔
327	m <- SAT.getModel solver	1✔
328	let v = C.evalObjectiveFunction cxt m	1✔
329	let ub' = v - 1	1✔
330	C.addSolution cxt m	1✔
331	SAT.addPBAtMost solver obj ub'	1✔
332	let fraction' = min 0.5 (fraction + 0.1)	1✔
333	loop fraction'	1✔
334	else
335	C.setFinished cxt	1✔
336	else do	1✔
337	C.logMessage cxt $ printf "Adaptive Search: %d <= obj <= %d; guessing obj <= %d" lb ub mid	×
338	sel <- SAT.newVar solver	1✔
339	SAT.addPBAtMostSoft solver sel obj mid	1✔
340	SAT.setConfBudget solver $ Just trialLimitConf	1✔
341	ret' <- try $ SAT.solveWith solver [sel]	1✔
342	SAT.setConfBudget solver Nothing	1✔
343	case ret' of	1✔
344	Left SAT.BudgetExceeded -> do	×
345	let fraction' = max 0 (fraction - 0.05)	×
346	loop fraction'	×
347	Right ret -> do	1✔
348	let fraction' = min 0.5 (fraction + 0.1)	1✔
349	if ret then do	1✔
350	m <- SAT.getModel solver	1✔
351	let v = C.evalObjectiveFunction cxt m	1✔
352	let ub' = v - 1	1✔
353	C.logMessage cxt $ printf "Adaptive Search: updating upper bound: %d -> %d" ub ub'	×
354	C.addSolution cxt m	1✔
355	-- old upper bound constraints will be removed by backward subsumption removal
356	SAT.addClause solver [sel]	1✔
357	SAT.addPBAtMost solver obj ub'	1✔
358	loop fraction'	1✔
359	else do	1✔
360	-- deleting temporary constraint
361	SAT.addClause solver [-sel]	×
362	let lb' = mid + 1	1✔
363	C.logMessage cxt $ printf "Adaptive Search: updating lower bound: %d -> %d" lb lb'	×
364	C.addLowerBound cxt lb'	1✔
365	SAT.addPBAtLeast solver obj lb'	×
366	loop fraction'	1✔
367
368	tweakParams :: SAT.Solver -> SAT.PBLinSum -> IO ()
369	tweakParams solver obj = do	×
370	forM_ obj $ \(c,l) -> do	×
371	let p = if c > 0 then not (SAT.litPolarity l) else SAT.litPolarity l	×
372	SAT.setVarPolarity solver (SAT.litVar l) p	×
373	let cs = Set.fromList [abs c \| (c,_) <- obj]	×
374	ws = Map.fromAscList $ zip (Set.toAscList cs) [1..]	×
375	forM_ obj $ \(c,l) -> do	×
376	let w = ws Map.! abs c	×
377	replicateM w $ SAT.varBumpActivity solver (SAT.litVar l)	×

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