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

42.11

/src/ToySolver/SAT/PBO/BC.hs

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

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

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) (0, 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

    loop :: (SAT.LitSet, SAT.LitSet) -> (Integer, Integer) -> IO ()
    loop (unrelaxed, relaxed) (lb, ub)
      | lb > ub = C.setFinished cxt
      | otherwise = do
          let mid = (lb + ub) `div` 2
          C.logMessage cxt $ printf "BC: %d <= obj <= %d; guessing obj <= %d" lb ub mid
          sel <- SAT.newVar solver
          SAT.addPBAtMostSoft solver sel [(w, -lit)  | (lit, w) <- IntMap.toList (IntMap.restrictKeys weights relaxed)] mid
          ret <- SAT.solveWith solver (sel : 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 "BC: updating upper bound: %d -> %d" ub ub'
            C.addSolution cxt m
            SAT.addClause solver [sel]
            SAT.addPBAtMost solver obj ub'
            loop (unrelaxed, relaxed) (lb, ub')
          else do
            core <- SAT.getFailedAssumptions solver
            SAT.addClause solver [-sel] -- delete temporary constraint
            let core2 = core `IntSet.intersection` unrelaxed
            if IntSet.null core2 then do
              C.logMessage cxt $ printf "BC: updating lower bound: %d -> %d" lb (mid+1)
              C.addLowerBound cxt (mid+1)
              loop (unrelaxed, relaxed) (mid+1, ub)
            else do
              let unrelaxed' = unrelaxed `IntSet.difference` core2
                  relaxed'   = relaxed `IntSet.union` core2
              C.logMessage cxt $ printf "BC: #unrelaxed=%d, #relaxed=%d" (IntSet.size unrelaxed') (IntSet.size relaxed')
              loop (unrelaxed', relaxed') (lb, ub)

1	{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
2	-----------------------------------------------------------------------------
3	-- \|
4	-- Module : ToySolver.SAT.PBO.BC
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	-- Core-Guided binary search algorithm.
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	-----------------------------------------------------------------------------
22	module ToySolver.SAT.PBO.BC
23	( solve
24	) where
25
26	import Control.Concurrent.STM
27	import qualified Data.IntSet as IntSet
28	import qualified Data.IntMap as IntMap
29	import qualified ToySolver.SAT as SAT
30	import qualified ToySolver.SAT.Types as SAT
31	import qualified ToySolver.SAT.PBO.Context as C
32	import Text.Printf
33
34	solve :: C.Context cxt => cxt -> SAT.Solver -> IO ()
35	solve cxt solver = solveWBO (C.normalize cxt) solver	1✔
36
37	solveWBO :: C.Context cxt => cxt -> SAT.Solver -> IO ()
38	solveWBO cxt solver = do	1✔
39	SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }	1✔
40	ub <- atomically $ C.getSearchUpperBound cxt	1✔
41	loop (IntSet.fromList [lit \| (lit,_) <- sels], IntSet.empty) (0, ub)	1✔
42
43	where
44	obj :: SAT.PBLinSum
45	obj = C.getObjectiveFunction cxt	1✔
46
47	sels :: [(SAT.Lit, Integer)]
UNCOV 48	sels = [(-lit, w) \| (w,lit) <- obj]	×
49
50	weights :: SAT.LitMap Integer
51	weights = IntMap.fromList sels	1✔
52
53	loop :: (SAT.LitSet, SAT.LitSet) -> (Integer, Integer) -> IO ()
54	loop (unrelaxed, relaxed) (lb, ub)	1✔
55	\| lb > ub = C.setFinished cxt	1✔
56	\| otherwise = do	×
57	let mid = (lb + ub) `div` 2	1✔
58	C.logMessage cxt $ printf "BC: %d <= obj <= %d; guessing obj <= %d" lb ub mid	×
59	sel <- SAT.newVar solver	1✔
UNCOV 60	SAT.addPBAtMostSoft solver sel [(w, -lit) \| (lit, w) <- IntMap.toList (IntMap.restrictKeys weights relaxed)] mid	×
61	ret <- SAT.solveWith solver (sel : IntSet.toList unrelaxed)	1✔
UNCOV 62	if ret then do	×
UNCOV 63	m <- SAT.getModel solver	×
UNCOV 64	let val = C.evalObjectiveFunction cxt m	×
UNCOV 65	let ub' = val - 1	×
66	C.logMessage cxt $ printf "BC: updating upper bound: %d -> %d" ub ub'	×
UNCOV 67	C.addSolution cxt m	×
UNCOV 68	SAT.addClause solver [sel]	×
UNCOV 69	SAT.addPBAtMost solver obj ub'	×
UNCOV 70	loop (unrelaxed, relaxed) (lb, ub')	×
71	else do	1✔
72	core <- SAT.getFailedAssumptions solver	1✔
UNCOV 73	SAT.addClause solver [-sel] -- delete temporary constraint	×
UNCOV 74	let core2 = core `IntSet.intersection` unrelaxed	×
UNCOV 75	if IntSet.null core2 then do	×
76	C.logMessage cxt $ printf "BC: updating lower bound: %d -> %d" lb (mid+1)	×
77	C.addLowerBound cxt (mid+1)	1✔
78	loop (unrelaxed, relaxed) (mid+1, ub)	1✔
UNCOV 79	else do	×
UNCOV 80	let unrelaxed' = unrelaxed `IntSet.difference` core2	×
UNCOV 81	relaxed' = relaxed `IntSet.union` core2	×
82	C.logMessage cxt $ printf "BC: #unrelaxed=%d, #relaxed=%d" (IntSet.size unrelaxed') (IntSet.size relaxed')	×
UNCOV 83	loop (unrelaxed', relaxed') (lb, 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