{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.PB2IP
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.PB2IP
  ( pb2ip
  , PB2IPInfo
  , wbo2ip
  , WBO2IPInfo

  , sat2ip
  , SAT2IPInfo
  , maxsat2ip
  , MaxSAT2IPInfo
  ) where

import Data.Array.IArray
import Data.Default.Class
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map

import qualified Data.PseudoBoolean as PBFile
import qualified Numeric.Optimization.MIP as MIP
import Numeric.Optimization.MIP ((.==.), (.<=.), (.>=.))

import ToySolver.Converter.Base
import ToySolver.Converter.PB
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

-- -----------------------------------------------------------------------------

newtype PB2IPInfo = PB2IPInfo Int
  deriving (PB2IPInfo -> PB2IPInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PB2IPInfo -> PB2IPInfo -> Bool
$c/= :: PB2IPInfo -> PB2IPInfo -> Bool
== :: PB2IPInfo -> PB2IPInfo -> Bool
$c== :: PB2IPInfo -> PB2IPInfo -> Bool
Eq, Var -> PB2IPInfo -> ShowS
[PB2IPInfo] -> ShowS
PB2IPInfo -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PB2IPInfo] -> ShowS
$cshowList :: [PB2IPInfo] -> ShowS
show :: PB2IPInfo -> String
$cshow :: PB2IPInfo -> String
showsPrec :: Var -> PB2IPInfo -> ShowS
$cshowsPrec :: Var -> PB2IPInfo -> ShowS
Show, ReadPrec [PB2IPInfo]
ReadPrec PB2IPInfo
Var -> ReadS PB2IPInfo
ReadS [PB2IPInfo]
forall a.
(Var -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [PB2IPInfo]
$creadListPrec :: ReadPrec [PB2IPInfo]
readPrec :: ReadPrec PB2IPInfo
$creadPrec :: ReadPrec PB2IPInfo
readList :: ReadS [PB2IPInfo]
$creadList :: ReadS [PB2IPInfo]
readsPrec :: Var -> ReadS PB2IPInfo
$creadsPrec :: Var -> ReadS PB2IPInfo
Read)

instance Transformer PB2IPInfo where
  type Source PB2IPInfo = SAT.Model
  type Target PB2IPInfo = Map MIP.Var Rational

instance ForwardTransformer PB2IPInfo where
  transformForward :: PB2IPInfo -> Source PB2IPInfo -> Target PB2IPInfo
transformForward PB2IPInfo
_ Source PB2IPInfo
m =
    forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var -> Var
convVar Var
v, if Bool
val then Rational
1 else Rational
0) | (Var
v,Bool
val) <- forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source PB2IPInfo
m]

instance BackwardTransformer PB2IPInfo where
  transformBackward :: PB2IPInfo -> Target PB2IPInfo -> Source PB2IPInfo
transformBackward (PB2IPInfo Var
nv) = Var -> Map Var Rational -> Model
mtrans Var
nv

pb2ip :: PBFile.Formula -> (MIP.Problem Integer, PB2IPInfo)
pb2ip :: Formula -> (Problem Integer, PB2IPInfo)
pb2ip Formula
formula = (Problem Integer
mip, Var -> PB2IPInfo
PB2IPInfo (Formula -> Var
PBFile.pbNumVars Formula
formula))
  where
    mip :: Problem Integer
mip = forall a. Default a => a
def
      { objectiveFunction :: ObjectiveFunction Integer
MIP.objectiveFunction = ObjectiveFunction Integer
obj2
      , constraints :: [Constraint Integer]
MIP.constraints = [Constraint Integer]
cs2
      , varType :: Map Var VarType
MIP.varType = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, VarType
MIP.IntegerVariable) | Var
v <- [Var]
vs]
      , varBounds :: Map Var (Bounds Integer)
MIP.varBounds = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, (BoundExpr Integer
0,BoundExpr Integer
1)) | Var
v <- [Var]
vs]
      }

    vs :: [Var]
vs = [Var -> Var
convVar Var
v | Var
v <- [Var
1..Formula -> Var
PBFile.pbNumVars Formula
formula]]

    obj2 :: ObjectiveFunction Integer
