{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.NAESAT
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Not-All-Equal SAT problems.
--
-----------------------------------------------------------------------------
module ToySolver.Converter.NAESAT
  (
  -- * Definition of NAE (Not-All-Equall) SAT problems.
    NAESAT
  , evalNAESAT
  , NAEClause
  , evalNAEClause

  -- * Conversion with SAT problem
  , SAT2NAESATInfo (..)
  , sat2naesat
  , NAESAT2SATInfo
  , naesat2sat

  -- * Conversion from general NAE-SAT to NAE-k-SAT
  , NAESAT2NAEKSATInfo (..)
  , naesat2naeksat

  -- ** NAE-SAT to MAX-2-SAT
  , NAESAT2Max2SATInfo
  , naesat2max2sat
  , NAE3SAT2Max2SATInfo
  , nae3sat2max2sat
  ) where

import Control.Monad.State.Strict
import Data.Array.Unboxed
import qualified Data.IntMap as IntMap
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU
import ToySolver.Converter.Base
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

type NAESAT = (Int, [NAEClause])

evalNAESAT :: SAT.IModel m => m -> NAESAT -> Bool
evalNAESAT :: forall m. IModel m => m -> NAESAT -> Bool
evalNAESAT m
m (Lit
_,[NAEClause]
cs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall m. IModel m => m -> NAEClause -> Bool
evalNAEClause m
m) [NAEClause]
cs

type NAEClause = VU.Vector SAT.PackedLit

evalNAEClause :: SAT.IModel m => m -> NAEClause -> Bool
evalNAEClause :: forall m. IModel m => m -> NAEClause -> Bool
evalNAEClause m
m NAEClause
c =
  forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.any (forall m. IModel m => m -> Lit -> Bool
SAT.evalLit m
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Lit
SAT.unpackLit) NAEClause
c Bool -> Bool -> Bool
&& forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. IModel m => m -> Lit -> Bool
SAT.evalLit m
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Lit
SAT.unpackLit) NAEClause
c

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

-- | Information of 'sat2naesat' conversion
newtype SAT2NAESATInfo = SAT2NAESATInfo SAT.Var
  deriving (SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
$c/= :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
== :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
$c== :: SAT2NAESATInfo -> SAT2NAESATInfo -> Bool
Eq, Lit -> SAT2NAESATInfo -> ShowS
[SAT2NAESATInfo] -> ShowS
SAT2NAESATInfo -> String
forall a.
(Lit -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SAT2NAESATInfo] -> ShowS
$cshowList :: [SAT2NAESATInfo] -> ShowS
show :: SAT2NAESATInfo -> String
$cshow :: SAT2NAESATInfo -> String
showsPrec :: Lit -> SAT2NAESATInfo -> ShowS
$cshowsPrec :: Lit -> SAT2NAESATInfo -> ShowS
Show, ReadPrec [SAT2NAESATInfo]
ReadPrec SAT2NAESATInfo
Lit -> ReadS SAT2NAESATInfo
ReadS [SAT2NAESATInfo]
forall a.
(Lit -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SAT2NAESATInfo]
$creadListPrec :: ReadPrec [SAT2NAESATInfo]
readPrec :: ReadPrec SAT2NAESATInfo
$creadPrec :: ReadPrec SAT2NAESATInfo
readList :: ReadS [SAT2NAESATInfo]
$creadList :: ReadS [SAT2NAESATInfo]
readsPrec :: Lit -> ReadS SAT2NAESATInfo
$creadsPrec :: Lit -> ReadS SAT2NAESATInfo
Read)

-- | Convert a CNF formula φ to an equisatifiable NAE-SAT formula ψ,
-- together with a 'SAT2NAESATInfo'
sat2naesat :: CNF.CNF -> (NAESAT, SAT2NAESATInfo)
sat2naesat :: CNF -> (NAESAT, SAT2NAESATInfo)
sat2naesat CNF
cnf = (NAESAT
ret, Lit -> SAT2NAESATInfo
SAT2NAESATInfo Lit
z)
  where
    z :: Lit
