msakai / toysolver / 513

Committed 24 Nov 2024 08:49AM UTC coverage: 68.675% (-1.0%) from 69.681%

Build # 513

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 496ed4263 into 46e1509c4

Run Details

5 of 121 new or added lines in 7 files covered. (4.13%)

105 existing lines in 14 files now uncovered.

9745 of 14190 relevant lines covered (68.68%)

0.69 hits per line

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

25.76

/src/ToySolver/SAT/PBO/BCD.hs

{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.BCD
-- Copyright   :  (c) Masahiro Sakai 2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  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.BCD
  ( solve
  ) where

import Control.Concurrent.STM
import Control.Monad
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Data.List
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO.Context as C
import Text.Printf

data CoreInfo
  = CoreInfo
  { coreLits :: SAT.LitSet
  , coreLB   :: !Integer
  , coreUB   :: !Integer
  }

coreMidValue :: CoreInfo -> Integer
coreMidValue c = (coreLB c + coreUB c) `div` 2

coreUnion :: CoreInfo -> CoreInfo -> CoreInfo
coreUnion c1 c2
  = CoreInfo
  { coreLits = IntSet.union (coreLits c1) (coreLits c2)
  , coreLB = coreLB c1 + coreLB c2
  , coreUB = coreUB c1 + coreUB c2
  }

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

solveWBO :: C.Context cxt => cxt -> SAT.Solver -> IO ()
solveWBO cxt solver = do
  SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }
  ub <- atomically $ C.getSearchUpperBound cxt
  loop (IntSet.fromList [lit | (lit,_) <- sels], IntSet.empty) [] ub

  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

    coreNew :: SAT.LitSet -> CoreInfo
    coreNew cs = CoreInfo{ coreLits = cs, coreLB = 0, coreUB = sum [weights IntMap.! lit | lit <- IntSet.toList cs] }

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

    loop :: (SAT.LitSet, SAT.LitSet) -> [CoreInfo] -> Integer -> IO ()
    loop (unrelaxed, relaxed) cores ub = do
      let lb = sum [coreLB info | info <- cores]
      C.logMessage cxt $ printf "BCD: %d <= obj <= %d" lb ub
      C.logMessage cxt $ printf "BCD: #cores=%d, #unrelaxed=%d, #relaxed=%d"
        (length cores) (IntSet.size unrelaxed) (IntSet.size relaxed)

      sels <- liftM IntMap.fromList $ forM cores $ \info -> do
        sel <- SAT.newVar solver
        SAT.addPBAtMostSoft solver sel (coreCostFun info) (coreMidValue info)
        return (sel, info)

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

      if ret then do
        m <- SAT.getModel solver
        let val = C.evalObjectiveFunction cxt m
        let ub' = val - 1
        C.logMessage cxt $ printf "BCD: updating upper bound: %d -> %d" ub ub'
        C.addSolution cxt m
        SAT.addPBAtMost solver obj ub'
        let cores' = map (\info -> info{ coreUB = SAT.evalPBLinSum m (coreCostFun info) }) cores
        cont (unrelaxed, relaxed) cores' ub'
      else do
        core <- SAT.getFailedAssumptions solver
        case IntSet.toList core of
          [] -> return ()
          [sel] | Just info <- IntMap.lookup sel sels -> do
            let info'  = info{ coreLB = coreMidValue info + 1 }
                cores' = IntMap.elems $ IntMap.insert sel info' sels
            C.logMessage cxt $ printf "BCD: updating lower bound of a core"
            SAT.addPBAtLeast solver (coreCostFun info') (coreLB info') -- redundant, but useful for direct search
            cont (unrelaxed, relaxed) cores' ub
          _ -> do
            let torelax     = unrelaxed `IntSet.intersection` core
                intersected = IntMap.elems $ IntMap.restrictKeys sels core
                rest        = IntMap.elems $ IntMap.withoutKeys sels core
                mergedCore  = foldl' coreUnion (coreNew torelax) intersected
                unrelaxed'  = unrelaxed `IntSet.difference` torelax
                relaxed'    = relaxed `IntSet.union` torelax
                cores'      = mergedCore : rest
            if null intersected then do
              C.logMessage cxt $ printf "BCD: found a new core of size %d" (IntSet.size torelax)
            else do
              C.logMessage cxt $ printf "BCD: merging cores"
            SAT.addPBAtLeast solver (coreCostFun mergedCore) (coreLB mergedCore) -- redundant, but useful for direct search
            forM_ (IntMap.keys sels) $ \sel -> SAT.addClause solver [-sel] -- delete temporary constraints
            cont (unrelaxed', relaxed') cores' ub

    cont :: (SAT.LitSet, SAT.LitSet) -> [CoreInfo] -> Integer -> IO ()
    cont (unrelaxed, relaxed) cores ub
      | all (\info -> coreLB info > coreUB info) cores = C.setFinished cxt
      | otherwise = loop (unrelaxed, relaxed) cores ub