obj2 =
      case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
        Just Sum
obj' -> forall a. Default a => a
def{ objDir :: OptDir
MIP.objDir = OptDir
MIP.OptMin, objExpr :: Expr Integer
MIP.objExpr = Sum -> Expr Integer
convExpr Sum
obj' }
        Maybe Sum
Nothing   -> forall a. Default a => a
def{ objDir :: OptDir
MIP.objDir = OptDir
MIP.OptMin, objExpr :: Expr Integer
MIP.objExpr = Expr Integer
0 }

    cs2 :: [Constraint Integer]
cs2 = do
      (Sum
lhs,Op
op,Integer
rhs) <- Formula -> [(Sum, Op, Integer)]
PBFile.pbConstraints Formula
formula
      let (Expr Integer
lhs2,Integer
c) = Expr Integer -> (Expr Integer, Integer)
splitConst forall a b. (a -> b) -> a -> b
$ Sum -> Expr Integer
convExpr Sum
lhs
          rhs2 :: Integer
rhs2 = Integer
rhs forall a. Num a => a -> a -> a
- Integer
c
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Op
op of
        Op
PBFile.Ge -> forall a. Default a => a
def{ constrExpr :: Expr Integer
MIP.constrExpr = Expr Integer
lhs2, constrLB :: BoundExpr Integer
MIP.constrLB = forall r. r -> Extended r
MIP.Finite Integer
rhs2 }
        Op
PBFile.Eq -> forall a. Default a => a
def{ constrExpr :: Expr Integer
MIP.constrExpr = Expr Integer
lhs2, constrLB :: BoundExpr Integer
MIP.constrLB = forall r. r -> Extended r
MIP.Finite Integer
rhs2, constrUB :: BoundExpr Integer
MIP.constrUB = forall r. r -> Extended r
MIP.Finite Integer
rhs2 }


convExpr :: PBFile.Sum -> MIP.Expr Integer
convExpr :: Sum -> Expr Integer
convExpr Sum
s = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
w forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Var -> Expr Integer
f Term
tm) | (Integer
w,Term
tm) <- Sum
s]
  where
    f :: PBFile.Lit -> MIP.Expr Integer
    f :: Var -> Expr Integer
f Var
x
      | Var
x forall a. Ord a => a -> a -> Bool
> Var
0     = forall c. Num c => Var -> Expr c
MIP.varExpr (Var -> Var
convVar Var
x)
      | Bool
otherwise = Expr Integer
1 forall a. Num a => a -> a -> a
- forall c. Num c => Var -> Expr c
MIP.varExpr (Var -> Var
convVar (forall a. Num a => a -> a
abs Var
x))

convVar :: PBFile.Var -> MIP.Var
convVar :: Var -> Var
convVar Var
x = String -> Var
MIP.toVar (String
"x" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var
x)

-- -----------------------------------------------------------------------------

data WBO2IPInfo = WBO2IPInfo !Int [(MIP.Var, PBFile.SoftConstraint)]
  deriving (WBO2IPInfo -> WBO2IPInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WBO2IPInfo -> WBO2IPInfo -> Bool
$c/= :: WBO2IPInfo -> WBO2IPInfo -> Bool
== :: WBO2IPInfo -> WBO2IPInfo -> Bool
$c== :: WBO2IPInfo -> WBO2IPInfo -> Bool
Eq, Var -> WBO2IPInfo -> ShowS
[WBO2IPInfo] -> ShowS
WBO2IPInfo -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WBO2IPInfo] -> ShowS
$cshowList :: [WBO2IPInfo] -> ShowS
show :: WBO2IPInfo -> String
$cshow :: WBO2IPInfo -> String
showsPrec :: Var -> WBO2IPInfo -> ShowS
$cshowsPrec :: Var -> WBO2IPInfo -> ShowS
Show)

instance Transformer WBO2IPInfo where
  type Source WBO2IPInfo = SAT.Model
  type Target WBO2IPInfo = Map MIP.Var Rational

