{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.PB.Internal.BCCNF
-- Copyright   :  (c) Masahiro Sakai 2022
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References
--
-- * 南 雄之 (Yushi Minami), 宋 剛秀 (Takehide Soh), 番原 睦則
--   (Mutsunori Banbara), 田村 直之 (Naoyuki Tamura). ブール基数制約を
--   経由した擬似ブール制約のSAT符号化手法 (A SAT Encoding of
--   Pseudo-Boolean Constraints via Boolean Cardinality Constraints).
--   Computer Software, 2018, volume 35, issue 3, pages 65-78,
--   <https://doi.org/10.11309/jssst.35.3_65>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.PB.Internal.BCCNF
  (
  -- * Monadic interface
    addPBLinAtLeastBCCNF
  , encodePBLinAtLeastWithPolarityBCCNF

  -- * High-level pure encoder
  , encode

  -- * Low-level implementation
  , preprocess

  -- ** Prefix sum
  , PrefixSum
  , toPrefixSum
  , encodePrefixSum
  , encodePrefixSumBuggy
  , encodePrefixSumNaive

  -- ** Boolean cardinality constraints
  , BCLit
  , toAtLeast
  , implyBCLit

  -- ** Clause over boolean cardinality constraints
  , BCClause
  , reduceBCClause
  , implyBCClause

  -- ** CNF over boolean cardinality constraints
  , BCCNF
  , reduceBCCNF
  ) where

import Control.Exception (assert)
import Control.Monad
import Control.Monad.Primitive
import Data.Function (on)
import Data.List (sortBy)
import Data.Maybe (listToMaybe)
import Data.Ord (comparing)

import ToySolver.SAT.Types
import qualified ToySolver.SAT.Encoder.Cardinality as Card
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

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

-- | \(\sum_{j=1}^i b_j s_j = \sum_{j=1}^i b_j (x_1, \ldots, x_j)\) is represented
-- as a list of tuples consisting of \(b_j, j, [x_1, \ldots, x_j]\).
type PrefixSum = [(Integer, Int, [Lit])]

-- | Convert 'PBLinSum' to 'PrefixSum'.
-- The 'PBLinSum' must be 'preprocess'ed before calling the function.
toPrefixSum :: PBLinSum -> PrefixSum
toPrefixSum :: PBLinSum -> PrefixSum
toPrefixSum PBLinSum
s =
  Bool -> PrefixSum -> PrefixSum
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 | (Integer
c, Int
_) <- PBLinSum
s] Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (((Integer, Int) -> (Integer, Int) -> Bool)
-> PBLinSum -> PBLinSum -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(>=) (Integer -> Integer -> Bool)
-> ((Integer, Int) -> Integer)
-> (Integer, Int)
-> (Integer, Int)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Integer, Int) -> Integer
forall a b. (a, b) -> a
fst) PBLinSum
s (PBLinSum -> PBLinSum
forall a. (?callStack::CallStack) => [a] -> [a]
tail PBLinSum
s))) (PrefixSum -> PrefixSum) -> PrefixSum -> PrefixSum
forall a b. (a -> b) -> a -> b
$
    Int -> [Int] -> PBLinSum -> PrefixSum
go Int
0 [] PBLinSum
s
  where
    go :: Int -> [Lit] -> PBLinSum -> PrefixSum
    go :: Int -> [Int] -> PBLinSum -> PrefixSum
go Int
_ [Int]
_ [] = []
    go !Int
i [Int]
prefix ((Integer
c, Int
l) : PBLinSum
ts)
      | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
c1 = (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c1, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, [Int] -> [Int]
forall a. [a] -> [a]
reverse (Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
prefix)) (Integer, Int, [Int]) -> PrefixSum -> PrefixSum
forall a. a -> [a] -> [a]
: Int -> [Int] -> PBLinSum -> PrefixSum
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
prefix) PBLinSum
ts
      | Bool
otherwise = Int -> [Int] -> PBLinSum -> PrefixSum
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
prefix) PBLinSum
ts
      where
        c1 :: Integer
c1 = Integer
-> ((Integer, Int) -> Integer) -> Maybe (Integer, Int) -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
0 (Integer, Int) -> Integer
forall a b. (a, b) -> a
fst (PBLinSum -> Maybe (Integer, Int)
forall a. [a] -> Maybe a
listToMaybe PBLinSum
ts)

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

