{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.PB
-- Copyright   :  (c) Masahiro Sakai 2013,2016-2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.PB
  ( module ToySolver.Converter.Base
  , module ToySolver.Converter.Tseitin

  -- * Normalization of PB/WBO problems
  , normalizePB
  , normalizeWBO

  -- * Linealization of PB/WBO problems
  , linearizePB
  , linearizeWBO
  , PBLinearizeInfo

  -- * Quadratization of PB problems
  , quadratizePB
  , quadratizePB'
  , PBQuadratizeInfo

  -- * Converting inequality constraints into equality constraints
  , inequalitiesToEqualitiesPB
  , PBInequalitiesToEqualitiesInfo

  -- * Converting constraints into penalty terms in objective function
  , unconstrainPB
  , PBUnconstrainInfo

  -- * PB↔WBO conversion
  , pb2wbo
  , PB2WBOInfo
  , wbo2pb
  , WBO2PBInfo (..)
  , addWBO

  -- * SAT↔PB conversion
  , sat2pb
  , SAT2PBInfo
  , pb2sat
  , PB2SATInfo

  -- * MaxSAT↔WBO conversion
  , maxsat2wbo
  , MaxSAT2WBOInfo
  , wbo2maxsat
  , WBO2MaxSATInfo

  -- * PB→QUBO conversion
  , pb2qubo'
  , PB2QUBOInfo'
  ) where

import Control.Monad
import Control.Monad.Primitive
import Control.Monad.ST
import Data.Array.IArray
import Data.Bits hiding (And (..))
import qualified Data.Foldable as F
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Primitive.MutVar
import qualified Data.Sequence as Seq
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.PseudoBoolean as PBFile

import ToySolver.Converter.Base
import qualified ToySolver.Converter.PB.Internal.Product as Product
import ToySolver.Converter.Tseitin
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))
import qualified ToySolver.SAT.Encoder.PB as PB
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
import ToySolver.SAT.Store.CNF
import ToySolver.SAT.Store.PB

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

-- XXX: we do not normalize objective function, because normalization might
-- introduce constant terms, but OPB file format does not allow constant terms.
--
-- Options:
-- (1) not normalize objective function (current implementation),
-- (2) normalize and simply delete constant terms (in pseudo-boolean package?),
-- (3) normalize and introduce dummy variable to make constant terms
--     into non-constant terms (in pseudo-boolean package?).
normalizePB :: PBFile.Formula -> PBFile.Formula
normalizePB :: Formula -> Formula
normalizePB Formula
formula =
  Formula
formula
  { pbConstraints :: [Constraint]
PBFile.pbConstraints =
      forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Constraint
normalizePBConstraint (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula)
  }

normalizeWBO :: PBFile.SoftFormula -> PBFile.SoftFormula
normalizeWBO :: SoftFormula -> SoftFormula
normalizeWBO SoftFormula
formula =
  SoftFormula
formula
  { wboConstraints :: [SoftConstraint]
PBFile.wboConstraints =
      forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe Integer
w,Constraint
constr) -> (Maybe Integer
w, Constraint -> Constraint
normalizePBConstraint Constraint
constr)) (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula)
  }

normalizePBConstraint :: PBFile.Constraint -> PBFile.Constraint
normalizePBConstraint :: Constraint -> Constraint
normalizePBConstraint (Sum
lhs,Op
op,Integer
rhs) =
  case forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL forall {a} {a}.
(Ord a, Num a, Num a) =>
a -> (a, [a]) -> (a, (a, [a]))
h Integer
0 Sum
lhs of
    (Integer
offset, Sum
lhs') -> (Sum
lhs', Op
op, Integer
rhs forall a. Num a => a -> a -> a
- Integer
offset)
  where
    h :: a -> (a, [a]) -> (a, (a, [a]))
h a
s (a
w,[a
x]) | a
x forall a. Ord a => a -> a -> Bool
< a
0 = (a
sforall a. Num a => a -> a -> a
+a
w, (-a
w,[-a
x]))
    h a
s (a, [a])
t = (a
s,(a, [a])
t)

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

type PBLinearizeInfo = TseitinInfo

linearizePB :: PBFile.Formula -> Bool -> (PBFile.Formula, PBLinearizeInfo)
linearizePB :: Formula -> Bool -> (Formula, PBLinearizeInfo)
linearizePB Formula
formula Bool
usePB = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  PBStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ PBStore (ST s)
db (Formula -> Lit
PBFile.pbNumVars Formula
formula)
  Encoder (ST s)
tseitin <-  forall (m :: * -> *) a.
(PrimMonad m, AddPBLin m a) =>
a -> m (Encoder m)
Tseitin.newEncoderWithPBLin PBStore (ST s)
db
  forall (m :: * -> *). PrimMonad m => Encoder m -> Bool -> m ()
Tseitin.setUsePB Encoder (ST s)
tseitin Bool
usePB
  Encoder (ST s)
pbnlc <- forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder PBStore (ST s)
db Encoder (ST s)
tseitin
  [Constraint]
cs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula) forall a b. (a -> b) -> a -> b
$ \(Sum
lhs,Op
op,Integer
rhs) -> do
    let p :: Polarity
p = case Op
op of
              Op
PBFile.Ge -> Polarity
Tseitin.polarityPos
              Op
PBFile.Eq -> Polarity
Tseitin.polarityBoth
    PBLinSum
lhs' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
p Sum
lhs
    forall (m :: * -> *) a. Monad m => a -> m a
