{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.SAT2MaxCut
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- http://www.cs.cornell.edu/courses/cs4820/2014sp/notes/reduction-maxcut.pdf
--
-----------------------------------------------------------------------------
module ToySolver.Converter.SAT2MaxCut
  (
  -- * SAT to MaxCut conversion
    SAT2MaxCutInfo
  , sat2maxcut

  -- * Low-level conversion

  -- ** NAE-SAT to MaxCut
  , NAESAT2MaxCutInfo
  , naesat2maxcut

  -- ** NAE-3-SAT to MaxCut
  , NAE3SAT2MaxCutInfo (..)
  , nae3sat2maxcut
  ) where

import qualified Data.Aeson as J
import Data.Aeson ((.=))
import Data.Array.Unboxed
import qualified Data.IntSet as IntSet
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU

import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Graph.Base
import qualified ToySolver.Graph.MaxCut as MaxCut
import ToySolver.Internal.JSON (withTypedObject)
import qualified ToySolver.SAT.Types as SAT
import ToySolver.Converter.Base
import ToySolver.Converter.NAESAT (NAESAT)
import qualified ToySolver.Converter.NAESAT as NAESAT

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

type SAT2MaxCutInfo = ComposedTransformer NAESAT.SAT2NAESATInfo NAESAT2MaxCutInfo

sat2maxcut :: CNF.CNF -> ((MaxCut.Problem Integer, Integer), SAT2MaxCutInfo)
sat2maxcut :: CNF -> ((Problem Integer, Integer), SAT2MaxCutInfo)
sat2maxcut CNF
x = ((Problem Integer, Integer)
x2, (SAT2NAESATInfo -> NAESAT2MaxCutInfo -> SAT2MaxCutInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2NAESATInfo
info1 NAESAT2MaxCutInfo
info2))
  where
    (NAESAT
x1, SAT2NAESATInfo
info1) = CNF -> (NAESAT, SAT2NAESATInfo)
NAESAT.sat2naesat CNF
x
    ((Problem Integer, Integer)
x2, NAESAT2MaxCutInfo
info2) = NAESAT -> ((Problem Integer, Integer), NAESAT2MaxCutInfo)
naesat2maxcut NAESAT
x1

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

type NAESAT2MaxCutInfo = ComposedTransformer NAESAT.NAESAT2NAEKSATInfo NAE3SAT2MaxCutInfo

naesat2maxcut :: NAESAT -> ((MaxCut.Problem Integer, Integer), NAESAT2MaxCutInfo)
naesat2maxcut :: NAESAT -> ((Problem Integer, Integer), NAESAT2MaxCutInfo)
naesat2maxcut NAESAT
x = ((Problem Integer, Integer)
x2, (NAESAT2NAEKSATInfo -> NAE3SAT2MaxCutInfo -> NAESAT2MaxCutInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer NAESAT2NAEKSATInfo
info1 NAE3SAT2MaxCutInfo
info2))
  where
    (NAESAT
x1, NAESAT2NAEKSATInfo
info1) = Lit -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
NAESAT.naesat2naeksat Lit
3 NAESAT
x
    ((Problem Integer, Integer)
x2, NAE3SAT2MaxCutInfo
info2) = NAESAT -> ((Problem Integer, Integer), NAE3SAT2MaxCutInfo)
nae3sat2maxcut NAESAT
x1

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

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

-- Original nae-sat problem is satisfiable iff Max-Cut problem has solution with >=threshold.
nae3sat2maxcut :: NAESAT -> ((MaxCut.Problem Integer, Integer), NAE3SAT2MaxCutInfo)
nae3sat2maxcut :: NAESAT -> ((Problem Integer, Integer), NAE3SAT2MaxCutInfo)
nae3sat2maxcut (Lit
n,[NAEClause]
cs)
  | (Vector Lit -> Bool) -> [Vector Lit] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Vector Lit
c -> Vector Lit -> Lit
forall (v :: * -> *) a. Vector v a => v a -> Lit
VG.length Vector Lit
c Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
< Lit
2) [Vector Lit]
cs' =
      ( (Lit -> [Edge Integer] -> Problem Integer
forall a. HasCallStack => Lit -> [Edge a] -> EdgeLabeledGraph a
graphFromUnorderedEdges (Lit
nLit -> Lit -> Lit
forall a. Num a => a -> a -> a
*Lit
2) [], Integer
1)
      , NAE3SAT2MaxCutInfo
NAE3SAT2MaxCutInfo
      )
  | Bool