z = CNF -> Lit
CNF.cnfNumVars CNF
cnf forall a. Num a => a -> a -> a
+ Lit
1
    ret :: NAESAT
ret =
      ( CNF -> Lit
CNF.cnfNumVars CNF
cnf forall a. Num a => a -> a -> a
+ Lit
1
      , [forall (v :: * -> *) a. Vector v a => v a -> a -> v a
VG.snoc NAEClause
clause (Lit -> PackedLit
SAT.packLit Lit
z) | NAEClause
clause <- CNF -> [NAEClause]
CNF.cnfClauses CNF
cnf]
      )

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

instance ForwardTransformer SAT2NAESATInfo where
  transformForward :: SAT2NAESATInfo -> Source SAT2NAESATInfo -> Target SAT2NAESATInfo
transformForward (SAT2NAESATInfo Lit
z) Source SAT2NAESATInfo
m = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1,Lit
z) forall a b. (a -> b) -> a -> b
$ (Lit
z,Bool
False) forall a. a -> [a] -> [a]
: forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source SAT2NAESATInfo
m

instance BackwardTransformer SAT2NAESATInfo where
  transformBackward :: SAT2NAESATInfo -> Target SAT2NAESATInfo -> Source SAT2NAESATInfo
transformBackward (SAT2NAESATInfo Lit
z) Target SAT2NAESATInfo
m =
    Lit -> UArray Lit Bool -> UArray Lit Bool
SAT.restrictModel (Lit
z forall a. Num a => a -> a -> a
- Lit
1) forall a b. (a -> b) -> a -> b
$
      if forall m. IModel m => m -> Lit -> Bool
SAT.evalVar Target SAT2NAESATInfo
m Lit
z then forall (a :: * -> * -> *) e' e i.
(IArray a e', IArray a e, Ix i) =>
(e' -> e) -> a i e' -> a i e
amap Bool -> Bool
not Target SAT2NAESATInfo
m else Target SAT2NAESATInfo
m

-- | Information of 'naesat2sat' conversion
type NAESAT2SATInfo = IdentityTransformer SAT.Model

-- | Convert a NAE-SAT formula φ to an equisatifiable CNF formula ψ,
-- together with a 'NAESAT2SATInfo'
naesat2sat :: NAESAT -> (CNF.CNF, NAESAT2SATInfo)
naesat2sat :: NAESAT -> (CNF, NAESAT2SATInfo)
naesat2sat (Lit
n,[NAEClause]
cs) =
  ( CNF.CNF
    { cnfNumVars :: Lit
CNF.cnfNumVars = Lit
n
    , cnfNumClauses :: Lit
CNF.cnfNumClauses = forall (t :: * -> *) a. Foldable t => t a -> Lit
length [NAEClause]
cs forall a. Num a => a -> a -> a
* Lit
2
    , cnfClauses :: [NAEClause]
CNF.cnfClauses = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[NAEClause
c, forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map forall a. Num a => a -> a
negate NAEClause
c] | NAEClause
c <- [NAEClause]
cs]
    }
  , forall a. IdentityTransformer a
IdentityTransformer
  )

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

-- Information of 'naesat2naeksta' conversion
data NAESAT2NAEKSATInfo = NAESAT2NAEKSATInfo !Int !Int [(SAT.Var, NAEClause, NAEClause)]
  deriving (NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
$c/= :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
== :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
$c== :: NAESAT2NAEKSATInfo -> NAESAT2NAEKSATInfo -> Bool
Eq, Lit -> NAESAT2NAEKSATInfo -> ShowS
[NAESAT2NAEKSATInfo] -> ShowS
NAESAT2NAEKSATInfo -> String
forall a.
(Lit -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NAESAT2NAEKSATInfo] -> ShowS
$cshowList :: [NAESAT2NAEKSATInfo] -> ShowS
show :: NAESAT2NAEKSATInfo -> String
$cshow :: NAESAT2NAEKSATInfo -> String
showsPrec :: Lit -> NAESAT2NAEKSATInfo -> ShowS
$cshowsPrec :: Lit -> NAESAT2NAEKSATInfo -> ShowS
Show, ReadPrec [NAESAT2NAEKSATInfo]
ReadPrec NAESAT2NAEKSATInfo
Lit -> ReadS NAESAT2NAEKSATInfo
ReadS [NAESAT2NAEKSATInfo]
forall a.
(Lit -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [NAESAT2NAEKSATInfo]
$creadListPrec :: ReadPrec [NAESAT2NAEKSATInfo]
readPrec :: ReadPrec NAESAT2NAEKSATInfo
$creadPrec :: ReadPrec NAESAT2NAEKSATInfo
readList :: ReadS [NAESAT2NAEKSATInfo]
$creadList :: ReadS [NAESAT2NAEKSATInfo]
readsPrec :: Lit -> ReadS NAESAT2NAEKSATInfo
$creadsPrec :: Lit -> ReadS NAESAT2NAEKSATInfo
Read)

naesat2naeksat :: Int -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat :: Lit -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat Lit
k NAESAT
_ | Lit
k forall a. Ord a => a -> a -> Bool
< Lit
3 = forall a. HasCallStack => String -> a
error String
"naesat2naeksat: k must be >=3"
naesat2naeksat Lit
k (Lit
n,[NAEClause]
cs) = ((Lit
n', [NAEClause]
cs'), Lit -> Lit -> [(Lit, NAEClause, NAEClause)] -> NAESAT2NAEKSATInfo
NAESAT2NAEKSATInfo Lit
n Lit
n' (forall a. [a] -> [a]
reverse [(Lit, NAEClause, NAEClause)]
table))
  where
    ([NAEClause]
cs',(Lit
n',[(Lit, NAEClause, NAEClause)]
table)) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> (a, s)
runState (Lit
n,[]) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NAEClause]
cs forall a b. (a -> b) -> a -> b
$ \NAEClause
c -> do
        let go :: NAEClause