return ([(Integer
c,[Lit
l]) | (Integer
c,Lit
l) <- PBLinSum
lhs'],Op
op,Integer
rhs)
  Maybe Sum
obj' <-
    case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
      Maybe Sum
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Just Sum
obj -> do
        PBLinSum
obj' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
Tseitin.polarityNeg Sum
obj
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [(Integer
c, [Lit
l]) | (Integer
c,Lit
l) <- PBLinSum
obj']
  Formula
formula' <- forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  [(Lit, Formula)]
defs <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    ( Formula
formula'
      { pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = Maybe Sum
obj'
      , pbConstraints :: [Constraint]
PBFile.pbConstraints = [Constraint]
cs' forall a. [a] -> [a] -> [a]
++ Formula -> [Constraint]
PBFile.pbConstraints Formula
formula'
      , pbNumConstraints :: Lit
PBFile.pbNumConstraints = Formula -> Lit
PBFile.pbNumConstraints Formula
formula forall a. Num a => a -> a -> a
+ Formula -> Lit
PBFile.pbNumConstraints Formula
formula'
      }
    , Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo (Formula -> Lit
PBFile.pbNumVars Formula
formula) (Formula -> Lit
PBFile.pbNumVars Formula
formula') [(Lit, Formula)]
defs
    )

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

linearizeWBO :: PBFile.SoftFormula -> Bool -> (PBFile.SoftFormula, PBLinearizeInfo)
linearizeWBO :: SoftFormula -> Bool -> (SoftFormula, PBLinearizeInfo)
linearizeWBO SoftFormula
formula Bool
usePB = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  PBStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ PBStore (ST s)
db (SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
formula)
  Encoder (ST s)
tseitin <-  forall (m :: * -> *) a.
(PrimMonad m, AddPBLin m a) =>
a -> m (Encoder m)
Tseitin.newEncoderWithPBLin PBStore (ST s)
db
  forall (m :: * -> *). PrimMonad m => Encoder m -> Bool -> m ()
Tseitin.setUsePB Encoder (ST s)
tseitin Bool
usePB
  Encoder (ST s)
pbnlc <- forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder PBStore (ST s)
db Encoder (ST s)
tseitin
  [SoftConstraint]
cs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula) forall a b. (a -> b) -> a -> b
$ \(Maybe Integer
cost,(Sum
lhs,Op
op,Integer
rhs)) -> do
    let p :: Polarity
p = case Op
op of
              Op
PBFile.Ge -> Polarity
Tseitin.polarityPos
              Op
PBFile.Eq -> Polarity
Tseitin.polarityBoth
    PBLinSum
lhs' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
p Sum
lhs
    forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
cost,([(Integer
c,[Lit
l]) | (Integer
c,Lit
l) <- PBLinSum
lhs'],Op
op,Integer
rhs))
  Formula
formula' <- forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  [(Lit, Formula)]
defs <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    ( PBFile.SoftFormula
      { wboTopCost :: Maybe Integer
PBFile.wboTopCost = SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula
      , wboConstraints :: [SoftConstraint]
PBFile.wboConstraints = [SoftConstraint]
cs' forall a. [a] -> [a] -> [a]
++ [(forall a. Maybe a
Nothing, Constraint
constr) | Constraint
constr <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula']
      , wboNumVars :: Lit
PBFile.wboNumVars = Formula -> Lit
PBFile.pbNumVars Formula
formula'
      , wboNumConstraints :: Lit
PBFile.wboNumConstraints = SoftFormula -> Lit
PBFile.wboNumConstraints SoftFormula
formula forall a. Num a => a -> a -> a
+ Formula -> Lit
PBFile.pbNumConstraints Formula
formula'
      }
    , Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo (SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
formula) (Formula -> Lit
PBFile.pbNumVars Formula
formula') [(Lit, Formula)]
defs
    )

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

-- | Quandratize PBO/PBS problem without introducing additional constraints.
quadratizePB :: PBFile.Formula -> ((PBFile.Formula, Integer), PBQuadratizeInfo)
quadratizePB :: Formula -> ((Formula, Integer), PBQuadratizeInfo)
quadratizePB Formula
formula = (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo)
quadratizePB' (Formula
formula, Sum -> Integer
SAT.pbUpperBound Sum
obj)
  where
    obj :: Sum
obj = forall a. a -> Maybe a -> a
fromMaybe [] forall a b. (a -> b) -> a -> b
$ Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula

-- | Quandratize PBO/PBS problem without introducing additional constraints.
quadratizePB' :: (PBFile.Formula, Integer) -> ((PBFile.Formula, Integer), PBQuadratizeInfo)
quadratizePB' :: (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo)
quadratizePB' (Formula
formula, Integer
maxObj) =
  ( ( PBFile.Formula
      { pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Sum -> Sum
conv Sum
obj forall a. [a] -> [a] -> [a]
++ Sum
penalty
      , pbConstraints :: [Constraint]
PBFile.pbConstraints = [(Sum -> Sum
conv Sum
lhs, Op
op, Integer
rhs) | (Sum
lhs,Op
op,Integer
rhs) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
      , pbNumVars :: Lit
PBFile.pbNumVars = Lit
nv2
      , pbNumConstraints :: Lit
PBFile.pbNumConstraints = Formula -> Lit
PBFile.pbNumConstraints Formula
formula
      }
    , Integer
maxObj
    )
  , PBLinearizeInfo -> PBQuadratizeInfo
PBQuadratizeInfo forall a b. (a -> b) -> a -> b
$ Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo Lit
nv1 Lit
nv2 [(Lit
v, [Formula] -> Formula
And [Lit -> Formula
Atom Lit
l1, Lit -> Formula
Atom Lit
l2]) | (Lit
v, (Lit
l1,Lit
l2)) <- [(Lit, (Lit, Lit))]
prodDefs]
  )
  where
    nv1 :: Lit
nv1 = Formula -> Lit
PBFile.pbNumVars Formula
formula
    nv2 :: Lit
nv2 = Formula -> Lit
PBFile.pbNumVars Formula
formula forall a. Num a => a -> a -> a
+ forall a. Set a -> Lit
Set.size Set IntSet
termsToReplace

    degGe3Terms :: Set IntSet
    degGe3Terms :: Set IntSet
degGe3Terms = Formula -> Set IntSet
collectDegGe3Terms Formula
formula

    m :: Map IntSet (IntSet,IntSet)
    m :: Map IntSet (IntSet, IntSet)
m = Set IntSet -> Map IntSet (IntSet, IntSet)
Product.decomposeToBinaryProducts Set IntSet
degGe3Terms

    termsToReplace :: Set IntSet
    termsToReplace :: Set IntSet
termsToReplace = [IntSet] -> Set IntSet -> Set IntSet
go [IntSet]
ts0 forall a. Set a
Set.empty
      where
        ts0 :: [IntSet]
ts0 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[IntSet
t1,IntSet
t2] | IntSet
t <- forall a. Set a -> [a]
Set.toList Set IntSet
degGe3Terms, let (IntSet
t1,IntSet
t2) = Map IntSet (IntSet, IntSet)
m forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t]
        go :: [IntSet] -> Set IntSet -> Set IntSet
go [] !Set IntSet
ret = Set IntSet
ret
        go (IntSet
t : [IntSet]
ts) !Set IntSet
ret
          | IntSet -> Lit
IntSet.size IntSet
t forall a. Ord a => a -> a -> Bool
< Lit
2  = [IntSet] -> Set IntSet -> Set IntSet
go [IntSet]
ts Set IntSet
ret
          | IntSet
t forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
ret = [IntSet] -> Set IntSet -> Set IntSet
go [IntSet]
ts Set IntSet
ret
          | Bool
otherwise =
              case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t Map IntSet (IntSet, IntSet)
m of
                Maybe (IntSet, IntSet)
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"quadratizePB.termsToReplace: should not happen"
                Just (IntSet
t1,IntSet
t2) -> [IntSet] -> Set IntSet -> Set IntSet
go (IntSet
t1 forall a. a -> [a] -> [a]
: IntSet
t2 forall a. a -> [a] -> [a]
: [IntSet]
ts) (forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
t Set IntSet
ret)

    fromV :: IntMap IntSet
    toV :: Map IntSet Int
    (IntMap IntSet
fromV, Map IntSet Lit
toV) = (forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit, IntSet)]
l, forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(IntSet
s,Lit
v) | (Lit
v,IntSet
s) <- [(Lit, IntSet)]
l])
      where
        l :: [(Lit, IntSet)]
l = forall a b. [a] -> [b] -> [(a, b)]
zip [Formula -> Lit
PBFile.pbNumVars Formula
formula forall a. Num a => a -> a -> a
+ Lit
1 ..] (forall a. Set a -> [a]
Set.toList Set IntSet
termsToReplace)

    prodDefs :: [(SAT.Var, (SAT.Var, SAT.Var))]
    prodDefs :: [(Lit, (Lit, Lit))]
prodDefs = [(Lit
v, (IntSet -> Lit
f IntSet
t1, IntSet -> Lit
f IntSet
t2)) | (Lit
v,IntSet
t) <- forall a. IntMap a -> [(Lit, a)]
IntMap.toList IntMap IntSet
fromV, let (IntSet
t1,IntSet
t2) = Map IntSet (IntSet, IntSet)
m forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t]
      where
        f :: IntSet -> Lit
f IntSet
t
          | IntSet -> Lit
