{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.SAT2MaxSAT
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * M. R. Garey, D. S. Johnson, and L. Stockmeyer. Some simplified NP-complete
--   problems. In STOC ’74: Proceedings of the sixth annual ACM symposium on Theory
--   of computing, pages 47–63, New York, NY, USA, 1974.
--   https://dl.acm.org/citation.cfm?doid=800119.803884
--   https://www.sciencedirect.com/science/article/pii/0304397576900591
--
-----------------------------------------------------------------------------
module ToySolver.Converter.SAT2MaxSAT
  (
  -- * SAT to Max-2-SAT conversion
    SATToMaxSAT2Info
  , satToMaxSAT2

  -- * Max-2-SAT to simple Max-Cut conversion
  , MaxSAT2ToSimpleMaxCutInfo
  , maxSAT2ToSimpleMaxCut

  -- * SAT to simple Max-Cut conversion
  , SATToSimpleMaxCutInfo
  , satToSimpleMaxCut

  -- * Low-level conversion

  -- ** 3-SAT to Max-2-SAT conversion
  , SAT3ToMaxSAT2Info (..)
  , sat3ToMaxSAT2

  -- ** Max-2-SAT to SimpleMaxSAT2 conversion
  , SimpleMaxSAT2
  , SimplifyMaxSAT2Info (..)
  , simplifyMaxSAT2

  -- ** SimpleMaxSAT2 to simple Max-Cut conversion
  , SimpleMaxSAT2ToSimpleMaxCutInfo (..)
  , simpleMaxSAT2ToSimpleMaxCut
  ) where

import Control.Monad
import Data.Array.MArray
import Data.Array.ST
import Data.Array.Unboxed
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.List hiding (insert)
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Converter.Base
import ToySolver.Converter.SAT2KSAT
import ToySolver.Graph.Base
import qualified ToySolver.Graph.MaxCut as MaxCut
import qualified ToySolver.SAT.Types as SAT

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

type SATToMaxSAT2Info = ComposedTransformer SAT2KSATInfo SAT3ToMaxSAT2Info

satToMaxSAT2 :: CNF.CNF -> ((CNF.WCNF, Integer), SATToMaxSAT2Info)
satToMaxSAT2 :: CNF -> ((WCNF, Integer), SATToMaxSAT2Info)
satToMaxSAT2 CNF
x = ((WCNF, Integer)
x2, (SAT2KSATInfo -> SAT3ToMaxSAT2Info -> SATToMaxSAT2Info
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2KSATInfo
info1 SAT3ToMaxSAT2Info
info2))
  where
    (CNF
x1, SAT2KSATInfo
info1) = Int -> CNF -> (CNF, SAT2KSATInfo)
sat2ksat Int
3 CNF
x
    ((WCNF, Integer)
x2, SAT3ToMaxSAT2Info
info2) = CNF -> ((WCNF, Integer), SAT3ToMaxSAT2Info)
sat3ToMaxSAT2 CNF
x1


sat3ToMaxSAT2 :: CNF.CNF -> ((CNF.WCNF, Integer), SAT3ToMaxSAT2Info)
sat3ToMaxSAT2 :: CNF -> ((WCNF, Integer), SAT3ToMaxSAT2Info)
sat3ToMaxSAT2 CNF
cnf =
  case ((Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
 -> PackedClause
 -> (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer))
-> (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
-> [PackedClause]
-> (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
-> PackedClause
-> (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
f (CNF -> Int
CNF.cnfNumVars CNF
cnf, Int
0, [], [], Integer
0) (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) of
    (!Int
nv, !Int
nc, ![WeightedClause]
cs, [(Int, (Int, Int, Int))]
ds, !Integer
t) ->
      ( ( WCNF :: Int -> Int -> Integer -> [WeightedClause] -> WCNF
CNF.WCNF
          { wcnfNumVars :: Int
CNF.wcnfNumVars = Int
nv
          , wcnfNumClauses :: Int
CNF.wcnfNumClauses = Int
nc
          , wcnfTopCost :: Integer
CNF.wcnfTopCost = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int
nc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [WeightedClause] -> [WeightedClause]
forall a. [a] -> [a]
reverse [WeightedClause]
cs
          }
        , Integer
t
        )
      , Int -> Int -> IntMap (Int, Int, Int) -> SAT3ToMaxSAT2Info
SAT3ToMaxSAT2Info (CNF -> Int
CNF.cnfNumVars CNF
cnf) Int
nv ([(Int, (Int, Int, Int))] -> IntMap (Int, Int, Int)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, (Int, Int, Int))]
ds)
      )
  where
    f :: (Int, Int, [CNF.WeightedClause], [(SAT.Var,(SAT.Lit,SAT.Lit,SAT.Lit))], Integer)
      -> SAT.PackedClause
      -> (Int, Int, [CNF.WeightedClause], [(SAT.Var,(SAT.Lit,SAT.Lit,SAT.Lit))], Integer)
    f :: (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
-> PackedClause
-> (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
f (!Int
nv, !Int
nc, [WeightedClause]
cs, [(Int, (Int, Int, Int))]
ds, Integer
t) PackedClause
clause =
      case PackedClause -> Clause
SAT.unpackClause PackedClause
clause of
        []       -> (Int
nv, Int
ncInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, (Integer
1,PackedClause
clause) WeightedClause -> [WeightedClause] -> [WeightedClause]
forall a. a -> [a] -> [a]
: [WeightedClause]
cs, [(Int, (Int, Int, Int))]
ds, Integer
t)
        [Int
_a]     -> (Int
nv, Int
ncInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, (Integer
1,PackedClause
clause) WeightedClause -> [WeightedClause] -> [WeightedClause]
forall a. a -> [a] -> [a]
: [WeightedClause]
cs, [(Int, (Int, Int, Int))]
ds, Integer
t)
        [Int
_a, Int
_b] -> (Int
nv, Int
ncInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, (Integer
1,PackedClause
clause) WeightedClause -> [WeightedClause] -> [WeightedClause]
forall a. a -> [a] -> [a]
: [WeightedClause]
cs, [(Int, (Int, Int, Int))]
ds, Integer
t)
        [Int
a, Int
b, Int
c] ->
          let d :: Int
d = Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
              cs2 :: [Clause]
cs2 = [[Int
a], [Int
b], [Int
c], [Int
d], [-Int
a,-Int
b], [-Int
a,-Int
c], [-Int
b,-Int
c], [Int
a,-Int
d], [Int
b,-Int
d], [Int
c,-Int
d]]
          in (Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, Int
nc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Clause] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cs2, (Clause -> WeightedClause) -> [Clause] -> [WeightedClause]
forall a b. (a -> b) -> [a] -> [b]
map (\Clause
clause' -> (Integer
1, Clause -> PackedClause
SAT.packClause Clause
clause')) [Clause]
cs2 [WeightedClause] -> [WeightedClause] -> [WeightedClause]
forall a. [a] -> [a] -> [a]
++ [WeightedClause]
cs, (Int
d, (Int
a,Int
b,Int
c)) (Int, (Int, Int, Int))
-> [(Int, (Int, Int, Int))] -> [(Int, (Int, Int, Int))]
forall a. a -> [a] -> [a]
: [(Int, (Int, Int, Int))]
ds, Integer
t Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
3)
        Clause
_ -> [Char]
-> (Int, Int, [WeightedClause], [(Int, (Int, Int, Int))], Integer)
forall a. HasCallStack => [Char] -> a
error [Char]
"not a 3-SAT instance"

data SAT3ToMaxSAT2Info = SAT3ToMaxSAT2Info !Int !Int (IntMap (SAT.Lit,SAT.Lit,SAT.Lit))
  deriving (SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool
(SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool)
-> (SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool)
-> Eq SAT3ToMaxSAT2Info
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool
$c/= :: SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool
== :: SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool
$c== :: SAT3ToMaxSAT2Info -> SAT3ToMaxSAT2Info -> Bool
Eq, Int -> SAT3ToMaxSAT2Info -> ShowS
[SAT3ToMaxSAT2Info] -> ShowS
SAT3ToMaxSAT2Info -> [Char]
(Int -> SAT3ToMaxSAT2Info -> ShowS)
-> (SAT3ToMaxSAT2Info -> [Char])
-> ([SAT3ToMaxSAT2Info] -> ShowS)
-> Show SAT3ToMaxSAT2Info
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SAT3ToMaxSAT2Info] -> ShowS
$cshowList :: [SAT3ToMaxSAT2Info] -> ShowS
show :: SAT3ToMaxSAT2Info -> [Char]
$cshow :: SAT3ToMaxSAT2Info -> [Char]
showsPrec :: Int -> SAT3ToMaxSAT2Info -> ShowS
$cshowsPrec :: Int -> SAT3ToMaxSAT2Info -> ShowS
Show, ReadPrec [SAT3ToMaxSAT2Info]
ReadPrec SAT3ToMaxSAT2Info
Int -> ReadS SAT3ToMaxSAT2Info
ReadS [SAT3ToMaxSAT2Info]
(Int -> ReadS SAT3ToMaxSAT2Info)
-> ReadS [SAT3ToMaxSAT2Info]
-> ReadPrec SAT3ToMaxSAT2Info
-> ReadPrec [SAT3ToMaxSAT2Info]
-> Read SAT3ToMaxSAT2Info
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SAT3ToMaxSAT2Info]
$creadListPrec :: ReadPrec [SAT3ToMaxSAT2Info]
readPrec :: ReadPrec SAT3ToMaxSAT2Info
$creadPrec :: ReadPrec SAT3ToMaxSAT2Info
readList :: ReadS [SAT3ToMaxSAT2Info]
$creadList :: ReadS [SAT3ToMaxSAT2Info]
readsPrec :: Int -> ReadS SAT3ToMaxSAT2Info
$creadsPrec :: Int -> ReadS SAT3ToMaxSAT2Info
Read)

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

instance ForwardTransformer SAT3ToMaxSAT2Info where
  transformForward :: SAT3ToMaxSAT2Info
-> Source SAT3ToMaxSAT2Info -> Target SAT3ToMaxSAT2Info
transformForward (SAT3ToMaxSAT2Info Int
nv1 Int
nv2 IntMap (Int, Int, Int)
ds) Source SAT3ToMaxSAT2Info
m = (forall s. ST s (STUArray s Int Bool)) -> UArray Int Bool
forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray ((forall s. ST s (STUArray s Int Bool)) -> UArray Int Bool)
-> (forall s. ST s (STUArray s Int Bool)) -> UArray Int Bool
forall a b. (a -> b) -> a -> b
$ do
    STUArray s Int Bool
m2 <- (Int, Int) -> ST s (STUArray s Int Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Int
1,Int
nv2)
    Clause -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
1..Int
nv1] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
v -> do
      STUArray s Int Bool -> Int -> Bool -> ST s ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Bool
m2 Int
v (UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar UArray Int Bool
Source SAT3ToMaxSAT2Info
m Int
v)
    [(Int, (Int, Int, Int))]
-> ((Int, (Int, Int, Int)) -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap (Int, Int, Int) -> [(Int, (Int, Int, Int))]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Int, Int, Int)
ds) (((Int, (Int, Int, Int)) -> ST s ()) -> ST s ())
-> ((Int, (Int, Int, Int)) -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Int
d, (Int
a,Int
b,Int
c)) -> do
      let n :: Int
          n :: Int
n = Clause -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int
1 | Int
l <- [Int
a,Int
b,Int
c], UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalLit UArray Int Bool
Source SAT3ToMaxSAT2Info
m Int
l]
      STUArray s Int Bool -> Int -> Bool -> ST s ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Bool
