{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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 qualified Data.Aeson as J
import Data.Aeson ((.=), (.:))
import Data.Array.Unboxed
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.Converter.Tseitin
import ToySolver.Graph.Base
import qualified ToySolver.Graph.MaxCut as MaxCut
import ToySolver.Internal.JSON (withTypedObject)
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Formula 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 -> SAT2KSATInfo -> SATToMaxSAT2Info
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2KSATInfo
info1 SAT2KSATInfo
info2))
  where
    (CNF
x1, SAT2KSATInfo
info1) = Int -> CNF -> (CNF, SAT2KSATInfo)
sat2ksat Int
3 CNF
x
    ((WCNF, Integer)
x2, SAT2KSATInfo
info2) = CNF -> ((WCNF, Integer), SAT2KSATInfo)
sat3ToMaxSAT2 CNF
x1


sat3ToMaxSAT2 :: CNF.CNF -> ((CNF.WCNF, Integer), SAT3ToMaxSAT2Info)
sat3ToMaxSAT2 :: CNF -> ((WCNF, Integer), SAT2KSATInfo)
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 b a. (b -> a -> b) -> b -> [a] -> b
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 = 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 -> VarMap Formula -> SAT2KSATInfo
TseitinInfo (CNF -> Int
CNF.cnfNumVars CNF
cnf) Int
nv (VarMap Formula -> SAT2KSATInfo) -> VarMap Formula -> SAT2KSATInfo
forall a b. (a -> b) -> a -> b
$ [(Int, Formula)] -> VarMap Formula
forall a. [(Int, a)] -> IntMap a
IntMap.fromList
          [ (Int
d, [Formula] -> Formula
SAT.And [Int -> Formula
atom Int
a, Int -> Formula
atom Int
b, Int -> Formula
atom Int
c])
            -- we define d as "a && b && c", but "a + b + c >= 2" is also fine.
          | (Int
d, (Int
a,Int
b,Int
c)) <- [(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 a. [a] -> 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"

    atom :: SAT.Lit -> SAT.Formula
    atom :: Int -> Formula
atom Int
l
      | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Formula -> Formula
SAT.Not (Int -> Formula
SAT.Atom (- Int
l))
      | Bool
otherwise = Int -> Formula
SAT.Atom Int
l


type SAT3ToMaxSAT2Info = TseitinInfo

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

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, (SAT2KSATInfo
-> SimpleMaxSAT2ToSimpleMaxCutInfo -> MaxSAT2ToSimpleMaxCutInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2KSATInfo
info1 SimpleMaxSAT2ToSimpleMaxCutInfo
info2))
  where
    (SimpleMaxSAT2
x1, SAT2KSATInfo
info1) = (WCNF, Integer) -> (SimpleMaxSAT2, SAT2KSATInfo)
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, SAT2KSATInfo)
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 b a. (b -> a -> b) -> b -> [a] -> b
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 {n}.
Integral n =>
(Int, Set (Int, Int), IntMap (Int, Int), n)
-> (n, PackedClause) -> (Int, Set (Int, Int), IntMap (Int, Int), n)
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 -> VarMap Formula -> SAT2KSATInfo
TseitinInfo Int
nv1 Int
nv2 (((Int, Int) -> Formula) -> IntMap (Int, Int) -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
a, Int
_b) -> Int -> Formula
atom (- Int
a)) IntMap (Int, Int)
defs)
        -- we deine v as "~a" but "~b" is also fine.
      )
  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
tn -> n -> n
forall a. Num a => a -> a -> a
-n
w)
        [Int
a]   -> n
-> ((Int, Set (Int, Int), IntMap (Int, Int), n)
    -> (Int, Set (Int, Int), IntMap (Int, Int), n))
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
forall n a. Integral n => n -> (a -> a) -> a -> a
applyN n
w ((Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
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] -> n
-> ((Int, Set (Int, Int), IntMap (Int, Int), n)
    -> (Int, Set (Int, Int), IntMap (Int, Int), n))
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
forall n a. Integral n => n -> (a -> a) -> a -> a
applyN n
w ((Int, Int)
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
-> (Int, Set (Int, Int), IntMap (Int, Int), n)
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), n)
r
        Clause
_ -> [Char] -> (Int, Set (Int, Int), IntMap (Int, Int), n)
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

    atom :: SAT.Lit -> SAT.Formula
    atom :: Int -> Formula
atom Int
l
      | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Formula -> Formula