IntSet.size IntSet
t forall a. Eq a => a -> a -> Bool
== Lit
1 = forall a. [a] -> a
head (IntSet -> [Lit]
IntSet.toList IntSet
t)
          | Bool
otherwise =
               case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t Map IntSet Lit
toV of
                 Maybe Lit
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"quadratizePB.prodDefs: should not happen"
                 Just Lit
v -> Lit
v

    obj :: PBFile.Sum
    obj :: Sum
obj = forall a. a -> Maybe a -> a
fromMaybe [] forall a b. (a -> b) -> a -> b
$ Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula

    minObj :: Integer
    minObj :: Integer
minObj = Sum -> Integer
SAT.pbLowerBound Sum
obj

    penalty :: PBFile.Sum
    penalty :: Sum
penalty = [(Integer
w forall a. Num a => a -> a -> a
* Integer
w2, [Lit]
ts) | (Integer
w,[Lit]
ts) <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall {a} {a}. Num a => a -> a -> a -> [(a, [a])]
p Lit
x Lit
y Lit
z | (Lit
z,(Lit
x,Lit
y)) <- [(Lit, (Lit, Lit))]
prodDefs]]
      where
        -- The penalty function P(x,y,z) = xy − 2xz − 2yz + 3z is such that
        -- P(x,y,z)=0 when z⇔xy and P(x,y,z)>0 when z⇎xy.
        p :: a -> a -> a -> [(a, [a])]
p a
x a
y a
z = [(a
1,[a
x,a
y]), (-a
2,[a
x,a
z]), (-a
2,[a
y,a
z]), (a
3,[a
z])]
        w2 :: Integer
w2 = forall a. Ord a => a -> a -> a
max (Integer
maxObj forall a. Num a => a -> a -> a
- Integer
minObj) Integer
0 forall a. Num a => a -> a -> a
+ Integer
1

    conv :: PBFile.Sum -> PBFile.Sum
    conv :: Sum -> Sum
conv Sum
s = [(Integer
w, [Lit] -> [Lit]
f [Lit]
t) | (Integer
w,[Lit]
t) <- Sum
s]
      where
        f :: [Lit] -> [Lit]
f [Lit]
t =
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t' Map IntSet Lit
toV of
            Just Lit
v  -> [Lit
v]
            Maybe Lit
Nothing
              | IntSet -> Lit
IntSet.size IntSet
t' forall a. Ord a => a -> a -> Bool
>= Lit
3 -> forall a b. (a -> b) -> [a] -> [b]
map IntSet -> Lit
g [IntSet
t1, IntSet
t2]
              | Bool
otherwise -> [Lit]
t
          where
            t' :: IntSet
t' = [Lit] -> IntSet
IntSet.fromList [Lit]
t
            (IntSet
t1, IntSet
t2) = Map IntSet (IntSet, IntSet)
m forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t'
        g :: IntSet -> Lit
g IntSet
t
          | IntSet -> Lit
IntSet.size IntSet
t forall a. Eq a => a -> a -> Bool
== Lit
1 = forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ IntSet -> [Lit]
IntSet.toList IntSet
t
          | Bool
otherwise = Map IntSet Lit
toV forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t


collectDegGe3Terms :: PBFile.Formula -> Set IntSet
collectDegGe3Terms :: Formula -> Set IntSet
collectDegGe3Terms Formula
formula = forall a. Ord a => [a] -> Set a
Set.fromList [IntSet
t' | [Lit]
t <- [[Lit]]
terms, let t' :: IntSet
t' = [Lit] -> IntSet
IntSet.fromList [Lit]
t, IntSet -> Lit
IntSet.size IntSet
t' forall a. Ord a => a -> a -> Bool
>= Lit
3]
  where
    sums :: [Sum]
sums = forall a. Maybe a -> [a]
maybeToList (Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula) forall a. [a] -> [a] -> [a]
++
           [Sum
lhs | (Sum
lhs,Op
_,Integer
_) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    terms :: [[Lit]]
terms = [[Lit]
t | Sum
s <- [Sum]
sums, (Integer
_,[Lit]
t) <- Sum
s]

newtype PBQuadratizeInfo = PBQuadratizeInfo TseitinInfo
  deriving (PBQuadratizeInfo -> PBQuadratizeInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PBQuadratizeInfo -> PBQuadratizeInfo -> Bool
$c/= :: PBQuadratizeInfo -> PBQuadratizeInfo -> Bool
== :: PBQuadratizeInfo -> PBQuadratizeInfo -> Bool
$c== :: PBQuadratizeInfo -> PBQuadratizeInfo -> Bool
Eq, Lit -> PBQuadratizeInfo -> ShowS
[PBQuadratizeInfo] -> ShowS
PBQuadratizeInfo -> [Char]
forall a.
(Lit -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [PBQuadratizeInfo] -> ShowS
$cshowList :: [PBQuadratizeInfo] -> ShowS
show :: PBQuadratizeInfo -> [Char]
$cshow :: PBQuadratizeInfo -> [Char]
showsPrec :: Lit -> PBQuadratizeInfo -> ShowS
$cshowsPrec :: Lit -> PBQuadratizeInfo -> ShowS
Show)

instance Transformer PBQuadratizeInfo where
  type Source PBQuadratizeInfo = SAT.Model
  type Target PBQuadratizeInfo = SAT.Model

instance ForwardTransformer PBQuadratizeInfo where
  transformForward :: PBQuadratizeInfo
-> Source PBQuadratizeInfo -> Target PBQuadratizeInfo
transformForward (PBQuadratizeInfo PBLinearizeInfo
info) = forall a. ForwardTransformer a => a -> Source a -> Target a
transformForward PBLinearizeInfo
info

instance BackwardTransformer PBQuadratizeInfo where
  transformBackward :: PBQuadratizeInfo
-> Target PBQuadratizeInfo -> Source PBQuadratizeInfo
transformBackward (PBQuadratizeInfo PBLinearizeInfo
info) = forall a. BackwardTransformer a => a -> Target a -> Source a
transformBackward PBLinearizeInfo
info

instance ObjValueTransformer PBQuadratizeInfo where
  type SourceObjValue PBQuadratizeInfo = Integer
  type TargetObjValue PBQuadratizeInfo = Integer

instance ObjValueForwardTransformer PBQuadratizeInfo where
  transformObjValueForward :: PBQuadratizeInfo
-> SourceObjValue PBQuadratizeInfo
-> TargetObjValue PBQuadratizeInfo
transformObjValueForward PBQuadratizeInfo
_ = forall a. a -> a
id

instance ObjValueBackwardTransformer PBQuadratizeInfo where
  transformObjValueBackward :: PBQuadratizeInfo
-> TargetObjValue PBQuadratizeInfo
-> SourceObjValue PBQuadratizeInfo
transformObjValueBackward PBQuadratizeInfo
_ = forall a. a -> a
id

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

-- | Convert inequality constraints into equality constraints by introducing surpass variables.
inequalitiesToEqualitiesPB :: PBFile.Formula -> (PBFile.Formula, PBInequalitiesToEqualitiesInfo)
inequalitiesToEqualitiesPB :: Formula -> (Formula, PBInequalitiesToEqualitiesInfo)
inequalitiesToEqualitiesPB Formula
formula = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  PBStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ PBStore (ST s)
db (Formula -> Lit
PBFile.pbNumVars Formula
formula)

  [(Sum, Integer, [Lit])]
defs <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula) forall a b. (a -> b) -> a -> b
$ \Constraint
constr -> do
    case Constraint
constr of
      (Sum
lhs, Op
PBFile.Eq, Integer
rhs) -> do
        forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly PBStore (ST s)
db Sum
lhs Integer
rhs
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      (Sum
lhs, Op
PBFile.Ge, Integer
rhs) -> do
        case (Sum, Integer) -> Maybe [Lit]
asClause (Sum
lhs,Integer
rhs) of
          Just [Lit]
clause -> do
            forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly PBStore (ST s)
db [(Integer
1, [- Lit
l | Lit
l <- [Lit]
clause])] Integer
0
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
          Maybe [Lit]
Nothing -> do
            let maxSurpass :: Integer
maxSurpass = forall a. Ord a => a -> a -> a
max (Sum -> Integer
SAT.pbUpperBound Sum
lhs forall a. Num a => a -> a -> a
- Integer
rhs) Integer
0
                maxSurpassNBits :: Lit
maxSurpassNBits = forall a. [a] -> a
head [Lit
i | Lit
i <- [Lit
0..], Integer
maxSurpass forall a. Ord a => a -> a -> Bool
< forall a. Bits a => Lit -> a
bit Lit
i]
            [Lit]
vs <- forall (m :: * -> *) a. NewVar m a => a -> Lit -> m [Lit]
SAT.newVars PBStore (ST s)
db Lit
maxSurpassNBits
            forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly PBStore (ST s)
db (Sum
lhs forall a. [a] -> [a] -> [a]
++ [(-Integer
c,[Lit
x]) | (Integer
c,Lit
x) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. (a -> a) -> a -> [a]
iterate (forall a. Num a => a -> a -> a
*Integer
2) Integer
1) [Lit]
vs]) Integer
rhs
            if Lit