-- | A constraint \(s_i \ge c\) where \(s_i = x_1 + \ldots + x_i\) is represnted as
-- a tuple of \(i\), \([x_1, \ldots, x_i]\), and \(c\).
type BCLit = (Int, [Lit], Int)

-- | Disjunction of 'BCLit'
type BCClause = [BCLit]

-- | Conjunction of 'BCClause'
type BCCNF = [BCClause]

-- | Forget \(s_i\) and returns \(x_1 + \ldots + x_i \ge c\).
toAtLeast :: BCLit -> AtLeast
toAtLeast :: BCLit -> AtLeast
toAtLeast (Int
_, [Int]
lhs, Int
rhs) = ([Int]
lhs, Int
rhs)

-- | \((s_i \ge a) \Rightarrow (s_j \ge b)\) is defined as
-- \((i \le j \wedge a \ge b) \vee (i \ge b \wedge i - a \le j - b)\).
implyBCLit :: BCLit -> BCLit -> Bool
implyBCLit :: BCLit -> BCLit -> Bool
implyBCLit (Int
i,[Int]
_,Int
a) (Int
j,[Int]
_,Int
b)
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
j = Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
b
  | Bool
otherwise = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b

-- | Remove redundant literals based on 'implyBCLit'.
reduceBCClause :: BCClause -> BCClause
reduceBCClause :: BCClause -> BCClause
reduceBCClause BCClause
lits = Bool -> BCClause -> BCClause
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (BCClause -> Bool
forall {a} {b} {c}. Ord a => [(a, b, c)] -> Bool
isAsc BCClause
lits2) (BCClause -> BCClause) -> BCClause -> BCClause
forall a b. (a -> b) -> a -> b
$ BCClause
lits2
  where
    isAsc :: [(a, b, c)] -> Bool
isAsc  [(a, b, c)]
ls = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [a
i1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
i2 | let is :: [a]
is = [a
i | (a
i,b
_,c
_) <- [(a, b, c)]
ls], (a
i1,a
i2) <- [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
is ([a] -> [a]
forall a. (?callStack::CallStack) => [a] -> [a]
tail [a]
is)]
    isDesc :: [(a, b, c)] -> Bool
isDesc [(a, b, c)]
ls = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [a
i1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
i2 | let is :: [a]
is = [a
i | (a
i,b
_,c
_) <- [(a, b, c)]
ls], (a
i1,a
i2) <- [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
is ([a] -> [a]
forall a. (?callStack::CallStack) => [a] -> [a]
tail [a]
is)]

    lits1 :: BCClause
lits1 = Bool -> BCClause -> BCClause
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (BCClause -> Bool
forall {a} {b} {c}. Ord a => [(a, b, c)] -> Bool
isAsc BCClause
lits) (BCClause -> BCClause) -> BCClause -> BCClause
forall a b. (a -> b) -> a -> b
$ BCClause -> Int -> BCClause -> BCClause
forall {t} {b}.
(Ord t, Num t) =>
[(t, b, t)] -> t -> [(t, b, t)] -> [(t, b, t)]
f1 [] Int
forall a. Bounded a => a
minBound BCClause
lits
    lits2 :: BCClause
lits2 = Bool -> BCClause -> BCClause
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (BCClause -> Bool
forall {a} {b} {c}. Ord a => [(a, b, c)] -> Bool
isDesc BCClause
lits1) (BCClause -> BCClause) -> BCClause -> BCClause
forall a b. (a -> b) -> a -> b
$ BCClause -> Int -> BCClause -> BCClause
forall {t} {a} {b}.
Ord t =>
[(a, b, t)] -> t -> [(a, b, t)] -> [(a, b, t)]
f2 [] Int
forall a. Bounded a => a
maxBound BCClause
lits1

    f1 :: [(t, b, t)] -> t -> [(t, b, t)] -> [(t, b, t)]
f1 [(t, b, t)]
r !t
_ [] = [(t, b, t)]
r
    f1 [(t, b, t)]
r !t
jb (l :: (t, b, t)
l@(t
i,b
_,t
a) : [(t, b, t)]
ls)
      | t
ia t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
jb = [(t, b, t)] -> t -> [(t, b, t)] -> [(t, b, t)]
f1 ((t, b, t)
l (t, b, t) -> [(t, b, t)] -> [(t, b, t)]
forall a. a -> [a] -> [a]
: [(t, b, t)]
r) t
ia [(t, b, t)]
ls
      | Bool
otherwise = [(t, b, t)] -> t -> [(t, b, t)] -> [(t, b, t)]
f1 [(t, b, t)]
r t
jb [(t, b, t)]
ls
      where
        ia :: t
ia = t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
a

    f2 :: [(a, b, t)] -> t -> [(a, b, t)] -> [(a, b, t)]
f2 [(a, b, t)]
r !t
_ [] = [(a, b, t)]
r
    f2 [(a, b, t)]
r !t
b (l :: (a, b, t)
l@(a
_,b
_,t
a) : [(a, b, t)]
ls)
      | t
a t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
b = [(a, b, t)] -> t -> [(a, b, t)] -> [(a, b, t)]
f2 ((a, b, t)
l (a, b, t) -> [(a, b, t)] -> [(a, b, t)]
forall a. a -> [a] -> [a]
: [(a, b, t)]
r) t
a [(a, b, t)]
ls
      | Bool
otherwise = [(a, b, t)] -> t -> [(a, b, t)] -> [(a, b, t)]
f2 [(a, b, t)]
r t
b [(a, b, t)]
ls

-- | \(C \Rightarrow C'\) is defined as \(\forall l\in C \exists l' \in C' (l \Rightarrow l')\).
implyBCClause :: BCClause -> BCClause -> Bool
implyBCClause :: BCClause -> BCClause -> Bool
implyBCClause BCClause
lits1 BCClause
lits2 = (BCLit -> Bool) -> BCClause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\BCLit
lit1 -> (BCLit -> Bool) -> BCClause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (BCLit -> BCLit -> Bool
implyBCLit BCLit
lit1) BCClause
lits2) BCClause
lits1