-> [NAEClause]
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
go NAEClause
c' [NAEClause]
r =
              if forall (v :: * -> *) a. Vector v a => v a -> Lit
VG.length NAEClause
c' forall a. Ord a => a -> a -> Bool
<= Lit
k then do
                forall (m :: * -> *) a. Monad m => a -> m a
return  forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse (NAEClause
c' forall a. a -> [a] -> [a]
: [NAEClause]
r)
              else do
                let (NAEClause
cs1, NAEClause
cs2) = forall (v :: * -> *) a. Vector v a => Lit -> v a -> (v a, v a)
VG.splitAt (Lit
k forall a. Num a => a -> a -> a
- Lit
1) NAEClause
c'
                (Lit
i, [(Lit, NAEClause, NAEClause)]
tbl) <- forall s (m :: * -> *). MonadState s m => m s
get
                let w :: Lit
w = Lit
iforall a. Num a => a -> a -> a
+Lit
1
                seq :: forall a b. a -> b -> b
seq Lit
w forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *). MonadState s m => s -> m ()
put (Lit
w, (Lit
w,NAEClause
cs1,NAEClause
cs2) forall a. a -> [a] -> [a]
: [(Lit, NAEClause, NAEClause)]
tbl)
                NAEClause
-> [NAEClause]
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
go (forall (v :: * -> *) a. Vector v a => a -> v a -> v a
VG.cons (Lit -> PackedLit
SAT.packLit (- Lit
w)) NAEClause
cs2) (forall (v :: * -> *) a. Vector v a => v a -> a -> v a
VG.snoc NAEClause
cs1 (Lit -> PackedLit
SAT.packLit Lit
w) forall a. a -> [a] -> [a]
: [NAEClause]
r)
        NAEClause
-> [NAEClause]
-> State (Lit, [(Lit, NAEClause, NAEClause)]) [NAEClause]
go NAEClause
c []

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