instance ForwardTransformer WBO2IPInfo where
  transformForward :: WBO2IPInfo -> Source WBO2IPInfo -> Target WBO2IPInfo
transformForward (WBO2IPInfo Var
_nv [(Var, SoftConstraint)]
relaxVariables) Source WBO2IPInfo
m = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Var Rational
m1 Map Var Rational
m2
      where
        m1 :: Map Var Rational
m1 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [(Var -> Var
convVar Var
v, if Bool
val then Rational
1 else Rational
0) | (Var
v,Bool
val) <- forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source WBO2IPInfo
m]
        m2 :: Map Var Rational
m2 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [(Var
v, if forall m. IModel m => m -> (Sum, Op, Integer) -> Bool
SAT.evalPBConstraint Source WBO2IPInfo
m (Sum, Op, Integer)
c then Rational
0 else Rational
1) | (Var
v, (Just Integer
_, (Sum, Op, Integer)
c)) <- [(Var, SoftConstraint)]
relaxVariables]

instance BackwardTransformer WBO2IPInfo where
  transformBackward :: WBO2IPInfo -> Target WBO2IPInfo -> Source WBO2IPInfo
transformBackward (WBO2IPInfo Var
nv [(Var, SoftConstraint)]
_relaxVariables) = Var -> Map Var Rational -> Model
mtrans Var
nv

wbo2ip :: Bool -> PBFile.SoftFormula -> (MIP.Problem Integer, WBO2IPInfo)
wbo2ip :: Bool -> SoftFormula -> (Problem Integer, WBO2IPInfo)
wbo2ip Bool
useIndicator SoftFormula
formula = (Problem Integer
mip, Var -> [(Var, SoftConstraint)] -> WBO2IPInfo
WBO2IPInfo (SoftFormula -> Var
PBFile.wboNumVars SoftFormula
formula) [(Var, SoftConstraint)]
relaxVariables)
  where
    mip :: Problem Integer
mip = forall a. Default a => a
def
      { objectiveFunction :: ObjectiveFunction Integer
MIP.objectiveFunction = ObjectiveFunction Integer
obj2
      , constraints :: [Constraint Integer]
MIP.constraints = [Constraint Integer]
topConstr forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [([(Integer, Var)], Constraint Integer)]
cs2
      , varType :: Map Var VarType
MIP.varType = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, VarType
MIP.IntegerVariable) | Var
v <- [Var]
vs]
      , varBounds :: Map Var (Bounds Integer)
MIP.varBounds = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, (BoundExpr Integer
0,BoundExpr Integer
1)) | Var
v <- [Var]
vs]
      }

    vs :: [Var]
vs = [Var -> Var
convVar Var
v | Var
v <- [Var
1..SoftFormula -> Var
PBFile.wboNumVars SoftFormula
formula]] forall a. [a] -> [a] -> [a]
++ [Var
v | ([(Integer, Var)]
ts, Constraint Integer
_) <- [([(Integer, Var)], Constraint Integer)]
cs2, (Integer
_, Var
v) <- [(Integer, Var)]
ts]

    obj2 :: ObjectiveFunction Integer
obj2 = forall a. Default a => a
def
      { objDir :: OptDir
MIP.objDir = OptDir
MIP.OptMin
      , objExpr :: Expr Integer
MIP.objExpr = forall c. [Term c] -> Expr c
MIP.Expr [forall c. c -> [Var] -> Term c
MIP.Term Integer
w [Var
v] | ([(Integer, Var)]
ts, Constraint Integer
_) <- [([(Integer, Var)], Constraint Integer)]
cs2, (Integer
w, Var
v) <- [(Integer, Var)]
ts]
      }

    topConstr :: [MIP.Constraint Integer]
    topConstr :: [Constraint Integer]
topConstr =
     case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula of
       Maybe Integer
Nothing -> []
       Just Integer
t ->
          [ forall a. Default a => a
def{ constrExpr :: Expr Integer
MIP.constrExpr = forall c. ObjectiveFunction c -> Expr c
MIP.objExpr ObjectiveFunction Integer
obj2, constrUB :: BoundExpr Integer
MIP.constrUB = forall r. r -> Extended r
MIP.Finite (forall a. Num a => Integer -> a
fromInteger Integer
t forall a. Num a => a -> a -> a
- Integer
1) } ]

    relaxVariables :: [(MIP.Var, PBFile.SoftConstraint)]
    relaxVariables :: [(Var, SoftConstraint)]