SAT.Not (Int -> Formula
SAT.Atom (- Int
l))
      | Bool
otherwise = Int -> Formula
SAT.Atom Int
l

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 = 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)

type SimplifyMaxSAT2Info = TseitinInfo

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

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 -> [Edge Integer] -> Problem Integer
forall a.
HasCallStack =>
(a -> a -> a) -> Int -> [Edge 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
$c== :: SimpleMaxSAT2ToSimpleMaxCutInfo
-> SimpleMaxSAT2ToSimpleMaxCutInfo -> Bool
== :: SimpleMaxSAT2ToSimpleMaxCutInfo
-> SimpleMaxSAT2ToSimpleMaxCutInfo -> Bool
$c/= :: SimpleMaxSAT2ToSimpleMaxCutInfo
-> SimpleMaxSAT2ToSimpleMaxCutInfo -> Bool
/= :: 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
$cshowsPrec :: Int -> SimpleMaxSAT2ToSimpleMaxCutInfo -> ShowS
showsPrec :: Int -> SimpleMaxSAT2ToSimpleMaxCutInfo -> ShowS
$cshow :: SimpleMaxSAT2ToSimpleMaxCutInfo -> [Char]
show :: SimpleMaxSAT2ToSimpleMaxCutInfo -> [Char]
$cshowList :: [SimpleMaxSAT2ToSimpleMaxCutInfo] -> ShowS
showList :: [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
$creadsPrec :: Int -> ReadS SimpleMaxSAT2ToSimpleMaxCutInfo
readsPrec :: Int -> ReadS SimpleMaxSAT2ToSimpleMaxCutInfo
$creadList :: ReadS [SimpleMaxSAT2ToSimpleMaxCutInfo]
readList :: ReadS [SimpleMaxSAT2ToSimpleMaxCutInfo]
$creadPrec :: ReadPrec SimpleMaxSAT2ToSimpleMaxCutInfo
readPrec :: ReadPrec SimpleMaxSAT2ToSimpleMaxCutInfo
$creadListPrec :: ReadPrec [SimpleMaxSAT2ToSimpleMaxCutInfo]
readListPrec :: ReadPrec [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)] -> Model
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 (Model -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar Model
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 (Model -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar Model
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], Model -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar Model
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], Model -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar Model
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)] -> Model
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)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1,Int
n) [(Int
i, (Model
Target SimpleMaxSAT2ToSimpleMaxCutInfo
sol Model -> 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 (Model
Target SimpleMaxSAT2ToSimpleMaxCutInfo
sol Model -> Int -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int -> Int
ff Int
0)

instance J.ToJSON SimpleMaxSAT2ToSimpleMaxCutInfo where
  toJSON :: SimpleMaxSAT2ToSimpleMaxCutInfo -> Value
toJSON (SimpleMaxSAT2ToSimpleMaxCutInfo Int
n Int
p) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"SimpleMaxSAT2ToSimpleMaxCutInfo" :: J.Value)
    , Key
"num_original_variables" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
n
    , Key
"num_transformed_nodes" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
p
    ]

instance J.FromJSON SimpleMaxSAT2ToSimpleMaxCutInfo where
  parseJSON :: Value -> Parser SimpleMaxSAT2ToSimpleMaxCutInfo
parseJSON =
    [Char]
-> (Object -> Parser SimpleMaxSAT2ToSimpleMaxCutInfo)
-> Value
-> Parser SimpleMaxSAT2ToSimpleMaxCutInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"SimpleMaxSAT2ToSimpleMaxCutInfo" ((Object -> Parser SimpleMaxSAT2ToSimpleMaxCutInfo)
 -> Value -> Parser SimpleMaxSAT2ToSimpleMaxCutInfo)
-> (Object -> Parser SimpleMaxSAT2ToSimpleMaxCutInfo)
-> Value
-> Parser SimpleMaxSAT2ToSimpleMaxCutInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
      Int -> Int -> SimpleMaxSAT2ToSimpleMaxCutInfo
SimpleMaxSAT2ToSimpleMaxCutInfo
        (Int -> Int -> SimpleMaxSAT2ToSimpleMaxCutInfo)
-> Parser Int -> Parser (Int -> SimpleMaxSAT2ToSimpleMaxCutInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"
        Parser (Int -> SimpleMaxSAT2ToSimpleMaxCutInfo)
-> Parser Int -> Parser SimpleMaxSAT2ToSimpleMaxCutInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_transformed_nodes"

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

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

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