m2 Int
d (Bool -> ST s ()) -> Bool -> ST s ()
forall a b. (a -> b) -> a -> b
$
        case Int
n of
          Int
1 -> Bool
False
          Int
2 -> Bool
False -- True is also OK
          Int
3 -> Bool
True
          Int
_ -> Bool
False -- precondition is violated
    STUArray s Int Bool -> ST s (STUArray s Int Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Bool
m2

instance BackwardTransformer SAT3ToMaxSAT2Info where
  transformBackward :: SAT3ToMaxSAT2Info
-> Target SAT3ToMaxSAT2Info -> Source SAT3ToMaxSAT2Info
transformBackward (SAT3ToMaxSAT2Info Int
nv1 Int
_nv2 IntMap (Int, Int, Int)
_ds) = Int -> UArray Int Bool -> UArray Int Bool
SAT.restrictModel Int
nv1

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

type MaxSAT2ToSimpleMaxCutInfo = ComposedTransformer SimplifyMaxSAT2Info SimpleMaxSAT2ToSimpleMaxCutInfo

maxSAT2ToSimpleMaxCut :: (CNF.WCNF, Integer) -> ((MaxCut.Problem Integer, Integer), MaxSAT2ToSimpleMaxCutInfo)
maxSAT2ToSimpleMaxCut :: (WCNF, Integer)
-> ((Problem Integer, Integer), MaxSAT2ToSimpleMaxCutInfo)
maxSAT2ToSimpleMaxCut (WCNF, Integer)
x = ((Problem Integer, Integer)
x2, (SimplifyMaxSAT2Info
-> SimpleMaxSAT2ToSimpleMaxCutInfo -> MaxSAT2ToSimpleMaxCutInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SimplifyMaxSAT2Info
info1 SimpleMaxSAT2ToSimpleMaxCutInfo
info2))
  where
    (SimpleMaxSAT2
x1, SimplifyMaxSAT2Info
info1) = (WCNF, Integer) -> (SimpleMaxSAT2, SimplifyMaxSAT2Info)
simplifyMaxSAT2 (WCNF, Integer)
x
    ((Problem Integer, Integer)
x2, SimpleMaxSAT2ToSimpleMaxCutInfo
info2) = SimpleMaxSAT2
-> ((Problem Integer, Integer), SimpleMaxSAT2ToSimpleMaxCutInfo)
simpleMaxSAT2ToSimpleMaxCut SimpleMaxSAT2
x1

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

type SimpleMaxSAT2 = (Int, Set (Int, Int), Integer)

simplifyMaxSAT2 :: (CNF.WCNF, Integer) -> (SimpleMaxSAT2, SimplifyMaxSAT2Info)
simplifyMaxSAT2 :: (WCNF, Integer) -> (SimpleMaxSAT2, SimplifyMaxSAT2Info)
simplifyMaxSAT2 (WCNF
wcnf, Integer
threshold) =
  case ((Int, Set (Int, Int), IntMap (Int, Int), Integer)
 -> WeightedClause
 -> (Int, Set (Int, Int), IntMap (Int, Int), Integer))
-> (Int, Set (Int, Int), IntMap (Int, Int), Integer)
-> [WeightedClause]
-> (Int, Set (Int, Int), IntMap (Int, Int), Integer)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Set (Int, Int), IntMap (Int, Int), Integer)
-> WeightedClause
-> (Int, Set (Int, Int), IntMap (Int, Int), Integer)
forall d.
Integral d =>
(Int, Set (Int, Int), IntMap (Int, Int), d)
-> (d, PackedClause) -> (Int, Set (Int, Int), IntMap (Int, Int), d)
f (Int
nv1, Set (Int, Int)
forall a. Set a
Set.empty, IntMap (Int, Int)
forall a. IntMap a
IntMap.empty, Integer
threshold) (WCNF -> [WeightedClause]
CNF.wcnfClauses WCNF
wcnf) of
    (Int
nv2, Set (Int, Int)
cs, IntMap (Int, Int)
defs, Integer
threshold2) -> ((Int
nv2, Set (Int, Int)
cs, Integer
threshold2), Int -> Int -> IntMap (Int, Int) -> SimplifyMaxSAT2Info
SimplifyMaxSAT2Info Int
nv1 Int
nv2 IntMap (Int, Int)
defs)
  where
    nv1 :: Int
