{-# 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, (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 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) ->
      ( ( CNF.WCNF
          { wcnfNumVars :: Int
CNF.wcnfNumVars = Int
nv
          , wcnfNumClauses :: Int
CNF.wcnfNumClauses = Int
nc
          , wcnfTopCost :: Integer
CNF.wcnfTopCost = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Int
nc forall a. Num a => a -> a -> a
+ Int
1
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = 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 (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
ncforall a. Num a => a -> a -> a
+Int
1, (Integer
1,PackedClause
clause) forall a. a -> [a] -> [a]
: [WeightedClause]
cs, [(Int, (Int, Int, Int))]
ds, Integer
t)
        [Int
_a]     -> (Int
nv, Int
ncforall a. Num a => a -> a -> a
+Int
1, (Integer
1,PackedClause
clause) forall a. a -> [a] -> [a]
: [WeightedClause]
cs, [(Int, (Int, Int, Int))]
ds, Integer
t)
        [Int
_a, Int
_b] -> (Int
nv, Int
ncforall a. Num a => a -> a -> a
+Int
1, (Integer
1,PackedClause
clause) 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
nvforall 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
nvforall a. Num a => a -> a -> a
+Int
1, Int
nc forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cs2, forall a b. (a -> b) -> [a] -> [b]
map (\Clause
clause' -> (Integer
1, Clause -> PackedClause
SAT.packClause Clause
clause')) [Clause]
cs2 forall a. [a] -> [a] -> [a]
++ [WeightedClause]
cs, (Int
d, (Int
a,Int
b,Int
c)) forall a. a -> [a] -> [a]
: [(Int, (Int, Int, Int))]
ds, Integer
t forall a. Num a => a -> a -> a
+ Integer
3)
        Clause
_ -> 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
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]
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]
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 i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray forall a b. (a -> b) -> a -> b
$ do
    STUArray s Int Bool
m2 <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Int
1,Int
nv2)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
1..Int
nv1] forall a b. (a -> b) -> a -> b
$ \Int
v -> do
      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 (forall a. IModel a => a -> Int -> Bool
SAT.evalVar Source SAT3ToMaxSAT2Info
m Int
v)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Int, Int, Int)
ds) forall a b. (a -> b) -> a -> b
$ \(Int
d, (Int
a,Int
b,Int
c)) -> do
      let n :: Int
          n :: Int
n = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int
1 | Int
l <- [Int
a,Int
b,Int
c], forall a. IModel a => a -> Int -> Bool
SAT.evalLit Source SAT3ToMaxSAT2Info
m Int
l]
      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 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
    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, (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 forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {n}.
Integral n =>
(Int, Set (Int, Int), IntMap (Int, Int), n)
-> (n, PackedClause) -> (Int, Set (Int, Int), IntMap (Int, Int), n)
f (Int
nv1, forall a. Set a
Set.empty, 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), n)
-> (n, PackedClause) -> (Int, Set (Int, Int), IntMap (Int, Int), n)
f r :: (Int, Set (Int, Int), IntMap (Int, Int), n)
r@(Int
nv, Set (Int, Int)
cs, IntMap (Int, Int)
defs, n
t) (n
w, PackedClause
clause) =
      case PackedClause -> Clause
SAT.unpackClause PackedClause
clause of
        []    -> (Int
nv, Set (Int, Int)
cs, IntMap (Int, Int)
defs, n
tforall a. Num a => a -> a -> a
-n
w)
        [Int
a]   -> forall n a. Integral n => n -> (a -> a) -> a -> a
applyN n
w (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), n)
r
        [Int
a,Int
b] -> forall n a. Integral n => n -> (a -> a) -> a -> a
applyN n
w (forall {d}.
(Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
-> (Int, Set (Int, Int), IntMap (Int, Int), d)
insert (forall a. Ord a => a -> a -> a
min Int
a Int
b, forall a. Ord a => a -> a -> a
max Int
a Int
b)) (Int, Set (Int, Int), IntMap (Int, Int), n)
r
        Clause
_ -> 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 forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Int, Int)
cs = (Int
v, forall a. Ord a => a -> Set a -> Set a
Set.insert (Int
a,Int
v) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert (Int
b,-Int
v) Set (Int, Int)
cs, 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, 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 forall a. Num a => a -> a -> a
+ Int
1

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

data SimplifyMaxSAT2Info
  = SimplifyMaxSAT2Info !Int !Int (IntMap (SAT.Lit, SAT.Lit))
  deriving (SimplifyMaxSAT2Info -> SimplifyMaxSAT2Info -> Bool
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]
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]
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 =
    forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1,Int
