{-# 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 -> IO ()
solve cxt
cxt Solver
solver = Normalized cxt -> Solver -> IO ()
forall cxt. Context cxt => cxt -> Solver -> IO ()
solveWBO (cxt -> Normalized cxt
forall a. Context a => a -> Normalized a
C.normalize cxt
cxt) Solver
solver

solveWBO :: C.Context cxt => cxt -> SAT.Solver -> IO ()
solveWBO :: cxt -> Solver -> IO ()
solveWBO cxt
cxt Solver
solver = do
  Solver -> (Config -> Config) -> IO ()
SAT.modifyConfig Solver
solver ((Config -> Config) -> IO ()) -> (Config -> Config) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Config
config -> Config
config{ configEnableBackwardSubsumptionRemoval :: Bool
SAT.configEnableBackwardSubsumptionRemoval = Bool
True }
  let sels0 :: [(Lit, Integer)]
sels0 = [(-Lit
v, Integer
c) | (Integer
c,Lit
v) <- cxt -> PBLinSum
forall a. Context a => a -> PBLinSum
C.getObjectiveFunction cxt
cxt]
  Integer -> LitMap Integer -> IO ()
loop Integer
0 ([(Lit, Integer)] -> LitMap Integer
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit, Integer)]
sels0)
  where
    loop :: Integer -> SAT.LitMap Integer -> IO ()
    loop :: Integer -> LitMap Integer -> IO ()
loop !Integer
lb LitMap Integer
sels = do
      cxt -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
C.addLowerBound cxt
cxt Integer
lb

      Bool
ret <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (LitMap Integer -> [Lit]
forall a. IntMap a -> [Lit]
IntMap.keys LitMap Integer
sels)
      if Bool
ret then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        -- モデルから余計な変数を除去する?
        cxt -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
C.addSolution cxt
cxt Model
m
        () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      else do
        LitSet
core <- Solver -> IO LitSet
SAT.getFailedAssumptions Solver
solver
        if LitSet -> Bool
IntSet.null LitSet
core then
          cxt -> IO ()
forall a. Context a => a -> IO ()
C.setFinished cxt
cxt
        else do
          let !min_c :: Integer
min_c = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [LitMap Integer
sels LitMap Integer -> Lit -> Integer
forall a. IntMap a -> Lit -> a
IntMap.! Lit
sel | Lit
sel <- LitSet -> [Lit]
IntSet.toList LitSet
core]
              !lb' :: Integer
lb' = Integer
lb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
min_c

          [(Lit, Lit)]
xs <- [Lit] -> (Lit -> IO (Lit, Lit)) -> IO [(Lit, Lit)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (LitSet -> [Lit]
IntSet.toList LitSet
core) ((Lit -> IO (Lit, Lit)) -> IO [(Lit, Lit)])
-> (Lit -> IO (Lit, Lit)) -> IO [(Lit, Lit)]
forall a b. (a -> b) -> a -> b
$ \Lit
sel -> do
            Lit
r <- Solver -> IO Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
            (Lit, Lit) -> IO (Lit, Lit)
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit
sel, Lit
r)
          Solver -> [Lit] -> Lit -> IO ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> [Lit] -> Lit -> m ()
SAT.addExactly Solver
solver (((Lit, Lit) -> Lit) -> [(Lit, Lit)] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map (Lit, Lit) -> Lit
forall a b. (a, b) -> b
snd [(Lit, Lit)]
xs) Lit
1
          Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
l | Lit
l <- LitSet -> [Lit]
IntSet.toList LitSet
core] -- optional constraint but sometimes useful

          LitMap Integer
ys <- ([LitMap Integer] -> LitMap Integer)
-> IO [LitMap Integer] -> IO (LitMap Integer)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [LitMap Integer] -> LitMap Integer
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IntMap.unions (IO [LitMap Integer] -> IO (LitMap Integer))
-> IO [LitMap Integer] -> IO (LitMap Integer)
forall a b. (a -> b) -> a -> b
$ [(Lit, Lit)]
-> ((Lit, Lit) -> IO (LitMap Integer)) -> IO [LitMap Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Lit, Lit)]
xs (((Lit, Lit) -> IO (LitMap Integer)) -> IO [LitMap Integer])
-> ((Lit, Lit) -> IO (LitMap Integer)) -> IO [LitMap Integer]
forall a b. (a -> b) -> a -> b
$ \(Lit
sel, Lit
r) -> do
            Lit
sel' <- Solver -> IO Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
            Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
sel', Lit
r, Lit
sel]
            let c :: Integer
c = LitMap Integer
sels LitMap Integer -> Lit -> Integer
forall a. IntMap a -> Lit -> a
IntMap.! Lit
sel
            if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
min_c
              then LitMap Integer -> IO (LitMap Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (LitMap Integer -> IO (LitMap Integer))
-> LitMap Integer -> IO (LitMap Integer)
forall a b. (a -> b) -> a -> b
$ [(Lit, Integer)] -> LitMap Integer
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit
sel', Integer
min_c), (Lit
sel, Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
min_c)]
              else LitMap Integer -> IO (LitMap Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (LitMap Integer -> IO (LitMap Integer))
-> LitMap Integer -> IO (LitMap Integer)
forall a b. (a -> b) -> a -> b
$ Lit -> Integer -> LitMap Integer
forall a. Lit -> a -> IntMap a
IntMap.singleton Lit
sel' Integer
min_c
          let sels' :: LitMap Integer
sels' = LitMap Integer -> LitMap Integer -> LitMap Integer
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union LitMap Integer
ys (LitMap Integer -> IntMap () -> LitMap Integer
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference LitMap Integer
sels ((Lit -> ()) -> LitSet -> IntMap ()
forall a. (Lit -> a) -> LitSet -> IntMap a
IntMap.fromSet (() -> Lit -> ()
forall a b. a -> b -> a
const ()) LitSet
core))

          Integer -> LitMap Integer -> IO ()
loop Integer
lb' LitMap Integer
sels'