otherwise =
      ( ( (Integer -> Integer -> Integer)
-> Lit -> [Edge Integer] -> Problem Integer
forall a.
HasCallStack =>
(a -> a -> a) -> Lit -> [Edge a] -> EdgeLabeledGraph a
graphFromUnorderedEdgesWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Lit
nLit -> Lit -> Lit
forall a. Num a => a -> a -> a
*Lit
2) ([Edge Integer]
variableEdges [Edge Integer] -> [Edge Integer] -> [Edge Integer]
forall a. [a] -> [a] -> [a]
++ [Edge Integer]
clauseEdges)
        , Integer
bigM Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Lit -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
clauseEdgesObjMax
        )
      , NAE3SAT2MaxCutInfo
NAE3SAT2MaxCutInfo
      )
  where
    cs' :: [Vector Lit]
cs' = (NAEClause -> Vector Lit) -> [NAEClause] -> [Vector Lit]
forall a b. (a -> b) -> [a] -> [b]
map ([Lit] -> Vector Lit
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Lit] -> Vector Lit)
-> (NAEClause -> [Lit]) -> NAEClause -> Vector Lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Lit]
IntSet.toList (IntSet -> [Lit]) -> (NAEClause -> IntSet) -> NAEClause -> [Lit]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Lit] -> IntSet
IntSet.fromList ([Lit] -> IntSet) -> (NAEClause -> [Lit]) -> NAEClause -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAEClause -> [Lit]
SAT.unpackClause) [NAEClause]
cs

    bigM :: Integer
bigM = Integer
clauseEdgesObjMax Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1

    ([Edge Integer]
clauseEdges, Integer
clauseEdgesObjMax) = (([Edge Integer], Integer)
 -> Vector Lit -> ([Edge Integer], Integer))
-> ([Edge Integer], Integer)
-> [Vector Lit]
-> ([Edge Integer], Integer)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([Edge Integer], Integer)
-> Vector Lit -> ([Edge Integer], Integer)
f ([],Integer
0) [Vector Lit]
cs'
      where
        f :: ([(Int,Int,Integer)], Integer) -> VU.Vector SAT.Lit -> ([(Int,Int,Integer)], Integer)
        f :: ([Edge Integer], Integer)