maxSurpassNBits forall a. Ord a => a -> a -> Bool
> Lit
0 then do
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Sum
lhs, Integer
rhs, [Lit]
vs)
            else
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

  Formula
formula' <- forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  forall (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula'{ pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula }
    , Lit
-> Lit -> [(Sum, Integer, [Lit])] -> PBInequalitiesToEqualitiesInfo
PBInequalitiesToEqualitiesInfo (Formula -> Lit
PBFile.pbNumVars Formula
formula) (Formula -> Lit
PBFile.pbNumVars Formula
formula') [(Sum, Integer, [Lit])]
defs
    )
  where
    asLinSum :: SAT.PBSum -> Maybe (SAT.PBLinSum, Integer)
    asLinSum :: Sum -> Maybe (PBLinSum, Integer)
asLinSum Sum
s = do
      [(Maybe (Integer, Lit), Integer)]
ret <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Sum
s forall a b. (a -> b) -> a -> b
$ \(Integer
c, [Lit]
ls) -> do
        case [Lit]
ls of
          [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, Integer
c)
          [Lit
l] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Integer
c,Lit
l), Integer
0)
          [Lit]
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [Maybe a] -> [a]
catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Maybe (Integer, Lit), Integer)]
ret), forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Maybe (Integer, Lit), Integer)]
ret))

    asClause :: (SAT.PBSum, Integer) -> Maybe SAT.Clause
    asClause :: (Sum, Integer) -> Maybe [Lit]
asClause (Sum
lhs, Integer
rhs) = do
      (PBLinSum
lhs', Integer
off) <- Sum -> Maybe (PBLinSum, Integer)
asLinSum Sum
lhs
      let rhs' :: Integer
rhs' = Integer
rhs forall a. Num a => a -> a -> a
- Integer
off
      case (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinAtLeast (PBLinSum
lhs', Integer
rhs') of
        (PBLinSum
lhs'', Integer
1) | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Integer
c,Lit
_) -> Integer
c forall a. Eq a => a -> a -> Bool
== Integer
1) PBLinSum
lhs'' -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd PBLinSum
lhs'')
        (PBLinSum, Integer)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

data PBInequalitiesToEqualitiesInfo
  = PBInequalitiesToEqualitiesInfo !Int !Int [(PBFile.Sum, Integer, [SAT.Var])]
  deriving (PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
$c/= :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
== :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
$c== :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
Eq, Lit -> PBInequalitiesToEqualitiesInfo -> ShowS
[PBInequalitiesToEqualitiesInfo] -> ShowS
PBInequalitiesToEqualitiesInfo -> [Char]
forall a.
(Lit -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [PBInequalitiesToEqualitiesInfo] -> ShowS
$cshowList :: [PBInequalitiesToEqualitiesInfo] -> ShowS
show :: PBInequalitiesToEqualitiesInfo -> [Char]
$cshow :: PBInequalitiesToEqualitiesInfo -> [Char]
showsPrec :: Lit -> PBInequalitiesToEqualitiesInfo -> ShowS
$cshowsPrec :: Lit -> PBInequalitiesToEqualitiesInfo -> ShowS
Show)

instance Transformer PBInequalitiesToEqualitiesInfo where
  type Source PBInequalitiesToEqualitiesInfo = SAT.Model
  type Target PBInequalitiesToEqualitiesInfo = SAT.Model

instance ForwardTransformer PBInequalitiesToEqualitiesInfo where
  transformForward :: PBInequalitiesToEqualitiesInfo
-> Source PBInequalitiesToEqualitiesInfo
-> Target PBInequalitiesToEqualitiesInfo
transformForward (PBInequalitiesToEqualitiesInfo Lit
_nv1 Lit
nv2 [(Sum, Integer, [Lit])]
defs) Source PBInequalitiesToEqualitiesInfo
m =
    forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1, Lit
nv2) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source PBInequalitiesToEqualitiesInfo
m forall a. [a] -> [a] -> [a]
++ [(Lit
v, forall a. Bits a => a -> Lit -> Bool
testBit Integer
n Lit
i) | (Sum
lhs, Integer
rhs, [Lit]
vs) <- [(Sum, Integer, [Lit])]
defs, let n :: Integer
n = forall m. IModel m => m -> Sum -> Integer
SAT.evalPBSum Source PBInequalitiesToEqualitiesInfo
m Sum
lhs forall a. Num a => a -> a -> a
- Integer
rhs, (Lit
i,Lit
v) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Lit
0..] [Lit]
vs]

instance BackwardTransformer PBInequalitiesToEqualitiesInfo where
  transformBackward :: PBInequalitiesToEqualitiesInfo
-> Target PBInequalitiesToEqualitiesInfo
-> Source PBInequalitiesToEqualitiesInfo
transformBackward (PBInequalitiesToEqualitiesInfo Lit
nv1 Lit
_nv2 [(Sum, Integer, [Lit])]
_defs) = Lit -> Model -> Model
SAT.restrictModel Lit
nv1

instance ObjValueTransformer PBInequalitiesToEqualitiesInfo where
  type SourceObjValue PBInequalitiesToEqualitiesInfo = Integer
  type TargetObjValue PBInequalitiesToEqualitiesInfo = Integer

instance ObjValueForwardTransformer PBInequalitiesToEqualitiesInfo where
  transformObjValueForward :: PBInequalitiesToEqualitiesInfo
-> SourceObjValue PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
transformObjValueForward PBInequalitiesToEqualitiesInfo
_ = forall a. a -> a
id

instance ObjValueBackwardTransformer PBInequalitiesToEqualitiesInfo where
  transformObjValueBackward :: PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
-> SourceObjValue PBInequalitiesToEqualitiesInfo
transformObjValueBackward PBInequalitiesToEqualitiesInfo
_ = forall a. a -> a
id

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