nv1 = WCNF -> Int
CNF.wcnfNumVars WCNF
wcnf
    f :: (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (d, PackedClause) -> (Int, Set (Int, Int), IntMap (Int, Int), d)
f r :: (Int, Set (Int, Int), IntMap (Int, Int), d)
r@(Int
nv, Set (Int, Int)
cs, IntMap (Int, Int)
defs, d
t) (d
w, PackedClause
clause) =
      case PackedClause -> Clause
SAT.unpackClause PackedClause
clause of
        []    -> (Int
nv, Set (Int, Int)
cs, IntMap (Int, Int)
defs, d
td -> d -> d
forall a. Num a => a -> a -> a
-d
w)
        [Int
a]   -> d
-> ((Int, Set (Int, Int), IntMap (Int, Int), d)
    -> (Int, Set (Int, Int), IntMap (Int, Int), d))
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
forall n a. Integral n => n -> (a -> a) -> a -> a
applyN d
w ((Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
forall d.
(Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
insert (Int
a,Int
a)) (Int, Set (Int, Int), IntMap (Int, Int), d)
r
        [Int
a,Int
b] -> d
-> ((Int, Set (Int, Int), IntMap (Int, Int), d)
    -> (Int, Set (Int, Int), IntMap (Int, Int), d))
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
forall n a. Integral n => n -> (a -> a) -> a -> a
applyN d
w ((Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
forall d.
(Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
insert (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
a Int
b, Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
a Int
b)) (Int, Set (Int, Int), IntMap (Int, Int), d)
r
        Clause
_ -> [Char] -> (Int, Set (Int, Int), IntMap (Int, Int), d)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
    insert :: (Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
insert c :: (Int, Int)
c@(Int
a,Int
b) (Int
nv,Set (Int, Int)
cs,IntMap (Int, Int)
defs,d
t)
      | (Int, Int)
c (Int, Int) -> Set (Int, Int) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Int, Int)
cs = (Int
v, (Int, Int) -> Set (Int, Int) -> Set (Int, Int)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int
a,Int
v) (Set (Int, Int) -> Set (Int, Int))
-> Set (Int, Int) -> Set (Int, Int)
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Set (Int, Int) -> Set (Int, Int)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int
b,-Int
v) Set (Int, Int)
cs, Int -> (Int, Int) -> IntMap (Int, Int) -> IntMap (Int, Int)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (Int
a,Int
b) IntMap (Int, Int)
defs, d
t)
      | Bool
otherwise         = (Int
nv, (Int, Int) -> Set (Int, Int) -> Set (Int, Int)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int, Int)
c Set (Int, Int)
cs, IntMap (Int, Int)
defs, d
t)
      where
        v :: Int
v = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

applyN :: Integral n => n -> (a -> a) -> (a -> a)
applyN :: n -> (a -> a) -> a -> a
applyN n
n a -> a
f = Endo a -> a -> a
forall a. Endo a -> a -> a
appEndo (Endo a -> a -> a) -> Endo a -> a -> a
forall a b. (a -> b) -> a -> b
$ [Endo a] -> Endo a
forall a. Monoid a => [a] -> a
mconcat ([Endo a] -> Endo a) -> [Endo a] -> Endo a
forall a b. (a -> b) -> a -> b
$ n -> Endo a -> [Endo a]
forall i a. Integral i => i -> a -> [a]
genericReplicate n
n ((a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo a -> a
f)

data SimplifyMaxSAT2Info
  = SimplifyMaxSAT2Info !Int !Int (IntMap (SAT.Lit, SAT.Lit))
  deriving (SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool
(SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool)
-> (SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool)
-> Eq SimplifyMaxSAT2Info
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool
$c/= :: SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool
== :: SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool
$c== :: SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool
Eq, Int -> SimplifyMaxSAT2Info -> ShowS
[SimplifyMaxSAT2Info] -> ShowS
SimplifyMaxSAT2Info -> [Char]
(Int -> SimplifyMaxSAT2Info -> ShowS)
-> (SimplifyMaxSAT2Info -> [Char])
-> ([SimplifyMaxSAT2Info] -> ShowS)
-> Show SimplifyMaxSAT2Info
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SimplifyMaxSAT2Info] -> ShowS
$cshowList :: [SimplifyMaxSAT2Info] -> ShowS
show :: SimplifyMaxSAT2Info -> [Char]
$cshow :: SimplifyMaxSAT2Info -> [Char]
showsPrec :: Int -> SimplifyMaxSAT2Info -> ShowS
$cshowsPrec :: Int -> SimplifyMaxSAT2Info -> ShowS
Show, ReadPrec [SimplifyMaxSAT2Info]
ReadPrec SimplifyMaxSAT2Info
Int -> ReadS SimplifyMaxSAT2Info
ReadS [SimplifyMaxSAT2Info]
(Int -> ReadS SimplifyMaxSAT2Info)
-> ReadS [SimplifyMaxSAT2Info]
-> ReadPrec SimplifyMaxSAT2Info
-> ReadPrec [SimplifyMaxSAT2Info]
-> Read SimplifyMaxSAT2Info
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SimplifyMaxSAT2Info]
$creadListPrec :: ReadPrec [SimplifyMaxSAT2Info]
readPrec :: ReadPrec SimplifyMaxSAT2Info
$creadPrec :: ReadPrec SimplifyMaxSAT2Info
readList :: ReadS [SimplifyMaxSAT2Info]
$creadList :: ReadS [SimplifyMaxSAT2Info]
readsPrec :: Int -> ReadS SimplifyMaxSAT2Info
$creadsPrec :: Int -> ReadS SimplifyMaxSAT2Info
Read)

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

instance ForwardTransformer SimplifyMaxSAT2Info where
  transformForward :: SimplifyMaxSAT2Info
-> Source SimplifyMaxSAT2Info -> Target SimplifyMaxSAT2Info
transformForward (SimplifyMaxSAT2Info Int
_nv1 Int
nv2 IntMap (Int, Int)
defs) Source SimplifyMaxSAT2Info
m =
    (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1,Int
nv2) ([(Int, Bool)] -> UArray Int Bool)
-> [(Int, Bool)] -> UArray Int Bool
forall a b. (a -> b) -> a -> b
$ UArray Int Bool -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Int Bool
Source SimplifyMaxSAT2Info
m [(Int, Bool)] -> [(Int, Bool)] -> [(Int, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Int
v, if UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalLit UArray Int Bool
Source SimplifyMaxSAT2Info
m Int
a then Bool
False else Bool
True) | (Int
v,(Int
a,Int
_b)) <- IntMap (Int, Int) -> [(Int, (Int, Int))]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Int, Int)
defs]