-> Vector Lit -> ([Edge Integer], Integer)
f ([Edge Integer]
clauseEdges', !Integer
clauseEdgesObjMax') Vector Lit
c =
          case (Lit -> Lit) -> [Lit] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Lit
encodeLit (Vector Lit -> [Lit]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Lit
c) of
            []  -> String -> ([Edge Integer], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2maxcut: should not happen"
            [Lit
_] -> String -> ([Edge Integer], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2maxcut: should not happen"
            [Lit
v0,Lit
v1]    -> ([(Lit
v0, Lit
v1, Integer
1)] [Edge Integer] -> [Edge Integer] -> [Edge Integer]
forall a. [a] -> [a] -> [a]
++ [Edge Integer]
clauseEdges', Integer
clauseEdgesObjMax' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
            [Lit
v0,Lit
v1,Lit
v2] -> ([(Lit
v0, Lit
v1, Integer
1), (Lit
v1, Lit
v2, Integer
1), (Lit
v2, Lit
v0, Integer
1)] [Edge Integer] -> [Edge Integer] -> [Edge Integer]
forall a. [a] -> [a] -> [a]
++ [Edge Integer]
clauseEdges', Integer
clauseEdgesObjMax' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2)
            [Lit]
_ -> String -> ([Edge Integer], Integer)
forall a. HasCallStack => String -> a
error String
"nae3sat2maxcut: cannot handle nae-clause of size >3"

    variableEdges :: [Edge Integer]
variableEdges = [(Lit -> Lit
encodeLit Lit
v, Lit -> Lit
encodeLit (-Lit
v), Integer
bigM) | Lit
v <- [Lit
1..Lit
n]]

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

instance ForwardTransformer NAE3SAT2MaxCutInfo where
  transformForward :: NAE3SAT2MaxCutInfo
-> Source NAE3SAT2MaxCutInfo -> Target NAE3SAT2MaxCutInfo
transformForward NAE3SAT2MaxCutInfo
_ Source NAE3SAT2MaxCutInfo
m = (Lit, Lit) -> [(Lit, Bool)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
0,Lit
2Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
*Lit
nLit -> Lit -> Lit
forall a. Num a => a -> a -> a
-Lit
1) ([(Lit, Bool)] -> Model) -> [(Lit, Bool)] -> Model
forall a b. (a -> b) -> a -> b
$ do
    Lit
v <- [Lit
1..Lit
n]
    let val :: Bool
val = Model -> Lit -> Bool
forall a. IModel a => a -> Lit -> Bool
SAT.evalVar Model
Source NAE3SAT2MaxCutInfo
m Lit
v
    [(Lit -> Lit
encodeLit Lit
v, Bool
val), (Lit -> Lit
encodeLit (-Lit
v), Bool -> Bool
not Bool
val)]
    where
      (Lit
_,Lit
n) = Model -> (Lit, Lit)
forall i. Ix i => UArray i Bool -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Model
Source NAE3SAT2MaxCutInfo
m

instance BackwardTransformer NAE3SAT2MaxCutInfo where
  transformBackward :: NAE3SAT2MaxCutInfo
-> Target NAE3SAT2MaxCutInfo -> Source NAE3SAT2MaxCutInfo
transformBackward NAE3SAT2MaxCutInfo
_ Target NAE3SAT2MaxCutInfo
sol = (Lit, Lit) -> [(Lit, Bool)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1,Lit
n) [(Lit
v, Model
Target NAE3SAT2MaxCutInfo
sol Model -> Lit -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Lit -> Lit
encodeLit Lit
v) | Lit
v <- [Lit
1..Lit
n]]
    where
      (Lit
_,Lit
n') = Model -> (Lit, Lit)
forall i. Ix i => UArray i Bool -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Model
Target NAE3SAT2MaxCutInfo
sol
      n :: Lit
n = (Lit
n'Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+Lit
1) Lit -> Lit -> Lit
forall a. Integral a => a -> a -> a
`div` Lit
2

instance J.ToJSON NAE3SAT2MaxCutInfo where
  toJSON :: NAE3SAT2MaxCutInfo -> Value
toJSON NAE3SAT2MaxCutInfo
_ =
    [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
"NAE3SAT2MaxCutInfo" :: J.Value)
    ]

instance J.FromJSON NAE3SAT2MaxCutInfo where
  parseJSON :: Value -> Parser NAE3SAT2MaxCutInfo
parseJSON = String
-> (Object -> Parser NAE3SAT2MaxCutInfo)
-> Value
-> Parser NAE3SAT2MaxCutInfo
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withTypedObject String
"NAE3SAT2MaxCutInfo" ((Object -> Parser NAE3SAT2MaxCutInfo)
 -> Value -> Parser NAE3SAT2MaxCutInfo)
-> (Object -> Parser NAE3SAT2MaxCutInfo)
-> Value
-> Parser NAE3SAT2MaxCutInfo
forall a b. (a -> b) -> a -> b
$ \Object
_ -> NAE3SAT2MaxCutInfo -> Parser NAE3SAT2MaxCutInfo
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NAE3SAT2MaxCutInfo
NAE3SAT2MaxCutInfo

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

encodeLit :: SAT.Lit -> Int
encodeLit :: Lit -> Lit
encodeLit Lit
l =
  if Lit
l Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
> Lit
0
  then (Lit
lLit -> Lit -> Lit
forall a. Num a => a -> a -> a
-Lit
1)Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
*Lit
2
  else (-Lit
lLit -> Lit -> Lit
forall a. Num a => a -> a -> a
-Lit
1)Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
*Lit
2Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+Lit
1

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