unconstrainPB :: PBFile.Formula -> ((PBFile.Formula, Integer), PBUnconstrainInfo)
unconstrainPB :: Formula -> ((Formula, Integer), PBUnconstrainInfo)
unconstrainPB Formula
formula = (Formula -> (Formula, Integer)
unconstrainPB' Formula
formula', PBInequalitiesToEqualitiesInfo -> PBUnconstrainInfo
PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info)
  where
    (Formula
formula', PBInequalitiesToEqualitiesInfo
info) = Formula -> (Formula, PBInequalitiesToEqualitiesInfo)
inequalitiesToEqualitiesPB Formula
formula

newtype PBUnconstrainInfo = PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
  deriving (PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
$c/= :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
== :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
$c== :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
Eq, Lit -> PBUnconstrainInfo -> ShowS
[PBUnconstrainInfo] -> ShowS
PBUnconstrainInfo -> [Char]
forall a.
(Lit -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [PBUnconstrainInfo] -> ShowS
$cshowList :: [PBUnconstrainInfo] -> ShowS
show :: PBUnconstrainInfo -> [Char]
$cshow :: PBUnconstrainInfo -> [Char]
showsPrec :: Lit -> PBUnconstrainInfo -> ShowS
$cshowsPrec :: Lit -> PBUnconstrainInfo -> ShowS
Show)

instance Transformer PBUnconstrainInfo where
  -- type Source PBUnconstrainInfo = Source PBInequalitiesToEqualitiesInfo
  type Source PBUnconstrainInfo = SAT.Model
  -- type Target PBUnconstrainInfo = Target PBInequalitiesToEqualitiesInfo
  type Target PBUnconstrainInfo = SAT.Model

instance ForwardTransformer PBUnconstrainInfo where
  transformForward :: PBUnconstrainInfo
-> Source PBUnconstrainInfo -> Target PBUnconstrainInfo
transformForward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = forall a. ForwardTransformer a => a -> Source a -> Target a
transformForward PBInequalitiesToEqualitiesInfo
info

instance BackwardTransformer PBUnconstrainInfo where
  transformBackward :: PBUnconstrainInfo
-> Target PBUnconstrainInfo -> Source PBUnconstrainInfo
transformBackward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = forall a. BackwardTransformer a => a -> Target a -> Source a
transformBackward PBInequalitiesToEqualitiesInfo
info

instance ObjValueTransformer PBUnconstrainInfo where
  -- type SourceObjValue PBUnconstrainInfo = SourceObjValue PBInequalitiesToEqualitiesInfo
  type SourceObjValue PBUnconstrainInfo = Integer
  -- type TargetObjValue PBUnconstrainInfo = TargetObjValue PBInequalitiesToEqualitiesInfo
  type TargetObjValue PBUnconstrainInfo = Integer

instance ObjValueForwardTransformer PBUnconstrainInfo where
  transformObjValueForward :: PBUnconstrainInfo
-> SourceObjValue PBUnconstrainInfo
-> TargetObjValue PBUnconstrainInfo
transformObjValueForward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = forall a.
ObjValueForwardTransformer a =>
a -> SourceObjValue a -> TargetObjValue a
transformObjValueForward PBInequalitiesToEqualitiesInfo
info

instance ObjValueBackwardTransformer PBUnconstrainInfo where
  transformObjValueBackward :: PBUnconstrainInfo
-> TargetObjValue PBUnconstrainInfo
-> SourceObjValue PBUnconstrainInfo
transformObjValueBackward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = forall a.
ObjValueBackwardTransformer a =>
a -> TargetObjValue a -> SourceObjValue a
transformObjValueBackward PBInequalitiesToEqualitiesInfo
info

unconstrainPB' :: PBFile.Formula -> (PBFile.Formula, Integer)
unconstrainPB' :: Formula -> (Formula, Integer)
unconstrainPB' Formula
formula =
  ( Formula
formula
    { pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Sum
obj1 forall a. [a] -> [a] -> [a]
++ Sum
obj2
    , pbConstraints :: [Constraint]
PBFile.pbConstraints = []
    , pbNumConstraints :: Lit
PBFile.pbNumConstraints = Lit
0
    }
  , Integer
obj1ub
  )
  where
    obj1 :: Sum
obj1 = forall a. a -> Maybe a -> a
fromMaybe [] (Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula)
    obj1ub :: Integer
obj1ub = Sum -> Integer
SAT.pbUpperBound Sum
obj1
    obj1lb :: Integer
obj1lb = Sum -> Integer
SAT.pbLowerBound Sum
obj1
    p :: Integer
p = Integer
obj1ub forall a. Num a => a -> a -> a
- Integer
obj1lb forall a. Num a => a -> a -> a
+ Integer
1
    obj2 :: Sum
obj2 = [(Integer
pforall a. Num a => a -> a -> a
*Integer
c, IntSet -> [Lit]
IntSet.toList IntSet
ls) | (IntSet
ls, Integer
c) <- forall k a. Map k a -> [(k, a)]
Map.toList Map IntSet Integer
obj2', Integer
c forall a. Eq a => a -> a -> Bool
/= Integer
0]
    obj2' :: Map IntSet Integer
obj2' = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Num a => a -> a -> a
(+) [forall {a}. Num a => [(a, [Lit])] -> Map IntSet a
sq ((-Integer
rhs, []) forall a. a -> [a] -> [a]
: Sum
lhs) | (Sum
lhs, Op
PBFile.Eq, Integer
rhs) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    sq :: [(a, [Lit])] -> Map IntSet a
sq [(a, [Lit])]
ts = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Num a => a -> a -> a
(+) forall a b. (a -> b) -> a -> b
$ do
              (a
c1,[Lit]
ls1) <- [(a, [Lit])]
ts
              (a
c2,[Lit]
ls2) <- [(a, [Lit])]
ts
              let ls3 :: IntSet
ls3 = [Lit] -> IntSet
IntSet.fromList [Lit]
ls1 IntSet -> IntSet -> IntSet
`IntSet.union` [Lit] -> IntSet
IntSet.fromList [Lit]
ls2
              forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ IntSet -> Bool
isFalse IntSet
ls3
              forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet
ls3, a
c1forall a. Num a => a -> a -> a
*a
c2)
    isFalse :: IntSet -> Bool
isFalse IntSet
ls = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ IntSet -> Bool
IntSet.null forall a b. (a -> b) -> a -> b
$ IntSet
ls IntSet -> IntSet -> IntSet
`IntSet.intersection` (Lit -> Lit) -> IntSet -> IntSet
IntSet.map forall a. Num a => a -> a
negate IntSet
ls

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

pb2qubo' :: PBFile.Formula -> ((PBFile.Formula, Integer), PB2QUBOInfo')
pb2qubo' :: Formula -> ((Formula, Integer), PB2QUBOInfo')
pb2qubo' Formula
formula = ((Formula
formula2, Integer
th2), forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer PBUnconstrainInfo
info1 PBQuadratizeInfo
info2)
  where
    ((Formula
formula1, Integer
th1), PBUnconstrainInfo
info1) = Formula -> ((Formula, Integer), PBUnconstrainInfo)
unconstrainPB Formula
formula
    ((Formula
formula2, Integer
th2), PBQuadratizeInfo
info2) = (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo)
quadratizePB' (Formula
formula1, Integer
th1)

type PB2QUBOInfo' = ComposedTransformer PBUnconstrainInfo PBQuadratizeInfo

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

type PB2WBOInfo = IdentityTransformer SAT.Model