instance ForwardTransformer NAESAT2NAEKSATInfo where
  transformForward :: NAESAT2NAEKSATInfo
-> Source NAESAT2NAEKSATInfo -> Target NAESAT2NAEKSATInfo
transformForward (NAESAT2NAEKSATInfo Lit
_n1 Lit
n2 [(Lit, NAEClause, NAEClause)]
table) Source NAESAT2NAEKSATInfo
m =
    forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1,Lit
n2) (forall {v :: * -> *} {v :: * -> *}.
(Vector v PackedLit, Vector v PackedLit) =>
IntMap Bool -> [(Lit, v PackedLit, v PackedLit)] -> [(Lit, Bool)]
go (forall a. [(Lit, a)] -> IntMap a
IntMap.fromList (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source NAESAT2NAEKSATInfo
m)) [(Lit, NAEClause, NAEClause)]
table)
    where
      go :: IntMap Bool -> [(Lit, v PackedLit, v PackedLit)] -> [(Lit, Bool)]
go IntMap Bool
im [] = forall a. IntMap a -> [(Lit, a)]
IntMap.toList IntMap Bool
im
      go IntMap Bool
im ((Lit
w,v PackedLit
cs1,v PackedLit
cs2) : [(Lit, v PackedLit, v PackedLit)]
tbl) = IntMap Bool -> [(Lit, v PackedLit, v PackedLit)] -> [(Lit, Bool)]
go (forall a. Lit -> a -> IntMap a -> IntMap a
IntMap.insert Lit
w Bool
val IntMap Bool
im) [(Lit, v PackedLit, v PackedLit)]
tbl
        where
          ev :: PackedLit -> Bool
ev PackedLit
x
            | PackedLit
x forall a. Ord a => a -> a -> Bool
> PackedLit
0     = IntMap Bool
im forall a. IntMap a -> Lit -> a
IntMap.! (PackedLit -> Lit
SAT.unpackLit PackedLit
x)
            | Bool
otherwise = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ IntMap Bool
im forall a. IntMap a -> Lit -> a
IntMap.! (- PackedLit -> Lit
SAT.unpackLit PackedLit
x)
          needTrue :: Bool
needTrue  = forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all PackedLit -> Bool
ev v PackedLit
cs2 Bool -> Bool -> Bool
|| forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Bool
ev) v PackedLit
cs1
          needFalse :: Bool
needFalse = forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all PackedLit -> Bool
ev v PackedLit
cs1 Bool -> Bool -> Bool
|| forall (v :: * -> *) a. Vector v a => (a -> Bool) -> v a -> Bool
VG.all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedLit -> Bool
ev) v PackedLit
cs2
          val :: Bool
val
            | Bool
needTrue Bool -> Bool -> Bool
&& Bool
needFalse = Bool
True -- error "naesat2naeksat_forward: invalid model"
            | Bool
needTrue  = Bool
True
            | Bool
needFalse = Bool
False
            | Bool
otherwise = Bool
False

instance BackwardTransformer NAESAT2NAEKSATInfo where
  transformBackward :: NAESAT2NAEKSATInfo
-> Target NAESAT2NAEKSATInfo -> Source NAESAT2NAEKSATInfo
transformBackward (NAESAT2NAEKSATInfo Lit
n1 Lit
_n2 [(Lit, NAEClause, NAEClause)]
_table) = Lit -> UArray Lit Bool -> UArray Lit Bool
SAT.restrictModel Lit
n1

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

type NAESAT2Max2SATInfo = ComposedTransformer NAESAT2NAEKSATInfo NAE3SAT2Max2SATInfo