instance BackwardTransformer SimplifyMaxSAT2Info where
  transformBackward :: SimplifyMaxSAT2Info
-> Target SimplifyMaxSAT2Info -> Source SimplifyMaxSAT2Info
transformBackward (SimplifyMaxSAT2Info Int
nv1 Int
_nv2 IntMap (Int, Int)
_defs) Target SimplifyMaxSAT2Info
m = Int -> UArray Int Bool -> UArray Int Bool
SAT.restrictModel Int
nv1 UArray Int Bool
Target SimplifyMaxSAT2Info
m

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

simpleMaxSAT2ToSimpleMaxCut
  :: SimpleMaxSAT2
  -> ( (MaxCut.Problem Integer, Integer)
     , SimpleMaxSAT2ToSimpleMaxCutInfo
     )
simpleMaxSAT2ToSimpleMaxCut :: SimpleMaxSAT2
-> ((Problem Integer, Integer), SimpleMaxSAT2ToSimpleMaxCutInfo)
simpleMaxSAT2ToSimpleMaxCut (Int
n, Set (Int, Int)
cs, Integer
threshold) =
  ( ( (Integer -> Integer -> Integer)
-> Int -> [(Int, Int, Integer)] -> Problem Integer
forall a.
(a -> a -> a) -> Int -> [(Int, Int, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdgesWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Int
numNodes [(Int
a,Int
b,Integer
1) | (Int
a,Int
b) <- ([(Int, Int)]
basicFramework [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a] -> [a]
++ [(Int, Int)]
additionalEdges)]
    , Integer
w
    )
  , Int -> Int -> SimpleMaxSAT2ToSimpleMaxCutInfo
SimpleMaxSAT2ToSimpleMaxCutInfo Int
n Int
p
  )
  where
    p :: Int
p = Set (Int, Int) -> Int
forall a. Set a -> Int
Set.size Set (Int, Int)
cs
    (Int
numNodes, Int -> Int
tt, Int -> Int
ff, Int -> Int -> Int
t, Int -> Int -> Int
f ,Int -> Int
xp, Int -> Int
xn, Int -> Int
l) = Int
-> Int
-> (Int, Int -> Int, Int -> Int, Int -> Int -> Int,
    Int -> Int -> Int, Int -> Int, Int -> Int, Int -> Int)
simpleMaxSAT2ToSimpleMaxCutNodes Int
n Int
p

    basicFramework :: [(Int, Int)]
basicFramework =
      [(Int -> Int
tt Int
i, Int -> Int
ff Int
j)   | Int
i <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p], Int
j <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p]] [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a] -> [a]
++
      [(Int -> Int -> Int
t Int
i Int
j, Int -> Int -> Int
f Int
i Int
j) | Int
i <- [Int
1..Int
n],   Int
j <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p]] [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a] -> [a]
++
      [(Int -> Int
xp Int
i,  Int -> Int -> Int
f Int
i Int
j) | Int
i <- [Int
1..Int
n],   Int
j <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p]] [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a] -> [a]
++
      [(Int -> Int
xn Int
i,  Int -> Int -> Int
t Int
i Int
j) | Int
i <- [Int
1..Int
n],   Int
j <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p]]
    sizeOfBasicFramework :: Int
