{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.Cardinality
-- Copyright   :  (c) Masahiro Sakai 2019
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.Cardinality
  ( Encoder
  , Strategy (..)
  , newEncoder
  , newEncoderWithStrategy
  , encodeAtLeast

    -- XXX
  , TotalizerDefinitions
  , getTotalizerDefinitions
  , evalTotalizerDefinitions
  ) where

import Control.Monad.Primitive
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Cardinality.Internal.Naive
import ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
import ToySolver.SAT.Encoder.PB.Internal.BDD as BDD
import qualified ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer as Totalizer

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

-- XXX
data Encoder m = Encoder (Totalizer.Encoder m) Strategy

data Strategy
  = Naive
  | SequentialCounter
  | ParallelCounter
  | Totalizer
  deriving (Int -> Strategy -> ShowS
[Strategy] -> ShowS
Strategy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Strategy] -> ShowS
$cshowList :: [Strategy] -> ShowS
show :: Strategy -> String
$cshow :: Strategy -> String
showsPrec :: Int -> Strategy -> ShowS
$cshowsPrec :: Int -> Strategy -> ShowS
Show, Strategy -> Strategy -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Strategy -> Strategy -> Bool
$c/= :: Strategy -> Strategy -> Bool
== :: Strategy -> Strategy -> Bool
$c== :: Strategy -> Strategy -> Bool
Eq, Eq Strategy
Strategy -> Strategy -> Bool
Strategy -> Strategy -> Ordering
Strategy -> Strategy -> Strategy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Strategy -> Strategy -> Strategy
$cmin :: Strategy -> Strategy -> Strategy
max :: Strategy -> Strategy -> Strategy
$cmax :: Strategy -> Strategy -> Strategy
>= :: Strategy -> Strategy -> Bool
$c>= :: Strategy -> Strategy -> Bool
> :: Strategy -> Strategy -> Bool
$c> :: Strategy -> Strategy -> Bool
<= :: Strategy -> Strategy -> Bool
$c<= :: Strategy -> Strategy -> Bool
< :: Strategy -> Strategy -> Bool
$c< :: Strategy -> Strategy -> Bool
compare :: Strategy -> Strategy -> Ordering
$ccompare :: Strategy -> Strategy -> Ordering
Ord, Int -> Strategy
Strategy -> Int
Strategy -> [Strategy]
Strategy -> Strategy
Strategy -> Strategy -> [Strategy]
Strategy -> Strategy -> Strategy -> [Strategy]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
$cenumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
enumFromTo :: Strategy -> Strategy -> [Strategy]
$cenumFromTo :: Strategy -> Strategy -> [Strategy]
enumFromThen :: Strategy -> Strategy -> [Strategy]
$cenumFromThen :: Strategy -> Strategy -> [Strategy]
enumFrom :: Strategy -> [Strategy]
$cenumFrom :: Strategy -> [Strategy]
fromEnum :: Strategy -> Int
$cfromEnum :: Strategy -> Int
toEnum :: Int -> Strategy
$ctoEnum :: Int -> Strategy
pred :: Strategy -> Strategy
$cpred :: Strategy -> Strategy
succ :: Strategy -> Strategy
$csucc :: Strategy -> Strategy
Enum, Strategy
forall a. a -> a -> Bounded a
maxBound :: Strategy
$cmaxBound :: Strategy
minBound :: Strategy
$cminBound :: Strategy
Bounded)
{-
"Sequential Counter" from "Towards an Optimal CNF Encoding of Boolean
Cardinality Constraints" is a special case of BDD-based encoding of
"Translating Pseudo-Boolean Constraints into SAT" (using the fact C→B
to represent ite(A,B,C) as (A∧B)∨C instead of (A∧B)∨(¬A∧C))?

http://www.carstensinz.de/papers/CP-2005.pdf
http://www.st.ewi.tudelft.nl/jsat/content/volume2/JSAT2_1_Een.pdf
-}

newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
newEncoder :: forall (m :: * -> *). PrimMonad m => Encoder m -> m (Encoder m)
newEncoder Encoder m
tseitin = forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
ParallelCounter

newEncoderWithStrategy :: PrimMonad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
strategy = do
  Encoder m
base <- forall (m :: * -> *). PrimMonad m => Encoder m -> m (Encoder m)
Totalizer.newEncoder Encoder m
tseitin
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Encoder m -> Strategy -> Encoder m
Encoder Encoder m
base Strategy
strategy

type TotalizerDefinitions = Totalizer.Definitions

getTotalizerDefinitions :: PrimMonad m => Encoder m -> m TotalizerDefinitions
getTotalizerDefinitions :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m TotalizerDefinitions
getTotalizerDefinitions (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m TotalizerDefinitions
Totalizer.getDefinitions Encoder m
base

evalTotalizerDefinitions :: SAT.IModel m => m -> TotalizerDefinitions -> [(SAT.Var, Bool)]
evalTotalizerDefinitions :: forall m. IModel m => m -> TotalizerDefinitions -> [(Int, Bool)]
evalTotalizerDefinitions m
m TotalizerDefinitions
defs = forall m. IModel m => m -> TotalizerDefinitions -> [(Int, Bool)]
Totalizer.evalDefinitions m
m TotalizerDefinitions
defs

-- getTseitinEncoder :: Encoder m -> Tseitin.Encoder m
-- getTseitinEncoder (Encoder tseitin _) = tseitin

instance Monad m => SAT.NewVar m (Encoder m) where
  newVar :: Encoder m -> m Int
newVar   (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Encoder m
base
  newVars :: Encoder m -> Int -> m [Int]
newVars  (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars Encoder m
base
  newVars_ :: Encoder m -> Int -> m ()
newVars_ (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Encoder m
base

instance Monad m => SAT.AddClause m (Encoder m) where
  addClause :: Encoder m -> [Int] -> m ()
addClause (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
base

instance PrimMonad m => SAT.AddCardinality m (Encoder m) where
  addAtLeast :: Encoder m -> [Int] -> Int -> m ()
addAtLeast (Encoder base :: Encoder m
base@(Totalizer.Encoder Encoder m
tseitin MutVar (PrimState m) (Map LitSet (Vector Int))
_) Strategy
strategy) [Int]
lhs Int
rhs
    | Int
rhs forall a. Ord a => a -> a -> Bool
<= Int
0  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise =
        case Strategy
strategy of
          Strategy
Naive -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
addAtLeastNaive Encoder m
tseitin ([Int]
lhs,Int
rhs)
          Strategy
ParallelCounter -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
addAtLeastParallelCounter Encoder m
tseitin ([Int]
lhs,Int
rhs)
          Strategy
SequentialCounter -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m ()
BDD.addPBLinAtLeastBDD Encoder m
tseitin ([(Integer
1,Int
l) | Int
l <- [Int]
lhs], forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
rhs)
          Strategy
Totalizer -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
Totalizer.addAtLeast Encoder m
base ([Int]
lhs,Int
rhs)

encodeAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m SAT.Lit
encodeAtLeast :: forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeast (Encoder base :: Encoder m
base@(Totalizer.Encoder Encoder m
tseitin MutVar (PrimState m) (Map LitSet (Vector Int))
_) Strategy
strategy) =
  case Strategy
strategy of
    Strategy
Naive -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeastNaive Encoder m
tseitin
    Strategy
ParallelCounter -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeastParallelCounter Encoder m
tseitin
    Strategy
SequentialCounter -> \([Int]
lhs,Int
rhs) -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m Int
BDD.encodePBLinAtLeastBDD Encoder m
tseitin ([(Integer
1,Int
l) | Int
l <- [Int]
lhs], forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
rhs)
    Strategy
Totalizer -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
Totalizer.encodeAtLeast Encoder m
base