relaxVariables = [(String -> Var
MIP.toVar (String
"r" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var
n), SoftConstraint
c) | (Var
n, SoftConstraint
c) <- forall a b. [a] -> [b] -> [(a, b)]
zip [(Var
0::Int)..] (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula)]

    cs2 :: [([(Integer, MIP.Var)], MIP.Constraint Integer)]
    cs2 :: [([(Integer, Var)], Constraint Integer)]
cs2 = do
      (Var
v, (Maybe Integer
w, (Sum
lhs,Op
op,Integer
rhs))) <- [(Var, SoftConstraint)]
relaxVariables
      let (Expr Integer
lhs2,Integer
c) = Expr Integer -> (Expr Integer, Integer)
splitConst forall a b. (a -> b) -> a -> b
$ Sum -> Expr Integer
convExpr Sum
lhs
          rhs2 :: Integer
rhs2 = Integer
rhs forall a. Num a => a -> a -> a
- Integer
c
          ([(Integer, Var)]
ts,Maybe (Var, Integer)
ind) =
            case Maybe Integer
w of
              Maybe Integer
Nothing -> ([], forall a. Maybe a
Nothing)
              Just Integer
w2 -> ([(Integer
w2,Var
v)], forall a. a -> Maybe a
Just (Var
v,Integer
0))
      if forall a. Maybe a -> Bool
isNothing Maybe Integer
w Bool -> Bool -> Bool
|| Bool
useIndicator then do
         let c :: Constraint Integer
c =
               case Op
op of
                 Op
PBFile.Ge -> (Expr Integer
lhs2 forall c. Num c => Expr c -> Expr c -> Constraint c
.>=. forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhs2) { constrIndicator :: Maybe (Var, Integer)
MIP.constrIndicator = Maybe (Var, Integer)
ind }
                 Op
PBFile.Eq -> (Expr Integer
lhs2 forall c. Num c => Expr c -> Expr c -> Constraint c
.==. forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhs2) { constrIndicator :: Maybe (Var, Integer)
MIP.constrIndicator = Maybe (Var, Integer)
ind }
         forall (m :: * -> *) a. Monad m => a -> m a
return ([(Integer, Var)]
ts, Constraint Integer
c)
      else do
         let (Expr Integer
lhsGE,Integer
rhsGE) = Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxGE Var
v (Expr Integer
lhs2,Integer
rhs2)
             c1 :: Constraint Integer
c1 = Expr Integer
lhsGE forall c. Num c => Expr c -> Expr c -> Constraint c
.>=. forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhsGE
         case Op
op of
           Op
PBFile.Ge -> do
             forall (m :: * -> *) a. Monad m => a -> m a
return ([(Integer, Var)]
ts, Constraint Integer
c1)
           Op
PBFile.Eq -> do
             let (Expr Integer
lhsLE,Integer
rhsLE) = Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxLE Var
v (Expr Integer
lhs2,Integer
rhs2)
                 c2 :: Constraint Integer
c2 = Expr Integer
lhsLE forall c. Num c => Expr c -> Expr c -> Constraint c
.<=. forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhsLE
             [ ([(Integer, Var)]
ts, Constraint Integer
c1), ([], Constraint Integer
c2) ]

splitConst :: MIP.Expr Integer -> (MIP.Expr Integer, Integer)
splitConst :: Expr Integer -> (Expr Integer, Integer)
splitConst Expr Integer
e = (Expr Integer
e2, Integer
c)
  where
    e2 :: Expr Integer
e2 = forall c. [Term c] -> Expr c
MIP.Expr [Term Integer
t | t :: Term Integer
t@(MIP.Term Integer
_ (Var
_:[Var]
_)) <- forall c. Expr c -> [Term c]
MIP.terms Expr Integer
e]
    c :: Integer
c = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | MIP.Term Integer
c [] <- forall c. Expr c -> [Term c]
MIP.terms Expr Integer
e]

relaxGE :: MIP.Var -> (MIP.Expr Integer, Integer) -> (MIP.Expr Integer, Integer)
relaxGE :: Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxGE Var
v (Expr Integer
lhs, Integer
rhs) = (forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr (Integer
rhs forall a. Num a => a -> a -> a
- Integer
lhs_lb) forall a. Num a => a -> a -> a
* forall c. Num c => Var -> Expr c
MIP.varExpr Var
v forall a. Num a => a -> a -> a
+ Expr Integer
lhs, Integer
rhs)
  where
    lhs_lb :: Integer
lhs_lb = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [forall a. Ord a => a -> a -> a
min Integer
c Integer
0 | MIP.Term Integer
c [Var]
_ <- forall c. Expr c -> [Term c]
MIP.terms Expr Integer
lhs]

relaxLE :: MIP.Var -> (MIP.Expr Integer, Integer) -> (MIP.Expr Integer, Integer)
relaxLE :: Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxLE Var
v (Expr Integer
lhs, Integer
rhs) = (forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr (Integer
rhs forall a. Num a => a -> a -> a
- Integer
lhs_ub) forall a. Num a => a -> a -> a
* forall c. Num c => Var -> Expr c
MIP.varExpr Var
v forall a. Num a => a -> a -> a
+ Expr Integer
lhs, Integer
rhs)
  where
    lhs_ub :: Integer
lhs_ub = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [forall a. Ord a => a -> a -> a
max Integer
c Integer
0 | MIP.Term Integer
c [Var]
_ <- forall c. Expr c -> [Term c]
MIP.terms Expr Integer
lhs]

mtrans :: Int -> Map MIP.Var Rational -> SAT.Model
mtrans :: Var -> Map Var Rational -> Model
mtrans Var
nvar Map Var Rational
m =
  forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Var
1, Var
nvar)
    [ (Var
i, Bool
val)
    | Var
i <- [Var
1 .. Var
nvar]
    , let val :: Bool
val =
            case forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Rational
0 (Var -> Var
convVar Var
i) Map Var Rational
m of
              Rational
0  -> Bool
False
              Rational
1  -> Bool
True
              Rational
v0 -> forall a. HasCallStack => String -> a
error (forall a. Show a => a -> String
show Rational
v0 forall a. [a] -> [a] -> [a]
++ String
" is neither 0 nor 1")
    ]

-- -----------------------------------------------------------------------------

type SAT2IPInfo = ComposedTransformer SAT2PBInfo PB2IPInfo

sat2ip :: CNF.CNF -> (MIP.Problem Integer, SAT2IPInfo)
sat2ip :: CNF -> (Problem Integer, SAT2IPInfo)
sat2ip CNF
cnf = (Problem Integer
ip, forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2PBInfo
info1 PB2IPInfo
info2)
  where
    (Formula
pb,SAT2PBInfo
info1) = CNF -> (Formula, SAT2PBInfo)
sat2pb CNF
cnf
    (Problem Integer
ip,PB2IPInfo
info2) = Formula -> (Problem Integer, PB2IPInfo)
pb2ip Formula
pb

type MaxSAT2IPInfo = ComposedTransformer MaxSAT2WBOInfo WBO2IPInfo

maxsat2ip :: Bool -> CNF.WCNF -> (MIP.Problem Integer, MaxSAT2IPInfo)
maxsat2ip :: Bool -> WCNF -> (Problem Integer, MaxSAT2IPInfo)
maxsat2ip Bool
useIndicator WCNF
wcnf = (Problem Integer
ip, forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2PBInfo
info1 WBO2IPInfo
info2)
  where
    (SoftFormula
wbo, SAT2PBInfo
info1) = WCNF -> (SoftFormula, SAT2PBInfo)
maxsat2wbo WCNF
wcnf
    (Problem Integer
ip, WBO2IPInfo
info2) = Bool -> SoftFormula -> (Problem Integer, WBO2IPInfo)
wbo2ip Bool
useIndicator SoftFormula
wbo

-- -----------------------------------------------------------------------------