sizeOfBasicFramework = (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

    additionalEdges :: [(Int, Int)]
additionalEdges =
      [ (Int -> Int
l Int
a, Int -> Int
l Int
b) | (Int
a,Int
b) <- Set (Int, Int) -> [(Int, Int)]
forall a. Set a -> [a]
Set.toList Set (Int, Int)
cs, Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
b ] [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a] -> [a]
++
      [ (Int -> Int
l Int
a, Int -> Int
ff (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) | (Int
i, (Int
a,Int
_b)) <- Clause -> [(Int, Int)] -> [(Int, (Int, Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] (Set (Int, Int) -> [(Int, Int)]
forall a. Set a -> [a]
Set.toList Set (Int, Int)
cs) ] [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a] -> [a]
++
      [ (Int -> Int
l Int
b, Int -> Int
ff (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
i  )) | (Int
i, (Int
_a,Int
b)) <- Clause -> [(Int, Int)] -> [(Int, (Int, Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] (Set (Int, Int) -> [(Int, Int)]
forall a. Set a -> [a]
Set.toList Set (Int, Int)
cs) ]

    k :: Integer
k = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set (Int, Int) -> Int
forall a. Set a -> Int
Set.size Set (Int, Int)
cs) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
threshold
    w :: Integer
w = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
sizeOfBasicFramework Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
k


simpleMaxSAT2ToSimpleMaxCutNodes
  :: Int -> Int
  -> ( Int
     , Int -> Int
     , Int -> Int
     , SAT.Var -> Int -> Int
     , SAT.Var -> Int -> Int
     , SAT.Var -> Int
     , SAT.Var -> Int
     , SAT.Lit -> Int
     )
simpleMaxSAT2ToSimpleMaxCutNodes :: Int
-> Int
-> (Int, Int -> Int, Int -> Int, Int -> Int -> Int,
    Int -> Int -> Int, Int -> Int, Int -> Int, Int -> Int)
simpleMaxSAT2ToSimpleMaxCutNodes Int
n Int
p = (Int
numNodes, Int -> Int
forall p. p -> p
tt, Int -> Int
ff, Int -> Int -> Int
t, Int -> Int -> Int
f ,Int -> Int
xp, Int -> Int
xn, Int -> Int
l)
  where
    numNodes :: Int
numNodes = (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
    tt :: p -> p
tt p
i  =                                                 p
i
    ff :: Int -> Int
ff Int
i  = (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+                                       Int
i
    t :: Int -> Int -> Int
t Int
i Int
j = (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+                             (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)Int -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j
    f :: Int -> Int -> Int
f Int
i Int
j = (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+                 (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)Int -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j
    xp :: Int -> Int
xp Int
i  = (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+     (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
    xn :: Int -> Int
xn Int
i  = (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*(Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
pInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
    l :: Int -> Int
l Int
x   = if Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Int -> Int
xp Int
x else Int -> Int
xn (- Int
x)


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

instance Transformer SimpleMaxSAT2ToSimpleMaxCutInfo where
  type Source SimpleMaxSAT2ToSimpleMaxCutInfo = SAT.Model
  type Target SimpleMaxSAT2ToSimpleMaxCutInfo = MaxCut.Solution

instance ForwardTransformer SimpleMaxSAT2ToSimpleMaxCutInfo where
  transformForward :: SimpleMaxSAT2ToSimpleMaxCutInfo
-> Source SimpleMaxSAT2ToSimpleMaxCutInfo
-> Target SimpleMaxSAT2ToSimpleMaxCutInfo
transformForward (SimpleMaxSAT2ToSimpleMaxCutInfo Int
n Int
p) Source SimpleMaxSAT2ToSimpleMaxCutInfo
m =
    (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
0,Int
numNodesInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [(Int
v, Bool -> Bool
not (Int
v Int -> IntSet -> Bool
`IntSet.member` IntSet
s1)) | Int
v <- [Int
0..Int
numNodesInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
    where
      (Int
numNodes, Int -> Int
_tt, Int -> Int
ff, Int -> Int -> Int
t, Int -> Int -> Int
f ,Int -> Int
xp, Int -> Int
xn, Int -> Int
_l) = Int
-> Int
-> (Int, Int -> Int, Int -> Int, Int -> Int -> Int,
    Int -> Int -> Int, Int -> Int, Int -> Int, Int -> Int)
simpleMaxSAT2ToSimpleMaxCutNodes Int
n Int
p
      s1 :: IntSet
s1 = Clause -> IntSet
IntSet.fromList (Clause -> IntSet) -> Clause -> IntSet
forall a b. (a -> b) -> a -> b
$
           [Int -> Int
ff Int
i  | Int
i <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p]] Clause -> Clause -> Clause
forall a. [a] -> [a] -> [a]
++
           [Int -> Int
xp Int
i  | Int
i <- [Int
1..Int
n], Bool -> Bool
not (UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar UArray Int Bool
Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i)] Clause -> Clause -> Clause
forall a. [a] -> [a] -> [a]
++
           [Int -> Int -> Int
t Int
i Int
j | Int
i <- [Int
1..Int
n], Bool -> Bool
not (UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar UArray Int Bool
Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i), Int
j <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p]] Clause -> Clause -> Clause
forall a. [a] -> [a] -> [a]
++
           [Int -> Int
xn Int
i  | Int
i <- [Int
1..Int
n], UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar UArray Int Bool
Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i] Clause -> Clause -> Clause
forall a. [a] -> [a] -> [a]
++
           [Int -> Int -> Int
f Int
i Int
j | Int
i <- [Int
1..Int
n], UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar UArray Int Bool
Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i, Int
j <- [Int
0..Int
3Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
p]]

instance BackwardTransformer SimpleMaxSAT2ToSimpleMaxCutInfo where
  transformBackward :: SimpleMaxSAT2ToSimpleMaxCutInfo
-> Target SimpleMaxSAT2ToSimpleMaxCutInfo
-> Source SimpleMaxSAT2ToSimpleMaxCutInfo
transformBackward (SimpleMaxSAT2ToSimpleMaxCutInfo Int
n Int
p) Target SimpleMaxSAT2ToSimpleMaxCutInfo
sol
    | Int
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1,Int
n) [(Int
i, Bool
False) | Int
i <- [Int
1..Int
n]]
    | Bool
otherwise = (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1,Int
n) [(Int
i, (UArray Int Bool
Target SimpleMaxSAT2ToSimpleMaxCutInfo
sol UArray Int Bool -> Int -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int -> Int
xp Int
i) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b) | Int
i <- [Int
1..Int
n]]
    where
      (Int
_numNodes, Int -> Int
_tt, Int -> Int
ff, Int -> Int -> Int
_t, Int -> Int -> Int
_f ,Int -> Int
xp, Int -> Int
_xn, Int -> Int
_l) = Int
-> Int
-> (Int, Int -> Int, Int -> Int, Int -> Int -> Int,
    Int -> Int -> Int, Int -> Int, Int -> Int, Int -> Int)
simpleMaxSAT2ToSimpleMaxCutNodes Int
n Int
p
      b :: Bool
b = Bool -> Bool
not (UArray Int Bool
Target SimpleMaxSAT2ToSimpleMaxCutInfo
sol UArray Int Bool -> Int -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int -> Int
ff Int
0)

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

type SATToSimpleMaxCutInfo = ComposedTransformer SATToMaxSAT2Info MaxSAT2ToSimpleMaxCutInfo

satToSimpleMaxCut :: CNF.CNF -> ((MaxCut.Problem Integer, Integer), SATToSimpleMaxCutInfo)
satToSimpleMaxCut :: CNF -> ((Problem Integer, Integer), SATToSimpleMaxCutInfo)
satToSimpleMaxCut CNF
x = ((Problem Integer, Integer)
x2, (SATToMaxSAT2Info
-> MaxSAT2ToSimpleMaxCutInfo -> SATToSimpleMaxCutInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SATToMaxSAT2Info
info1 MaxSAT2ToSimpleMaxCutInfo
info2))
  where
    ((WCNF, Integer)
x1, SATToMaxSAT2Info
info1) = CNF -> ((WCNF, Integer), SATToMaxSAT2Info)
satToMaxSAT2 CNF
x
    ((Problem Integer, Integer)
x2, MaxSAT2ToSimpleMaxCutInfo
info2) = (WCNF, Integer)
-> ((Problem Integer, Integer), MaxSAT2ToSimpleMaxCutInfo)
maxSAT2ToSimpleMaxCut (WCNF, Integer)
x1

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