-- | Reduce 'BCCNF' by reducing each clause using 'reduceBCClause' and then
-- remove redundant clauses based on 'implyBCClause'.
reduceBCCNF :: BCCNF -> BCCNF
reduceBCCNF :: BCCNF -> BCCNF
reduceBCCNF = BCCNF -> BCCNF
reduceBCCNF' (BCCNF -> BCCNF) -> (BCCNF -> BCCNF) -> BCCNF -> BCCNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BCClause -> BCClause) -> BCCNF -> BCCNF
forall a b. (a -> b) -> [a] -> [b]
map BCClause -> BCClause
reduceBCClause

reduceBCCNF' :: BCCNF -> BCCNF
reduceBCCNF' :: BCCNF -> BCCNF
reduceBCCNF' = BCCNF -> BCCNF -> BCCNF
go []
  where
    go :: BCCNF -> BCCNF -> BCCNF
go BCCNF
r [] = BCCNF -> BCCNF
forall a. [a] -> [a]
reverse BCCNF
r
    go BCCNF
r (BCClause
c : BCCNF
cs)
      | (BCClause -> Bool) -> BCCNF -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\BCClause
c' -> BCClause -> BCClause -> Bool
implyBCClause BCClause
c' BCClause
c) (BCCNF
r BCCNF -> BCCNF -> BCCNF
forall a. [a] -> [a] -> [a]
++ BCCNF
cs) = BCCNF -> BCCNF -> BCCNF
go BCCNF
r BCCNF
cs
      | Bool
otherwise = BCCNF -> BCCNF -> BCCNF
go (BCClause
c BCClause -> BCCNF -> BCCNF
forall a. a -> [a] -> [a]
: BCCNF
r) BCCNF
cs

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

-- | Encode a given pseudo boolean constraint \(\sum_i a_i x_i \ge c\)
-- into an equilavent formula in the form of
-- \(\bigwedge_j \bigvee_k \sum_{l \in L_{j,k}} l \ge d_{j,k}\).
encode :: PBLinAtLeast -> [[AtLeast]]
encode :: PBLinAtLeast -> [[AtLeast]]
encode PBLinAtLeast
constr = (BCClause -> [AtLeast]) -> BCCNF -> [[AtLeast]]
forall a b. (a -> b) -> [a] -> [b]
map ((BCLit -> AtLeast) -> BCClause -> [AtLeast]
forall a b. (a -> b) -> [a] -> [b]
map BCLit -> AtLeast
toAtLeast) (BCCNF -> [[AtLeast]]) -> BCCNF -> [[AtLeast]]
forall a b. (a -> b) -> a -> b
$ BCCNF -> BCCNF
reduceBCCNF (BCCNF -> BCCNF) -> BCCNF -> BCCNF
forall a b. (a -> b) -> a -> b
$ PrefixSum -> Integer -> BCCNF
encodePrefixSum (PBLinSum -> PrefixSum
toPrefixSum PBLinSum
lhs) Integer
rhs
  where
    (PBLinSum
lhs, Integer
rhs) = PBLinAtLeast -> PBLinAtLeast
preprocess PBLinAtLeast
constr