pb2wbo :: PBFile.Formula -> (PBFile.SoftFormula, PB2WBOInfo)
pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo)
pb2wbo Formula
formula
  = ( PBFile.SoftFormula
      { wboTopCost :: Maybe Integer
PBFile.wboTopCost = forall a. Maybe a
Nothing
      , wboConstraints :: [SoftConstraint]
PBFile.wboConstraints = [SoftConstraint]
cs1 forall a. [a] -> [a] -> [a]
++ [SoftConstraint]
cs2
      , wboNumVars :: Lit
PBFile.wboNumVars = Formula -> Lit
PBFile.pbNumVars Formula
formula
      , wboNumConstraints :: Lit
PBFile.wboNumConstraints = Formula -> Lit
PBFile.pbNumConstraints Formula
formula forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Lit
length [SoftConstraint]
cs2
      }
    , forall a. IdentityTransformer a
IdentityTransformer
    )
  where
    cs1 :: [SoftConstraint]
cs1 = [(forall a. Maybe a
Nothing, Constraint
c) | Constraint
c <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    cs2 :: [SoftConstraint]
cs2 = case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
            Maybe Sum
Nothing -> []
            Just Sum
e  ->
              [ if Integer
w forall a. Ord a => a -> a -> Bool
>= Integer
0
                then (forall a. a -> Maybe a
Just Integer
w,       ([(-Integer
1,[Lit]
ls)], Op
PBFile.Ge, Integer
0))
                else (forall a. a -> Maybe a
Just (forall a. Num a => a -> a
abs Integer
w), ([(Integer
1,[Lit]
ls)],  Op
PBFile.Ge, Integer
1))
              | (Integer
w,[Lit]
ls) <- Sum
e
              ]

wbo2pb :: PBFile.SoftFormula -> (PBFile.Formula, WBO2PBInfo)
wbo2pb :: SoftFormula -> (Formula, WBO2PBInfo)
wbo2pb SoftFormula
wbo = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  let nv :: Lit
nv = SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
wbo
  PBStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  (Sum
obj, [(Lit, Constraint)]
defs) <- forall (m :: * -> *) enc.
(PrimMonad m, AddPBNL m enc) =>
enc -> SoftFormula -> m (Sum, [(Lit, Constraint)])
addWBO PBStore (ST s)
db SoftFormula
wbo
  Formula
formula <- forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  forall (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula{ pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = forall a. a -> Maybe a
Just Sum
obj }
    , Lit -> Lit -> [(Lit, Constraint)] -> WBO2PBInfo
WBO2PBInfo Lit
nv (Formula -> Lit
PBFile.pbNumVars Formula
formula) [(Lit, Constraint)]
defs
    )

data WBO2PBInfo = WBO2PBInfo !Int !Int [(SAT.Var, PBFile.Constraint)]
  deriving (WBO2PBInfo -> WBO2PBInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WBO2PBInfo -> WBO2PBInfo -> Bool
$c/= :: WBO2PBInfo -> WBO2PBInfo -> Bool
== :: WBO2PBInfo -> WBO2PBInfo -> Bool
$c== :: WBO2PBInfo -> WBO2PBInfo -> Bool
Eq, Lit -> WBO2PBInfo -> ShowS
[WBO2PBInfo] -> ShowS
WBO2PBInfo -> [Char]
forall a.
(Lit -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [WBO2PBInfo] -> ShowS
$cshowList :: [WBO2PBInfo] -> ShowS
show :: WBO2PBInfo -> [Char]
$cshow :: WBO2PBInfo -> [Char]
showsPrec :: Lit -> WBO2PBInfo -> ShowS
$cshowsPrec :: Lit -> WBO2PBInfo -> ShowS
Show)

instance Transformer WBO2PBInfo where
  type Source WBO2PBInfo = SAT.Model
  type Target WBO2PBInfo = SAT.Model

instance ForwardTransformer WBO2PBInfo where
  transformForward :: WBO2PBInfo -> Source WBO2PBInfo -> Target WBO2PBInfo
transformForward (WBO2PBInfo Lit
_nv1 Lit
nv2 [(Lit, Constraint)]
defs) Source WBO2PBInfo
m =
    forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1, Lit
nv2) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source WBO2PBInfo
m forall a. [a] -> [a] -> [a]
++ [(Lit
v, forall m. IModel m => m -> Constraint -> Bool
SAT.evalPBConstraint Source WBO2PBInfo
m Constraint
constr) | (Lit
v, Constraint
constr) <- [(Lit, Constraint)]
defs]

instance BackwardTransformer WBO2PBInfo where
  transformBackward :: WBO2PBInfo -> Target WBO2PBInfo -> Source WBO2PBInfo
transformBackward (WBO2PBInfo Lit
nv1 Lit
_nv2 [(Lit, Constraint)]
_defs) = Lit -> Model -> Model
SAT.restrictModel Lit
nv1

addWBO :: (PrimMonad m, SAT.AddPBNL m enc) => enc -> PBFile.SoftFormula -> m (SAT.PBSum, [(SAT.Var, PBFile.Constraint)])
addWBO :: forall (m :: * -> *) enc.
(PrimMonad m, AddPBNL m enc) =>
enc -> SoftFormula -> m (Sum, [(Lit, Constraint)])
addWBO enc
db SoftFormula
wbo = do
  forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ enc
db forall a b. (a -> b) -> a -> b
$ SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
wbo

  MutVar (PrimState m) Sum
objRef <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar []
  MutVar (PrimState m) Integer
objOffsetRef <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Integer
0
  MutVar (PrimState m) [(Lit, Constraint)]
defsRef <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar []
  MutVar (PrimState m) Lit
trueLitRef <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Lit
SAT.litUndef

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
wbo) forall a b. (a -> b) -> a -> b
$ \(Maybe Integer
cost, constr :: Constraint
constr@(Sum
lhs,Op
op,Integer
rhs)) -> do
    case Maybe Integer
cost of
      Maybe Integer
Nothing -> do
        case Op
op of
          Op
PBFile.Ge -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtLeast enc
db Sum
lhs Integer
rhs
          Op
PBFile.Eq -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly enc
db Sum
lhs Integer
rhs
        Lit
trueLit <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Lit
trueLitRef
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Lit
trueLit forall a. Eq a => a -> a -> Bool
== Lit
SAT.litUndef) forall a b. (a -> b) -> a -> b
$ do
          case Constraint -> Maybe Lit
detectTrueLit Constraint
constr of
            Maybe Lit
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just Lit
l -> forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar MutVar (PrimState m) Lit
trueLitRef Lit
l
      Just Integer
w -> do
        case Op
op of
          Op
PBFile.Ge -> do
            case Sum
lhs of
              [(Integer
c,[Lit]
ls)] | Integer
c forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& (Integer
rhs forall a. Num a => a -> a -> a
+ Integer
c forall a. Num a => a -> a -> a
- Integer
1) forall a. Integral a => a -> a -> a
`div` Integer
c forall a. Eq a => a -> a -> Bool
== Integer
1 -> do
                -- c ∧L ≥ rhs ⇔ ∧L ≥ ⌈rhs / c⌉
                -- ∧L ≥ 1 ⇔ ∧L
                -- obj += w * (1 - ∧L)
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Lit]
ls) forall a b. (a -> b) -> a -> b
$ do
                  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef (\Sum
obj -> (-Integer
w,[Lit]
ls) forall a. a -> [a] -> [a]
: Sum
obj)
                  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Integer
