msakai / toysolver / 797

Committed 09 May 2026 11:18AM UTC coverage: 71.463% (-0.4%) from 71.864%

Build # 797

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 2564c0a1a into 36153c78c

Coverage Stats

11046 of 15457 relevant lines covered (71.46%)

0.71 hits per line

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

60.61

/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 (foldl')
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 (foldl')
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
43	{ coreLits :: SAT.LitSet	1✔
44	, coreLB :: !Integer	1✔
45	, coreUB :: !Integer	1✔
46	}
47
48	coreMidValue :: CoreInfo -> Integer
49	coreMidValue c = (coreLB c + coreUB c) `div` 2	1✔
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)]
73	sels = [(-lit, w) \| (w,lit) <- obj]	1✔
74
75	weights :: SAT.LitMap Integer
76	weights = IntMap.fromList sels	1✔
77
78	coreNew :: SAT.LitSet -> CoreInfo
79	coreNew cs = CoreInfo{ coreLits = cs, coreLB = 0, coreUB = sum [weights IntMap.! lit \| lit <- IntSet.toList cs] }	1✔
80
81	coreCostFun :: CoreInfo -> SAT.PBLinSum
82	coreCostFun c = [(w, -lit) \| (lit, w) <- IntMap.toList (IntMap.restrictKeys weights (coreLits c))]	1✔
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
91	sels <- liftM IntMap.fromList $ forM cores $ \info -> do	1✔
92	sel <- SAT.newVar solver	1✔
93	SAT.addPBAtMostSoft solver sel (coreCostFun info) (coreMidValue info)	1✔
94	return (sel, info)	1✔
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✔
105	let cores' = map (\info -> info{ coreUB = SAT.evalPBLinSum m (coreCostFun info) }) cores	1✔
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 ()	×
111	[sel] \| Just info <- IntMap.lookup sel sels -> do	1✔
112	let info' = info{ coreLB = coreMidValue info + 1 }	1✔
113	cores' = IntMap.elems $ IntMap.insert sel info' sels	1✔
114	C.logMessage cxt $ printf "BCD: updating lower bound of a core"	×
115	SAT.addPBAtLeast solver (coreCostFun info') (coreLB info') -- redundant, but useful for direct search	1✔
116	cont (unrelaxed, relaxed) cores' ub	×
117	_ -> do	1✔
118	let torelax = unrelaxed `IntSet.intersection` core	1✔
119	intersected = IntMap.elems $ IntMap.restrictKeys sels core	×
120	rest = IntMap.elems $ IntMap.withoutKeys sels core	×
121	mergedCore = foldl' coreUnion (coreNew torelax) intersected	×
122	unrelaxed' = unrelaxed `IntSet.difference` torelax	1✔
123	relaxed' = relaxed `IntSet.union` torelax	×
124	cores' = mergedCore : rest	1✔
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"	×
129	SAT.addPBAtLeast solver (coreCostFun mergedCore) (coreLB mergedCore) -- redundant, but useful for direct search	1✔
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✔
135	\| all (\info -> coreLB info > coreUB info) cores = C.setFinished cxt	1✔
136	\| otherwise = loop (unrelaxed, relaxed) cores ub	×

msakai / toysolver / 797

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