-- | Perform 'normalizePBLinAtLeast' and sort the terms in descending order of coefficients
preprocess :: PBLinAtLeast -> PBLinAtLeast
preprocess :: PBLinAtLeast -> PBLinAtLeast
preprocess PBLinAtLeast
constr = (PBLinSum
lhs2, Integer
rhs1)
  where
    (PBLinSum
lhs1, Integer
rhs1) = PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast PBLinAtLeast
constr
    lhs2 :: PBLinSum
lhs2 = ((Integer, Int) -> (Integer, Int) -> Ordering)
-> PBLinSum -> PBLinSum
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Integer, Int) -> (Integer, Int) -> Ordering)
-> (Integer, Int) -> (Integer, Int) -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Integer, Int) -> Integer)
-> (Integer, Int) -> (Integer, Int) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Integer, Int) -> Integer
forall a b. (a, b) -> a
fst) ((Integer, Int) -> (Integer, Int) -> Ordering)
-> ((Integer, Int) -> (Integer, Int) -> Ordering)
-> (Integer, Int)
-> (Integer, Int)
-> Ordering
forall a. Semigroup a => a -> a -> a
<> ((Integer, Int) -> Int)
-> (Integer, Int) -> (Integer, Int) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int -> Int
forall a. Num a => a -> a
abs (Int -> Int) -> ((Integer, Int) -> Int) -> (Integer, Int) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Int) -> Int
forall a b. (a, b) -> b
snd)) PBLinSum
lhs1

-- | Algorithm 2 in the paper but with a bug fixed
encodePrefixSum :: PrefixSum -> Integer -> [[BCLit]]
encodePrefixSum :: PrefixSum -> Integer -> BCCNF
encodePrefixSum = Int -> Int -> PrefixSum -> Integer -> BCCNF
forall {a} {a} {b}.
(Integral a, Integral a) =>
a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f Int
0 Int
0
  where
    f :: a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f !a
_ !a
_ [] !a
c = if a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 then [[]] else []
    f a
i0 a
d0 ((a
0,a
_,b
_) : [(a, a, b)]
bss) a
c = a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f a
i0 a
d0 [(a, a, b)]
bss a
c
    f a
i0 a
d0 ((a
b,a
i,b
ls) : [(a, a, b)]
bss) a
c =
      [ [(a
i, b
ls, [a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [a]
ds' a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)] | Bool -> Bool
not ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ds') ]
      [[(a, b, a)]] -> [[(a, b, a)]] -> [[(a, b, a)]]
forall a. [a] -> [a] -> [a]
++
      [ if a
da -> a -> a
forall a. Num a => a -> a -> a
+a
1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
i then [(a, b, a)]
theta else (a
i, b
ls, a
da -> a -> a
forall a. Num a => a -> a -> a
+a
1) (a, b, a) -> [(a, b, a)] -> [(a, b, a)]
forall a. a -> [a] -> [a]
: [(a, b, a)]
theta
      | a
d <- [a]
ds, [(a, b, a)]
theta <- a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f a
i a
d [(a, a, b)]
bss (a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d))
      ]
      where
        bssMax :: a -> a
bssMax a
d = a -> a
forall {a}. Integral a => a -> a
bssMin a
d a -> a -> a
forall a. Num a => a -> a -> a
+ [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a
b' a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
i' a -> a -> a
forall a. Num a => a -> a -> a
- a
i) | (a
b', a
i', b
_) <- [(a, a, b)]
bss]
        bssMin :: a -> a
bssMin a
d = [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a
b' | (a
b', a
_, b
_) <- [(a, a, b)]
bss]  a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d
        ds :: [a]
ds  = [a
d | a
d <- [a
d0 .. a
d0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
i a -> a -> a
forall a. Num a => a -> a -> a
- a
i0], let bd :: a
bd = a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d, a
c a -> a -> a
forall a. Num a => a -> a -> a
- a -> a
forall {a}. Integral a => a -> a
bssMax a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
bd, a
bd a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c a -> a -> a
forall a. Num a => a -> a -> a
- a -> a
forall {a}. Integral a => a -> a
bssMin a
d]
        ds' :: [a]
ds' = [a
d | a
d <- [a
d0 .. a
d0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
i a -> a -> a
forall a. Num a => a -> a -> a
- a
i0], a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c a -> a -> a
forall a. Num a => a -> a -> a
- a -> a
forall {a}. Integral a => a -> a
bssMax a
d]