objOffsetRef (forall a. Num a => a -> a -> a
+ Integer
w)
              [(Integer
c,[Lit]
ls)] | Integer
c forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
&& (Integer
rhs forall a. Num a => a -> a -> a
+ forall a. Num a => a -> a
abs Integer
c forall a. Num a => a -> a -> a
- Integer
1) forall a. Integral a => a -> a -> a
`div` forall a. Num a => a -> a
abs Integer
c forall a. Num a => a -> a -> a
+ Integer
1 forall a. Eq a => a -> a -> Bool
== Integer
1 -> do
                -- c*∧L ≥ rhs ⇔ -1*∧L ≥ ⌈rhs / abs c⌉ ⇔ (1 - ∧L) ≥ ⌈rhs / abs c⌉ + 1 ⇔ ¬∧L ≥ ⌈rhs / abs c⌉ + 1
                -- ￢∧L ≥ 1 ⇔ ￢∧L
                -- obj += w * ∧L
                if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Lit]
ls then do
                  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Integer
objOffsetRef (forall a. Num a => a -> a -> a
+ Integer
w)
                else do
                  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w,[Lit]
ls) forall a. a -> [a] -> [a]
:)
              Sum
_ | Integer
rhs forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
c forall a. Ord a => a -> a -> Bool
>= Integer
rhs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Lit
length [Lit]
ls forall a. Eq a => a -> a -> Bool
== Lit
1 | (Integer
c,[Lit]
ls) <- Sum
lhs] -> do
                -- ∑L ≥ 1 ⇔ ∨L ⇔ ￢∧￢L
                -- obj += w * ∧￢L
                if forall (t :: * -> *) a. Foldable t => t a -> Bool
null Sum
lhs then do
                  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Integer
objOffsetRef (forall a. Num a => a -> a -> a
+ Integer
w)
                else do
                  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w, [-Lit
l | (Integer
_,[Lit
l]) <- Sum
lhs]) forall a. a -> [a] -> [a]
:)
              Sum
_ -> do
                Lit
sel <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar enc
db
                forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> Sum -> Integer -> m ()
SAT.addPBNLAtLeastSoft enc
db Lit
sel Sum
lhs Integer
rhs
                forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w,[-Lit
sel]) forall a. a -> [a] -> [a]
:)
                forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef ((Lit
sel,Constraint
constr) forall a. a -> [a] -> [a]
:)
          Op
PBFile.Eq -> do
            Lit
sel <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar enc
db
            forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> Sum -> Integer -> m ()
SAT.addPBNLExactlySoft enc
db Lit
sel Sum
lhs Integer
rhs
            forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w,[-Lit
sel]) forall a. a -> [a] -> [a]
:)
            forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef ((Lit
sel,Constraint
constr) forall a. a -> [a] -> [a]
:)

  Integer
offset <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Integer
objOffsetRef
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
offset forall a. Eq a => a -> a -> Bool
/= Integer
0) forall a b. (a -> b) -> a -> b
$ do
    Lit
l <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Lit
trueLitRef
    Lit
trueLit <-
      if Lit
l forall a. Eq a => a -> a -> Bool
/= Lit
SAT.litUndef then
        forall (m :: * -> *) a. Monad m => a -> m a
return Lit
l
      else do
        Lit
v <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar enc
db
        forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause enc
db [Lit
v]
        forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef ((Lit
v, ([], Op
PBFile.Ge, Integer
0)) forall a. a -> [a] -> [a]
:)
        forall (m :: * -> *) a. Monad m => a -> m a
return Lit
v
    forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
offset,[Lit
trueLit]) forall a. a -> [a] -> [a]
:)

  Sum
obj <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Sum
objRef
  [(Lit, Constraint)]
defs <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef

  case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
wbo of
    Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Integer
t -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtMost enc
db Sum
obj (Integer
t forall a. Num a => a -> a -> a
- Integer
1)

  forall (m :: * -> *) a. Monad m => a -> m a
return (Sum
obj, [(Lit, Constraint)]
defs)


detectTrueLit :: PBFile.Constraint -> Maybe SAT.Lit
detectTrueLit :: Constraint -> Maybe Lit
detectTrueLit (Sum
lhs, Op
op, Integer
rhs) =
  case Op
op of
    Op
PBFile.Ge -> forall {a} {a}. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f Sum
lhs Integer
rhs
    Op
PBFile.Eq -> forall {a} {a}. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f Sum
lhs Integer
rhs forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall {a} {a}. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f [(- Integer
c, [Lit]
ls) | (Integer
c,[Lit]
ls) <- Sum
lhs] (- Integer
rhs)
  where
    f :: [(a, [a])] -> a -> Maybe a
f [(a
c, [a
l])] a
rhs
      | a
c forall a. Ord a => a -> a -> Bool
> a
0 Bool -> Bool -> Bool
&& (a
rhs forall a. Num a => a -> a -> a
+ a
c forall a. Num a => a -> a -> a
- a
1) forall a. Integral a => a -> a -> a
`div` a
c forall a. Eq a => a -> a -> Bool
== a
1 =
          -- c l ≥ rhs ↔ l ≥ ⌈rhs / c⌉
          forall (m :: * -> *) a. Monad m => a -> m a
return a
l
      | a
c forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
&& a
rhs forall a. Integral a => a -> a -> a
`div` a
c forall a. Eq a => a -> a -> Bool
== a
0 =
          -- c l ≥ rhs ↔ l ≤ ⌊rhs / c⌋
          forall (m :: * -> *) a. Monad m => a -> m a
return (- a
l)
    f [(a, [a])]
_ a
_ = forall a. Maybe a
Nothing

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

type SAT2PBInfo = IdentityTransformer SAT.Model

sat2pb :: CNF.CNF -> (PBFile.Formula, SAT2PBInfo)
sat2pb :: CNF -> (Formula, PB2WBOInfo)
sat2pb CNF
cnf
  = ( PBFile.Formula
      { pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = forall a. Maybe a
Nothing
      , pbConstraints :: [Constraint]
PBFile.pbConstraints = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {c}.
(Num a, Num c) =>
PackedClause -> ([(a, [Lit])], Op, c)
f (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf)
      , pbNumVars :: Lit
PBFile.pbNumVars = CNF -> Lit
CNF.cnfNumVars CNF
cnf
      , pbNumConstraints :: Lit
PBFile.pbNumConstraints = CNF -> Lit
CNF.cnfNumClauses CNF
cnf
      }
    , forall a. IdentityTransformer a
IdentityTransformer
    )
  where
    f :: PackedClause -> ([(a, [Lit])], Op, c)
f PackedClause
clause = ([(a
1,[Lit
l]) | Lit
l <- PackedClause -> [Lit]
SAT.unpackClause PackedClause
clause], Op
PBFile.Ge, c
1)

type PB2SATInfo = TseitinInfo

-- | Convert a pseudo boolean formula φ to a equisatisfiable CNF formula ψ
-- together with two functions f and g such that:
--
-- * if M ⊨ φ then f(M) ⊨ ψ
--
-- * if M ⊨ ψ then g(M) ⊨ φ
--
pb2sat :: PBFile.Formula -> (CNF.CNF, PB2SATInfo)
pb2sat :: Formula -> (CNF, PBLinearizeInfo)
pb2sat Formula
formula = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  CNFStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  let nv1 :: Lit
nv1 = Formula -> Lit
PBFile.pbNumVars Formula
formula
  forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ CNFStore (ST s)
db Lit
nv1
  Encoder (ST s)
tseitin <-  forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder CNFStore (ST s)
db
  Encoder (ST s)
