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

39.39

/src/ToySolver/SAT/PBO/UnsatBased.hs

{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.UnsatBased
-- Copyright   :  (c) Masahiro Sakai 2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Reference:
--
-- * Vasco Manquinho Ruben Martins Inês Lynce
--   Improving Unsatisfiability-based Algorithms for Boolean Optimization.
--   Theory and Applications of Satisfiability Testing – SAT 2010, pp 181-193.
--   <https://doi.org/10.1007/978-3-642-14186-7_16>
--   <http://sat.inesc-id.pt/~ruben/papers/manquinho-sat10.pdf>
--   <http://sat.inesc-id.pt/~ruben/talks/sat10-talk.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.PBO.UnsatBased
  ( solve
  ) where

import Control.Monad
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.PBO.Context as C

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 }
  let sels0 = [(-v, c) | (c,v) <- C.getObjectiveFunction cxt]
  loop 0 (IntMap.fromList sels0)
  where
    loop :: Integer -> SAT.LitMap Integer -> IO ()
    loop !lb sels = do
      C.addLowerBound cxt lb

      ret <- SAT.solveWith solver (IntMap.keys sels)
      if ret then do
        m <- SAT.getModel solver
        -- モデルから余計な変数を除去する?
        C.addSolution cxt m
        return ()
      else do
        core <- SAT.getFailedAssumptions solver
        if IntSet.null core then
          C.setFinished cxt
        else do
          let !min_c = minimum $ IntMap.elems $ IntMap.restrictKeys sels core
              !lb' = lb + min_c

          xs <- forM (IntSet.toList core) $ \sel -> do
            r <- SAT.newVar solver
            return (sel, r)
          SAT.addExactly solver (map snd xs) 1
          SAT.addClause solver [-l | l <- IntSet.toList core] -- optional constraint but sometimes useful

          ys <- liftM IntMap.unions $ forM xs $ \(sel, r) -> do
            sel' <- SAT.newVar solver
            SAT.addClause solver [-sel', r, sel]
            let c = sels IntMap.! sel
            if c > min_c
              then return $ IntMap.fromList [(sel', min_c), (sel, c - min_c)]
              else return $ IntMap.singleton sel' min_c
          let sels' = IntMap.union ys (IntMap.withoutKeys sels core)

          loop lb' sels'

1	{-# LANGUAGE BangPatterns #-}
2	{-# OPTIONS_GHC -Wall #-}
3	{-# OPTIONS_HADDOCK show-extensions #-}
4	-----------------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.SAT.PBO.UnsatBased
7	-- Copyright : (c) Masahiro Sakai 2013
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : provisional
12	-- Portability : non-portable
13	--
14	-- Reference:
15	--
16	-- * Vasco Manquinho Ruben Martins Inês Lynce
17	-- Improving Unsatisfiability-based Algorithms for Boolean Optimization.
18	-- Theory and Applications of Satisfiability Testing – SAT 2010, pp 181-193.
19	-- <https://doi.org/10.1007/978-3-642-14186-7_16>
20	-- <http://sat.inesc-id.pt/~ruben/papers/manquinho-sat10.pdf>
21	-- <http://sat.inesc-id.pt/~ruben/talks/sat10-talk.pdf>
22	--
23	-----------------------------------------------------------------------------
24	module ToySolver.SAT.PBO.UnsatBased
25	( solve
26	) where
27
28	import Control.Monad
29	import qualified Data.IntMap as IntMap
30	import qualified Data.IntSet as IntSet
31	import qualified ToySolver.SAT as SAT
32	import qualified ToySolver.SAT.Types as SAT
33	import qualified ToySolver.SAT.PBO.Context as C
34
35	solve :: C.Context cxt => cxt -> SAT.Solver -> IO ()
36	solve cxt solver = solveWBO (C.normalize cxt) solver	1✔
37
38	solveWBO :: C.Context cxt => cxt -> SAT.Solver -> IO ()
39	solveWBO cxt solver = do	1✔
40	SAT.modifyConfig solver $ \config -> config{ SAT.configEnableBackwardSubsumptionRemoval = True }	1✔
UNCOV 41	let sels0 = [(-v, c) \| (c,v) <- C.getObjectiveFunction cxt]	×
42	loop 0 (IntMap.fromList sels0)	1✔
43	where
44	loop :: Integer -> SAT.LitMap Integer -> IO ()
45	loop !lb sels = do	1✔
46	C.addLowerBound cxt lb	1✔
47
48	ret <- SAT.solveWith solver (IntMap.keys sels)	1✔
49	if ret then do	1✔
50	m <- SAT.getModel solver	1✔
51	-- モデルから余計な変数を除去する?
52	C.addSolution cxt m	1✔
53	return ()	×
54	else do	1✔
55	core <- SAT.getFailedAssumptions solver	1✔
UNCOV 56	if IntSet.null core then	×
57	C.setFinished cxt	1✔
UNCOV 58	else do	×
UNCOV 59	let !min_c = minimum $ IntMap.elems $ IntMap.restrictKeys sels core	×
UNCOV 60	!lb' = lb + min_c	×
61
UNCOV 62	xs <- forM (IntSet.toList core) $ \sel -> do	×
UNCOV 63	r <- SAT.newVar solver	×
UNCOV 64	return (sel, r)	×
UNCOV 65	SAT.addExactly solver (map snd xs) 1	×
UNCOV 66	SAT.addClause solver [-l \| l <- IntSet.toList core] -- optional constraint but sometimes useful	×
67
UNCOV 68	ys <- liftM IntMap.unions $ forM xs $ \(sel, r) -> do	×
UNCOV 69	sel' <- SAT.newVar solver	×
70	SAT.addClause solver [-sel', r, sel]	×
UNCOV 71	let c = sels IntMap.! sel	×
72	if c > min_c	×
73	then return $ IntMap.fromList [(sel', min_c), (sel, c - min_c)]	×
74	else return $ IntMap.singleton sel' min_c	×
UNCOV 75	let sels' = IntMap.union ys (IntMap.withoutKeys sels core)	×
76
UNCOV 77	loop lb' sels'	×

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