-- | Algorithm 2 in the paper
encodePrefixSumBuggy :: PrefixSum -> Integer -> [[BCLit]]
encodePrefixSumBuggy :: PrefixSum -> Integer -> BCCNF
encodePrefixSumBuggy = Int -> Int -> PrefixSum -> Integer -> BCCNF
forall {a} {a} {b}.
(Integral a, Integral a) =>
a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f Int
0 Int
0
  where
    f :: a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f !a
_ !a
_ [] !a
c = if a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 then [[]] else []
    f a
i0 a
d0 ((a
0,a
_,b
_) : [(a, a, b)]
bss) a
c = a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f a
i0 a
d0 [(a, a, b)]
bss a
c
    f a
i0 a
d0 ((a
b,a
i,b
ls) : [(a, a, b)]
bss) a
c =
      [ [(a
i, b
ls, a -> a -> a
forall a. Ord a => a -> a -> a
max ([a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [a]
ds' a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) a
d0)] | Bool -> Bool
not ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ds') ]
      [[(a, b, a)]] -> [[(a, b, a)]] -> [[(a, b, a)]]
forall a. [a] -> [a] -> [a]
++
      [ if a
da -> a -> a
forall a. Num a => a -> a -> a
+a
1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
i then [(a, b, a)]
theta else (a
i, b
ls, a
da -> a -> a
forall a. Num a => a -> a -> a
+a
1) (a, b, a) -> [(a, b, a)] -> [(a, b, a)]
forall a. a -> [a] -> [a]
: [(a, b, a)]
theta
      | a
d <- [a]
ds, [(a, b, a)]
theta <- a -> a -> [(a, a, b)] -> a -> [[(a, b, a)]]
f a
i a
d [(a, a, b)]
bss (a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d))
      ]
      where
        bssMax :: a -> a
bssMax a
d = a -> a
forall {a}. Integral a => a -> a
bssMin a
d a -> a -> a
forall a. Num a => a -> a -> a
+ [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a
b' a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
i' a -> a -> a
forall a. Num a => a -> a -> a
- a
i) | (a
b', a
i', b
_) <- [(a, a, b)]
bss]
        bssMin :: a -> a
bssMin a
d = [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a
b' | (a
b', a
_, b
_) <- [(a, a, b)]
bss]  a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d
        ds :: [a]
ds  = [a
d | a
d <- [a
d0 .. a
d0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
i a -> a -> a
forall a. Num a => a -> a -> a
- a
i0], let bd :: a
bd = a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d, a
c a -> a -> a
forall a. Num a => a -> a -> a
- a -> a
forall {a}. Integral a => a -> a
bssMax a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
bd, a
bd a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c a -> a -> a
forall a. Num a => a -> a -> a
- a -> a
forall {a}. Integral a => a -> a
bssMin a
d]
        ds' :: [a]
ds' = [a
d | a
d <- [a
0..a
i], a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c a -> a -> a
forall a. Num a => a -> a -> a
- a -> a
forall {a}. Integral a => a -> a
bssMax a
d]

-- | Algorithm 1 in the paper
encodePrefixSumNaive :: PrefixSum -> Integer -> [[BCLit]]
encodePrefixSumNaive :: PrefixSum -> Integer -> BCCNF
encodePrefixSumNaive = PrefixSum -> Integer -> BCCNF
forall {a} {a} {b}.
(Integral a, Integral a) =>
[(a, a, b)] -> a -> [[(a, b, a)]]
f
  where
    f :: [(a, a, b)] -> a -> [[(a, b, a)]]