nv2) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source SimplifyMaxSAT2Info
m forall a. [a] -> [a] -> [a]
++ [(Int
v, if forall a. IModel a => a -> Int -> Bool
SAT.evalLit Source SimplifyMaxSAT2Info
m Int
a then Bool
False else Bool
True) | (Int
v,(Int
a,Int
_b)) <- 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 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) =
  ( ( forall a.
(a -> a -> a) -> Int -> [(Int, Int, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdgesWith forall a. Num a => a -> a -> a
(+) Int
numNodes [(Int
a,Int
b,Integer
1) | (Int
a,Int
b) <- ([(Int, Int)]
basicFramework forall a. [a] -> [a] -> [a]
++ [(Int, Int)]
additionalEdges)]
    , Integer
w
    )
  , Int -> Int -> SimpleMaxSAT2ToSimpleMaxCutInfo
SimpleMaxSAT2ToSimpleMaxCutInfo Int
n Int
p
  )
  where
    p :: Int
p = 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
3forall a. Num a => a -> a -> a
*Int
p], Int
j <- [Int
0..Int
3forall a. Num a => a -> a -> a
*Int
p]] 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
3forall a. Num a => a -> a -> a
*Int
p]] 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
3forall a. Num a => a -> a -> a
*Int
p]] 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
3forall a. Num a => a -> a -> a
*Int
p]]
    sizeOfBasicFramework :: Int
sizeOfBasicFramework = (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1)forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Int
3 forall a. Num a => a -> a -> a
* Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall 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) <- forall a. Set a -> [a]
Set.toList Set (Int, Int)
cs, Int
a forall a. Eq a => a -> a -> Bool
/= Int
b ] forall a. [a] -> [a] -> [a]
++
      [ (Int -> Int
l Int
a, Int -> Int
ff (Int
2forall a. Num a => a -> a -> a
*Int
iforall a. Num a => a -> a -> a
-Int
1)) | (Int
i, (Int
a,Int
_b)) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] (forall a. Set a -> [a]
Set.toList Set (Int, Int)
cs) ] forall a. [a] -> [a] -> [a]
++
      [ (Int -> Int
l Int
b, Int -> Int
ff (Int
2forall a. Num a => a -> a -> a
*Int
i  )) | (Int
i, (Int
_a,Int
b)) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] (forall a. Set a -> [a]
Set.toList Set (Int, Int)
cs) ]

    k :: Integer
k = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Set a -> Int
Set.size Set (Int, Int)
cs) forall a. Num a => a -> a -> a
- Integer
threshold
    w :: Integer
w = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
sizeOfBasicFramework forall a. Num a => a -> a -> a
+ Integer
2forall 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, 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
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
n forall a. Num a => a -> a -> a
+ Int
n
    tt :: p -> p
tt p
i  =                                                 p
i
    ff :: Int -> Int
ff Int
i  = (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+                                       Int
i
    t :: Int -> Int -> Int
t Int
i Int
j = (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+                             (Int
iforall a. Num a => a -> a -> a
-Int
1)forall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
j
    f :: Int -> Int -> Int
f Int
i Int
j = (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+                 (Int
iforall a. Num a => a -> a -> a
-Int
1)forall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
j
    xp :: Int -> Int
xp Int
i  = (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+     (Int
iforall a. Num a => a -> a -> a
-Int
1)
    xn :: Int -> Int
xn Int
i  = (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ (Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
nforall a. Num a => a -> a -> a
*(Int
3forall a. Num a => a -> a -> a
*Int
pforall a. Num a => a -> a -> a
+Int
1) forall a. Num a => a -> a -> a
+ Int
n forall a. Num a => a -> a -> a
+ (Int
iforall a. Num a => a -> a -> a
-Int
1)
    l :: Int -> Int
l Int
x   = if Int
x 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
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]
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]
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 =
    forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
0,Int
numNodesforall 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
numNodesforall 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 forall a b. (a -> b) -> a -> b
$
           [Int -> Int
ff Int
i  | Int
i <- [Int
0..Int
3forall a. Num a => a -> a -> a
*Int
p]] forall a. [a] -> [a] -> [a]
++
           [Int -> Int
xp Int
i  | Int
i <- [Int
1..Int
n], Bool -> Bool
not (forall a. IModel a => a -> Int -> Bool
SAT.evalVar Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i)] forall a. [a] -> [a] -> [a]
++
           [Int -> Int -> Int
t Int
i Int
j | Int
i <- [Int
1..Int
n], Bool -> Bool
not (forall a. IModel a => a -> Int -> Bool
SAT.evalVar Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i), Int
j <- [Int
0..Int
3forall a. Num a => a -> a -> a
*Int
p]] forall a. [a] -> [a] -> [a]
++
           [Int -> Int
xn Int
i  | Int
i <- [Int
1..Int
n], forall a. IModel a => a -> Int -> Bool
SAT.evalVar Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i] forall a. [a] -> [a] -> [a]
++
           [Int -> Int -> Int
f Int
i Int
j | Int
i <- [Int
1..Int
n], forall a. IModel a => a -> Int -> Bool
SAT.evalVar Source SimpleMaxSAT2ToSimpleMaxCutInfo
m Int
i, Int
j <- [Int
0..Int
3forall 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 forall a. Eq a => a -> a -> Bool
== Int
0    = 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 = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1,Int
n) [(Int
i, (Target SimpleMaxSAT2ToSimpleMaxCutInfo
sol forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int -> Int
xp Int
i) 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 (Target SimpleMaxSAT2ToSimpleMaxCutInfo
sol 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, (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

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