pb <- forall (m :: * -> *). Monad m => Encoder m -> m (Encoder m)
PB.newEncoder Encoder (ST s)
tseitin
  Encoder (ST s)
pbnlc <- forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder Encoder (ST s)
pb Encoder (ST s)
tseitin
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula) forall a b. (a -> b) -> a -> b
$ \(Sum
lhs,Op
op,Integer
rhs) -> do
    case Op
op of
      Op
PBFile.Ge -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtLeast Encoder (ST s)
pbnlc Sum
lhs Integer
rhs
      Op
PBFile.Eq -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly Encoder (ST s)
pbnlc Sum
lhs Integer
rhs
  CNF
cnf <- forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  [(Lit, Formula)]
defs <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  forall (m :: * -> *) a. Monad m => a -> m a
return (CNF
cnf, Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo Lit
nv1 (CNF -> Lit
CNF.cnfNumVars CNF
cnf) [(Lit, Formula)]
defs)

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

type MaxSAT2WBOInfo = IdentityTransformer SAT.Model

maxsat2wbo :: CNF.WCNF -> (PBFile.SoftFormula, MaxSAT2WBOInfo)
maxsat2wbo :: WCNF -> (SoftFormula, PB2WBOInfo)
maxsat2wbo
  CNF.WCNF
  { wcnfTopCost :: WCNF -> Integer
CNF.wcnfTopCost = Integer
top
  , wcnfClauses :: WCNF -> [WeightedClause]
CNF.wcnfClauses = [WeightedClause]
cs
  , wcnfNumVars :: WCNF -> Lit
CNF.wcnfNumVars = Lit
nv
  , wcnfNumClauses :: WCNF -> Lit
CNF.wcnfNumClauses = Lit
nc
  } =
  ( PBFile.SoftFormula
    { wboTopCost :: Maybe Integer
PBFile.wboTopCost = forall a. Maybe a
Nothing
    , wboConstraints :: [SoftConstraint]
PBFile.wboConstraints = forall a b. (a -> b) -> [a] -> [b]
map WeightedClause -> SoftConstraint
f [WeightedClause]
cs
    , wboNumVars :: Lit
PBFile.wboNumVars = Lit
nv
    , wboNumConstraints :: Lit
PBFile.wboNumConstraints = Lit
nc
    }
  , forall a. IdentityTransformer a
IdentityTransformer
  )
  where
    f :: WeightedClause -> SoftConstraint
f (Integer
w,PackedClause
c)
     | Integer
wforall a. Ord a => a -> a -> Bool
>=Integer
top    = (forall a. Maybe a
Nothing, Constraint
p) -- hard constraint
     | Bool
otherwise = (forall a. a -> Maybe a
Just Integer
w, Constraint
p)  -- soft constraint
     where
       p :: Constraint
p = ([(Integer
1,[Lit
l]) | Lit
l <- PackedClause -> [Lit]
SAT.unpackClause PackedClause
c], Op
PBFile.Ge, Integer
1)

type WBO2MaxSATInfo = TseitinInfo

wbo2maxsat :: PBFile.SoftFormula -> (CNF.WCNF, WBO2MaxSATInfo)
wbo2maxsat :: SoftFormula -> (WCNF, PBLinearizeInfo)
wbo2maxsat SoftFormula
formula = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  CNFStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ CNFStore (ST s)
db (SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
formula)
  Encoder (ST s)
tseitin <-  forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder CNFStore (ST s)
db
  Encoder (ST s)
pb <- forall (m :: * -> *). Monad m => Encoder m -> m (Encoder m)
PB.newEncoder Encoder (ST s)
tseitin
  Encoder (ST s)
pbnlc <- forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder Encoder (ST s)
pb Encoder (ST s)
tseitin

  Seq WeightedClause
softClauses <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula) forall a b. (a -> b) -> a -> b
$ \(Maybe Integer
cost, (Sum
lhs,Op
op,Integer
rhs)) -> do
    case Maybe Integer
cost of
      Maybe Integer
Nothing ->
        case Op
op of
          Op
PBFile.Ge -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtLeast Encoder (ST s)
pbnlc Sum
lhs Integer
rhs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
          Op
PBFile.Eq -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly Encoder (ST s)
pbnlc Sum
lhs Integer
rhs forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
      Just Integer
c -> do
        case Op
op of
          Op
PBFile.Ge -> do
            PBLinSum
lhs2 <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
Tseitin.polarityPos Sum
lhs
            let (PBLinSum
lhs3,Integer
rhs3) = (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinAtLeast (PBLinSum
lhs2,Integer
rhs)
            if Integer
rhs3forall a. Eq a => a -> a -> Bool
==Integer
1 Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
cforall a. Eq a => a -> a -> Bool
==Integer
1 | (Integer
c,Lit
_) <- PBLinSum
lhs3] then
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton (Integer
c, [Lit] -> PackedClause
SAT.packClause [Lit
l | (Integer
_,Lit
l) <- PBLinSum
lhs3])
            else do
              Lit
lit <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Lit
PB.encodePBLinAtLeast Encoder (ST s)
pb (PBLinSum
lhs3,Integer
rhs3)
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton (Integer
c, [Lit] -> PackedClause
SAT.packClause [Lit
lit])
          Op
PBFile.Eq -> do
            PBLinSum
lhs2 <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
Tseitin.polarityBoth Sum
lhs
            Lit
lit1 <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Lit
PB.encodePBLinAtLeast Encoder (ST s)
pb (PBLinSum
lhs2, Integer
rhs)
            Lit
lit2 <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Lit
PB.encodePBLinAtLeast Encoder (ST s)
pb ([(-Integer
c, Lit
l) | (Integer
c,Lit
l) <- PBLinSum
lhs2], forall a. Num a => a -> a
negate Integer
rhs)
            Lit
lit <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Lit] -> m Lit
Tseitin.encodeConjWithPolarity Encoder (ST s)
tseitin Polarity
Tseitin.polarityPos [Lit
lit1,Lit
lit2]
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton (Integer
c, [Lit] -> PackedClause
SAT.packClause [Lit
lit])

  case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula of
    Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Integer
top -> forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtMost Encoder (ST s)
pbnlc [(Integer
c, [-Lit
l | Lit
l <- PackedClause -> [Lit]
SAT.unpackClause PackedClause
clause]) | (Integer
c,PackedClause
clause) <- forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq WeightedClause
softClauses] (Integer
top forall a. Num a => a -> a -> a
- Integer
1)

  let top :: Integer
top = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
F.sum (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq WeightedClause
softClauses) forall a. Num a => a -> a -> a
+ Integer
1
  CNF
cnf <- forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  let cs :: Seq WeightedClause
cs = Seq WeightedClause
softClauses forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> Seq a
Seq.fromList [(Integer
top, PackedClause
clause) | PackedClause
clause <- CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf]
  let wcnf :: WCNF
wcnf = CNF.WCNF
             { wcnfNumVars :: Lit
CNF.wcnfNumVars = CNF -> Lit
CNF.cnfNumVars CNF
cnf
             , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = forall a. Seq a -> Lit
Seq.length Seq WeightedClause
cs
             , wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
top
             , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq WeightedClause
cs
             }
  [(Lit, Formula)]
defs <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  forall (m :: * -> *) a. Monad m => a -> m a
return (WCNF
wcnf, Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo (SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
formula) (CNF -> Lit
CNF.cnfNumVars CNF
cnf) [(Lit, Formula)]
defs)

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