1	{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
2	-----------------------------------------------------------------------------
3	-- \|
4	-- Module : ToySolver.SAT.PBO.BCD
5	-- Copyright : (c) Masahiro Sakai 2014
6	-- License : BSD-style
7	--
8	-- Maintainer : masahiro.sakai@gmail.com
9	-- Stability : provisional
10	-- Portability : portable
11	--
12	-- Reference:
13	--
14	-- * Federico Heras, Antonio Morgado, João Marques-Silva,
15	-- Core-Guided binary search algorithms for maximum satisfiability,
16	-- Twenty-Fifth AAAI Conference on Artificial Intelligence, 2011.
17	-- <http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3713>
18	--
19	-- * A. Morgado, F. Heras, and J. Marques-Silva,
20	-- Improvements to Core-Guided binary search for MaxSAT,
21	-- in Theory and Applications of Satisfiability Testing (SAT 2012),
22	-- pp. 284-297.
23	-- <https://doi.org/10.1007/978-3-642-31612-8_22>
24	-- <http://ulir.ul.ie/handle/10344/2771>
25	--
26	-----------------------------------------------------------------------------
27	module ToySolver.SAT.PBO.BCD
28	( solve
29	) where
30
31	import Control.Concurrent.STM
32	import Control.Monad
33	import qualified Data.IntSet as IntSet
34	import qualified Data.IntMap as IntMap
35	import Data.List
36	import qualified ToySolver.SAT as SAT
37	import qualified ToySolver.SAT.Types as SAT
38	import qualified ToySolver.SAT.PBO.Context as C
39	import Text.Printf
40
41	data CoreInfo
42	= CoreInfo
UNCOV 43	{ coreLits :: SAT.LitSet	×
UNCOV 44	, coreLB :: !Integer	×
UNCOV 45	, coreUB :: !Integer	×
46	}
47
48	coreMidValue :: CoreInfo -> Integer
UNCOV 49	coreMidValue c = (coreLB c + coreUB c) `div` 2	×
50
51	coreUnion :: CoreInfo -> CoreInfo -> CoreInfo
52	coreUnion c1 c2	×
53	= CoreInfo	×
54	{ coreLits = IntSet.union (coreLits c1) (coreLits c2)	×
55	, coreLB = coreLB c1 + coreLB c2	×
56	, coreUB = coreUB c1 + coreUB c2	×
57	}
58
59	solve :: C.Context cxt => cxt -> SAT.Solver -> IO ()
60	solve cxt solver = solveWBO (C.normalize cxt) solver	1✔
61
62	solveWBO :: C.Context cxt => cxt -> SAT.Solver -> IO ()
63	solveWBO cxt solver = do	1✔
64	SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }	1✔
65	ub <- atomically $ C.getSearchUpperBound cxt	1✔
66	loop (IntSet.fromList [lit \| (lit,_) <- sels], IntSet.empty) [] ub	×
67
68	where
69	obj :: SAT.PBLinSum
70	obj = C.getObjectiveFunction cxt	1✔
71
72	sels :: [(SAT.Lit, Integer)]
UNCOV 73	sels = [(-lit, w) \| (w,lit) <- obj]	×
74
75	weights :: SAT.LitMap Integer
UNCOV 76	weights = IntMap.fromList sels	×
77
78	coreNew :: SAT.LitSet -> CoreInfo
UNCOV 79	coreNew cs = CoreInfo{ coreLits = cs, coreLB = 0, coreUB = sum [weights IntMap.! lit \| lit <- IntSet.toList cs] }	×
80
81	coreCostFun :: CoreInfo -> SAT.PBLinSum
UNCOV 82	coreCostFun c = [(w, -lit) \| (lit, w) <- IntMap.toList (IntMap.restrictKeys weights (coreLits c))]	×
83
84	loop :: (SAT.LitSet, SAT.LitSet) -> [CoreInfo] -> Integer -> IO ()
85	loop (unrelaxed, relaxed) cores ub = do	1✔
86	let lb = sum [coreLB info \| info <- cores]	×
87	C.logMessage cxt $ printf "BCD: %d <= obj <= %d" lb ub	×
88	C.logMessage cxt $ printf "BCD: #cores=%d, #unrelaxed=%d, #relaxed=%d"	×
89	(length cores) (IntSet.size unrelaxed) (IntSet.size relaxed)	×
90
UNCOV 91	sels <- liftM IntMap.fromList $ forM cores $ \info -> do	×
UNCOV 92	sel <- SAT.newVar solver	×
UNCOV 93	SAT.addPBAtMostSoft solver sel (coreCostFun info) (coreMidValue info)	×
UNCOV 94	return (sel, info)	×
95
96	ret <- SAT.solveWith solver (IntMap.keys sels ++ IntSet.toList unrelaxed)	1✔
97
98	if ret then do	1✔
99	m <- SAT.getModel solver	1✔
100	let val = C.evalObjectiveFunction cxt m	1✔
101	let ub' = val - 1	1✔
102	C.logMessage cxt $ printf "BCD: updating upper bound: %d -> %d" ub ub'	×
103	C.addSolution cxt m	1✔
104	SAT.addPBAtMost solver obj ub'	1✔
UNCOV 105	let cores' = map (\info -> info{ coreUB = SAT.evalPBLinSum m (coreCostFun info) }) cores	×
106	cont (unrelaxed, relaxed) cores' ub'	×
107	else do	1✔
108	core <- SAT.getFailedAssumptions solver	1✔
109	case IntSet.toList core of	1✔
110	[] -> return ()	×
UNCOV 111	[sel] \| Just info <- IntMap.lookup sel sels -> do	×
UNCOV 112	let info' = info{ coreLB = coreMidValue info + 1 }	×
UNCOV 113	cores' = IntMap.elems $ IntMap.insert sel info' sels	×
114	C.logMessage cxt $ printf "BCD: updating lower bound of a core"	×
UNCOV 115	SAT.addPBAtLeast solver (coreCostFun info') (coreLB info') -- redundant, but useful for direct search	×
116	cont (unrelaxed, relaxed) cores' ub	×
UNCOV 117	_ -> do	×
UNCOV 118	let torelax = unrelaxed `IntSet.intersection` core	×
UNCOV 119	intersected = IntMap.elems $ IntMap.restrictKeys sels core	×
UNCOV 120	rest = IntMap.elems $ IntMap.withoutKeys sels core	×
121	mergedCore = foldl' coreUnion (coreNew torelax) intersected	×
UNCOV 122	unrelaxed' = unrelaxed `IntSet.difference` torelax	×
123	relaxed' = relaxed `IntSet.union` torelax	×
UNCOV 124	cores' = mergedCore : rest	×
125	if null intersected then do	×
126	C.logMessage cxt $ printf "BCD: found a new core of size %d" (IntSet.size torelax)	×
127	else do	×
128	C.logMessage cxt $ printf "BCD: merging cores"	×
UNCOV 129	SAT.addPBAtLeast solver (coreCostFun mergedCore) (coreLB mergedCore) -- redundant, but useful for direct search	×
UNCOV 130	forM_ (IntMap.keys sels) $ \sel -> SAT.addClause solver [-sel] -- delete temporary constraints	×
131	cont (unrelaxed', relaxed') cores' ub	×
132
133	cont :: (SAT.LitSet, SAT.LitSet) -> [CoreInfo] -> Integer -> IO ()
134	cont (unrelaxed, relaxed) cores ub	1✔
UNCOV 135	\| all (\info -> coreLB info > coreUB info) cores = C.setFinished cxt	×
136	\| otherwise = loop (unrelaxed, relaxed) cores ub	×

msakai / toysolver / 513

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