naesat2max2sat :: NAESAT -> ((CNF.WCNF, Integer), NAESAT2Max2SATInfo)
naesat2max2sat :: NAESAT -> ((WCNF, Integer), NAESAT2Max2SATInfo)
naesat2max2sat NAESAT
x = ((WCNF, Integer)
x2, (forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer NAESAT2NAEKSATInfo
info1 NAESAT2SATInfo
info2))
  where
    (NAESAT
x1, NAESAT2NAEKSATInfo
info1) = Lit -> NAESAT -> (NAESAT, NAESAT2NAEKSATInfo)
naesat2naeksat Lit
3 NAESAT
x
    ((WCNF, Integer)
x2, NAESAT2SATInfo
info2) = NAESAT -> ((WCNF, Integer), NAESAT2SATInfo)
nae3sat2max2sat NAESAT
x1

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

type NAE3SAT2Max2SATInfo = IdentityTransformer SAT.Model

-- Original nae-sat problem is satisfiable iff MAX-2-SAT problem has solution with cost <=threshold.
nae3sat2max2sat :: NAESAT -> ((CNF.WCNF, Integer), NAE3SAT2Max2SATInfo)
nae3sat2max2sat :: NAESAT -> ((WCNF, Integer), NAESAT2SATInfo)
nae3sat2max2sat (Lit
n,[NAEClause]
cs)
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\NAEClause
c -> forall (v :: * -> *) a. Vector v a => v a -> Lit
VG.length NAEClause
c forall a. Ord a => a -> a -> Bool
< Lit
2) [NAEClause]
cs =
      ( ( CNF.WCNF
          { wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
2
          , wcnfNumVars :: Lit
CNF.wcnfNumVars = Lit
n
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [(Integer
1, Clause -> NAEClause
SAT.packClause [])]
          , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = Lit
1
          }
        , Integer
0
        )
      , forall a. IdentityTransformer a
IdentityTransformer
      )
  | Bool
otherwise =
      ( ( CNF.WCNF
          { wcnfTopCost :: Integer
CNF.wcnfTopCost = forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
nc' forall a. Num a => a -> a -> a
+ Integer
1
          , wcnfNumVars :: Lit
CNF.wcnfNumVars = Lit
n
          , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [WeightedClause]
cs'
          , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = Lit
nc'
          }
        , Integer
t
        )
      , forall a. IdentityTransformer a
IdentityTransformer
      )
  where
    nc' :: Lit
nc' = forall (t :: * -> *) a. Foldable t => t a -> Lit
length [WeightedClause]
cs'
    ([WeightedClause]
cs', Integer
t) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([WeightedClause], Integer)
-> NAEClause -> ([WeightedClause], Integer)
f ([],Integer
0) [NAEClause]
cs
      where
        f :: ([CNF.WeightedClause], Integer) -> NAEClause -> ([CNF.WeightedClause], Integer)
        f :: ([WeightedClause], Integer)
-> NAEClause -> ([WeightedClause], Integer)
f ([WeightedClause]
cs, !Integer
t) NAEClause
c =
          case NAEClause -> Clause
SAT.unpackClause NAEClause
c of
            []  -> forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: should not happen"
            [Lit
_] -> forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: should not happen"
            [Lit
_,Lit
_] ->
                ( [(Integer
1, NAEClause
c), (Integer
1, forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map forall a. Num a => a -> a
negate NAEClause
c)] forall a. [a] -> [a] -> [a]
++ [WeightedClause]
cs
                , Integer
t
                )
            [Lit
l0,Lit
l1,Lit
l2] ->
                ( forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Integer
1, Clause -> NAEClause
SAT.packClause [Lit
a,Lit
b]), (Integer
1, Clause -> NAEClause
SAT.packClause [-Lit
a,-Lit
b])] | (Lit
a,Lit
b) <- [(Lit
l0,Lit
l1),(Lit
l1,Lit
l2),(Lit
l2,Lit
l0)]] forall a. [a] -> [a] -> [a]
++ [WeightedClause]
cs
                , Integer
t forall a. Num a => a -> a -> a
+ Integer
1
                )
            Clause
_ -> forall a. HasCallStack => String -> a
error String
"nae3sat2max2sat: cannot handle nae-clause of size >3"

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