f [] !a
c = if a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 then [[]] else []
    f ((a
0,a
_,b
_) : [(a, a, b)]
bss) a
c = [(a, a, b)] -> a -> [[(a, b, a)]]
f [(a, a, b)]
bss a
c
    f ((a
b,a
i,b
ls) : [(a, a, b)]
bss) a
c =
      [ [(a
i, b
ls, [a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [a]
ds' a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)] | Bool -> Bool
not ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ds') ]
      [[(a, b, a)]] -> [[(a, b, a)]] -> [[(a, b, a)]]
forall a. [a] -> [a] -> [a]
++
      [ if a
da -> a -> a
forall a. Num a => a -> a -> a
+a
1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
i then [(a, b, a)]
theta else (a
i, b
ls, a
da -> a -> a
forall a. Num a => a -> a -> a
+a
1) (a, b, a) -> [(a, b, a)] -> [(a, b, a)]
forall a. a -> [a] -> [a]
: [(a, b, a)]
theta
      | a
d <- [a]
ds, [(a, b, a)]
theta <- [(a, a, b)] -> a -> [[(a, b, a)]]
f [(a, a, b)]
bss (a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d))
      ]
      where
        bssMax :: a
bssMax = [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [a
b' a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
i' | (a
b', a
i', b
_) <- [(a, a, b)]
bss]
        bssMin :: a
bssMin = a
0
        ds :: [a]
ds  = [a
d | a
d <- [a
0..a
i], let bd :: a
bd = a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d, a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
bssMax a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
bd, a
bd a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
bssMin]
        ds' :: [a]
ds' = [a
d | a
d <- [a
0..a
i], a
b a -> a -> a
forall a. Num a => a -> a -> a
* a -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
bssMax]

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

addPBLinAtLeastBCCNF :: PrimMonad m => Card.Encoder m -> PBLinAtLeast -> m ()
addPBLinAtLeastBCCNF :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m ()
addPBLinAtLeastBCCNF Encoder m
enc PBLinAtLeast
constr = do
  [[AtLeast]] -> ([AtLeast] -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (PBLinAtLeast -> [[AtLeast]]
encode PBLinAtLeast
constr) (([AtLeast] -> m ()) -> m ()) -> ([AtLeast] -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \[AtLeast]
clause -> do
    Encoder m -> [Int] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
addClause Encoder m
enc ([Int] -> m ()) -> m [Int] -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (AtLeast -> m Int) -> [AtLeast] -> m [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Encoder m -> AtLeast -> m Int
forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
Card.encodeAtLeast Encoder m
enc) [AtLeast]
clause

encodePBLinAtLeastWithPolarityBCCNF :: PrimMonad m => Card.Encoder m -> Tseitin.Polarity -> PBLinAtLeast -> m Lit
encodePBLinAtLeastWithPolarityBCCNF :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> PBLinAtLeast -> m Int
encodePBLinAtLeastWithPolarityBCCNF Encoder m
enc Polarity
polarity PBLinAtLeast
constr = do
  let tseitin :: Encoder m
tseitin = Encoder m -> Encoder m
forall (m :: * -> *). Encoder m -> Encoder m
Card.getTseitinEncoder Encoder m
enc
  [Int]
ls <- [[AtLeast]] -> ([AtLeast] -> m Int) -> m [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (PBLinAtLeast -> [[AtLeast]]
encode PBLinAtLeast
constr) (([AtLeast] -> m Int) -> m [Int])
-> ([AtLeast] -> m Int) -> m [Int]
forall a b. (a -> b) -> a -> b
$ \[AtLeast]
clause -> do
    Encoder m -> Polarity -> [Int] -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Int] -> m Int
Tseitin.encodeDisjWithPolarity Encoder m
tseitin Polarity
polarity ([Int] -> m Int) -> m [Int] -> m Int
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (AtLeast -> m Int) -> [AtLeast] -> m [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Encoder m -> Polarity -> AtLeast -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> AtLeast -> m Int
Card.encodeAtLeastWithPolarity Encoder m
enc Polarity
polarity) [AtLeast]
clause
  Encoder m -> Polarity -> [Int] -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Int] -> m Int
Tseitin.encodeConjWithPolarity Encoder m
tseitin Polarity
polarity [Int]
ls

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