msakai / toysolver / 496

Committed 10 Nov 2024 11:05AM UTC coverage: 69.994% (-1.1%) from 71.113%

Build # 496

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #117 from msakai/update-coveralls-and-haddock

GitHub Actions: Update coveralls and haddock configuration

Run Details

9872 of 14104 relevant lines covered (69.99%)

0.7 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

73.61

/src/ToySolver/SAT/Encoder/PB/Internal/BCCNF.hs

{-# 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 s =
  assert (and [c > 0 | (c, _) <- s] && and (zipWith ((>=) `on` fst) s (tail s))) $
    go 0 [] s
  where
    go :: Int -> [Lit] -> PBLinSum -> PrefixSum
    go _ _ [] = []
    go !i prefix ((c, l) : ts)
      | c > c1 = (c - c1, i + 1, reverse (l : prefix)) : go (i + 1) (l : prefix) ts
      | otherwise = go (i + 1) (l : prefix) ts
      where
        c1 = maybe 0 fst (listToMaybe 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 (_, lhs, rhs) = (lhs, 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 (i,_,a) (j,_,b)
  | i <= j = a >= b
  | otherwise = i - a <= j - b

-- | Remove redundant literals based on 'implyBCLit'.
reduceBCClause :: BCClause -> BCClause
reduceBCClause lits = assert (isAsc lits2) $ lits2
  where
    isAsc  ls = and [i1 <= i2 | let is = [i | (i,_,_) <- ls], (i1,i2) <- zip is (tail is)]
    isDesc ls = and [i1 >= i2 | let is = [i | (i,_,_) <- ls], (i1,i2) <- zip is (tail is)]

    lits1 = assert (isAsc lits) $ f1 [] minBound lits
    lits2 = assert (isDesc lits1) $ f2 [] maxBound lits1

    f1 r !_ [] = r
    f1 r !jb (l@(i,_,a) : ls)
      | ia > jb = f1 (l : r) ia ls
      | otherwise = f1 r jb ls
      where
        ia = i - a

    f2 r !_ [] = r
    f2 r !b (l@(_,_,a) : ls)
      | a < b = f2 (l : r) a ls
      | otherwise = f2 r b ls

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

-- | Reduce 'BCCNF' by reducing each clause using 'reduceBCClause' and then
-- remove redundant clauses based on 'implyBCClause'.
reduceBCCNF :: BCCNF -> BCCNF
reduceBCCNF = reduceBCCNF' . map reduceBCClause

reduceBCCNF' :: BCCNF -> BCCNF
reduceBCCNF' = go []
  where
    go r [] = reverse r
    go r (c : cs)
      | any (\c' -> implyBCClause c' c) (r ++ cs) = go r cs
      | otherwise = go (c : r) 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 constr = map (map toAtLeast) $ reduceBCCNF $ encodePrefixSum (toPrefixSum lhs) rhs
  where
    (lhs, rhs) = preprocess constr

-- | Perform 'normalizePBLinAtLeast' and sort the terms in descending order of coefficients
preprocess :: PBLinAtLeast -> PBLinAtLeast
preprocess constr = (lhs2, rhs1)
  where
    (lhs1, rhs1) = normalizePBLinAtLeast constr
    lhs2 = sortBy (flip (comparing fst) <> comparing (abs . snd)) lhs1

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

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

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

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

addPBLinAtLeastBCCNF :: PrimMonad m => Card.Encoder m -> PBLinAtLeast -> m ()
addPBLinAtLeastBCCNF enc constr = do
  forM_ (encode constr) $ \clause -> do
    addClause enc =<< mapM (Card.encodeAtLeast enc) clause

encodePBLinAtLeastWithPolarityBCCNF :: PrimMonad m => Card.Encoder m -> Tseitin.Polarity -> PBLinAtLeast -> m Lit
encodePBLinAtLeastWithPolarityBCCNF enc polarity constr = do
  let tseitin = Card.getTseitinEncoder enc
  ls <- forM (encode constr) $ \clause -> do
    Tseitin.encodeDisjWithPolarity tseitin polarity =<< mapM (Card.encodeAtLeastWithPolarity enc polarity) clause
  Tseitin.encodeConjWithPolarity tseitin polarity ls

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

1	{-# LANGUAGE BangPatterns #-}
2	{-# OPTIONS_GHC -Wall #-}
3	{-# OPTIONS_HADDOCK show-extensions #-}
4	-----------------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.SAT.Encoder.PB.Internal.BCCNF
7	-- Copyright : (c) Masahiro Sakai 2022
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : provisional
12	-- Portability : non-portable
13	--
14	-- References
15	--
16	-- * 南雄之 (Yushi Minami), 宋剛秀 (Takehide Soh), 番原睦則
17	-- (Mutsunori Banbara), 田村直之 (Naoyuki Tamura). ブール基数制約を
18	-- 経由した擬似ブール制約のSAT符号化手法 (A SAT Encoding of
19	-- Pseudo-Boolean Constraints via Boolean Cardinality Constraints).
20	-- Computer Software, 2018, volume 35, issue 3, pages 65-78,
21	-- <https://doi.org/10.11309/jssst.35.3_65>
22	--
23	-----------------------------------------------------------------------------
24	module ToySolver.SAT.Encoder.PB.Internal.BCCNF
25	(
26	-- * Monadic interface
27	addPBLinAtLeastBCCNF
28	, encodePBLinAtLeastWithPolarityBCCNF
29
30	-- * High-level pure encoder
31	, encode
32
33	-- * Low-level implementation
34	, preprocess
35
36	-- ** Prefix sum
37	, PrefixSum
38	, toPrefixSum
39	, encodePrefixSum
40	, encodePrefixSumBuggy
41	, encodePrefixSumNaive
42
43	-- ** Boolean cardinality constraints
44	, BCLit
45	, toAtLeast
46	, implyBCLit
47
48	-- ** Clause over boolean cardinality constraints
49	, BCClause
50	, reduceBCClause
51	, implyBCClause
52
53	-- ** CNF over boolean cardinality constraints
54	, BCCNF
55	, reduceBCCNF
56	) where
57
58	import Control.Exception (assert)
59	import Control.Monad
60	import Control.Monad.Primitive
61	import Data.Function (on)
62	import Data.List (sortBy)
63	import Data.Maybe (listToMaybe)
64	import Data.Ord (comparing)
65
66	import ToySolver.SAT.Types
67	import qualified ToySolver.SAT.Encoder.Cardinality as Card
68	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
69
70	-- ------------------------------------------------------------------------
71
72	-- \| \(\sum_{j=1}^i b_j s_j = \sum_{j=1}^i b_j (x_1, \ldots, x_j)\) is represented
73	-- as a list of tuples consisting of \(b_j, j, [x_1, \ldots, x_j]\).
74	type PrefixSum = [(Integer, Int, [Lit])]
75
76	-- \| Convert 'PBLinSum' to 'PrefixSum'.
77	-- The 'PBLinSum' must be 'preprocess'ed before calling the function.
78	toPrefixSum :: PBLinSum -> PrefixSum
79	toPrefixSum s =	1✔
80	assert (and [c > 0 \| (c, _) <- s] && and (zipWith ((>=) `on` fst) s (tail s))) $	×
81	go 0 [] s	1✔
82	where
83	go :: Int -> [Lit] -> PBLinSum -> PrefixSum
84	go _ _ [] = []	1✔
85	go !i prefix ((c, l) : ts)
86	\| c > c1 = (c - c1, i + 1, reverse (l : prefix)) : go (i + 1) (l : prefix) ts	1✔
87	\| otherwise = go (i + 1) (l : prefix) ts	×
88	where
89	c1 = maybe 0 fst (listToMaybe ts)	1✔
90
91	-- ------------------------------------------------------------------------
92
93	-- \| A constraint \(s_i \ge c\) where \(s_i = x_1 + \ldots + x_i\) is represnted as
94	-- a tuple of \(i\), \([x_1, \ldots, x_i]\), and \(c\).
95	type BCLit = (Int, [Lit], Int)
96
97	-- \| Disjunction of 'BCLit'
98	type BCClause = [BCLit]
99
100	-- \| Conjunction of 'BCClause'
101	type BCCNF = [BCClause]
102
103	-- \| Forget \(s_i\) and returns \(x_1 + \ldots + x_i \ge c\).
104	toAtLeast :: BCLit -> AtLeast
105	toAtLeast (_, lhs, rhs) = (lhs, rhs)	1✔
106
107	-- \| \((s_i \ge a) \Rightarrow (s_j \ge b)\) is defined as
108	-- \((i \le j \wedge a \ge b) \vee (i \ge b \wedge i - a \le j - b)\).
109	implyBCLit :: BCLit -> BCLit -> Bool
110	implyBCLit (i,_,a) (j,_,b)	1✔
111	\| i <= j = a >= b	1✔
112	\| otherwise = i - a <= j - b	×
113
114	-- \| Remove redundant literals based on 'implyBCLit'.
115	reduceBCClause :: BCClause -> BCClause
116	reduceBCClause lits = assert (isAsc lits2) $ lits2	×
117	where
118	isAsc ls = and [i1 <= i2 \| let is = [i \| (i,_,_) <- ls], (i1,i2) <- zip is (tail is)]	×
119	isDesc ls = and [i1 >= i2 \| let is = [i \| (i,_,_) <- ls], (i1,i2) <- zip is (tail is)]	×
120
121	lits1 = assert (isAsc lits) $ f1 [] minBound lits	×
122	lits2 = assert (isDesc lits1) $ f2 [] maxBound lits1	×
123
124	f1 r !_ [] = r	1✔
125	f1 r !jb (l@(i,_,a) : ls)
126	\| ia > jb = f1 (l : r) ia ls	1✔
127	\| otherwise = f1 r jb ls	×
128	where
129	ia = i - a	1✔
130
131	f2 r !_ [] = r	1✔
132	f2 r !b (l@(_,_,a) : ls)
133	\| a < b = f2 (l : r) a ls	1✔
134	\| otherwise = f2 r b ls	×
135
136	-- \| \(C \Rightarrow C'\) is defined as \(\forall l\in C \exists l' \in C' (l \Rightarrow l')\).
137	implyBCClause :: BCClause -> BCClause -> Bool
138	implyBCClause lits1 lits2 = all (\lit1 -> any (implyBCLit lit1) lits2) lits1	1✔
139
140	-- \| Reduce 'BCCNF' by reducing each clause using 'reduceBCClause' and then
141	-- remove redundant clauses based on 'implyBCClause'.
142	reduceBCCNF :: BCCNF -> BCCNF
143	reduceBCCNF = reduceBCCNF' . map reduceBCClause	1✔
144
145	reduceBCCNF' :: BCCNF -> BCCNF
146	reduceBCCNF' = go []	1✔
147	where
148	go r [] = reverse r	1✔
149	go r (c : cs)
150	\| any (\c' -> implyBCClause c' c) (r ++ cs) = go r cs	1✔
151	\| otherwise = go (c : r) cs	×
152
153	-- ------------------------------------------------------------------------
154
155	-- \| Encode a given pseudo boolean constraint \(\sum_i a_i x_i \ge c\)
156	-- into an equilavent formula in the form of
157	-- \(\bigwedge_j \bigvee_k \sum_{l \in L_{j,k}} l \ge d_{j,k}\).
158	encode :: PBLinAtLeast -> [[AtLeast]]
159	encode constr = map (map toAtLeast) $ reduceBCCNF $ encodePrefixSum (toPrefixSum lhs) rhs	1✔
160	where
161	(lhs, rhs) = preprocess constr	1✔
162
163	-- \| Perform 'normalizePBLinAtLeast' and sort the terms in descending order of coefficients
164	preprocess :: PBLinAtLeast -> PBLinAtLeast
165	preprocess constr = (lhs2, rhs1)	1✔
166	where
167	(lhs1, rhs1) = normalizePBLinAtLeast constr	1✔
168	lhs2 = sortBy (flip (comparing fst) <> comparing (abs . snd)) lhs1	1✔
169
170	-- \| Algorithm 2 in the paper but with a bug fixed
171	encodePrefixSum :: PrefixSum -> Integer -> [[BCLit]]
172	encodePrefixSum = f 0 0	1✔
173	where
174	f !_ !_ [] !c = if c > 0 then [[]] else []	1✔
175	f i0 d0 ((0,_,_) : bss) c = f i0 d0 bss c	×
176	f i0 d0 ((b,i,ls) : bss) c =
177	[ [(i, ls, maximum ds' + 1)] \| not (null ds') ]	1✔
178	++
179	[ if d+1 > i then theta else (i, ls, d+1) : theta	1✔
180	\| d <- ds, theta <- f i d bss (fromIntegral (c - b * fromIntegral d))	1✔
181	]
182	where
183	bssMax d = bssMin d + sum [b' * fromIntegral (i' - i) \| (b', i', _) <- bss]	1✔
184	bssMin d = sum [b' \| (b', _, _) <- bss] * fromIntegral d	1✔
185	ds = [d \| d <- [d0 .. d0 + i - i0], let bd = b * fromIntegral d, c - bssMax d <= bd, bd < c - bssMin d]	1✔
186	ds' = [d \| d <- [d0 .. d0 + i - i0], b * fromIntegral d < c - bssMax d]	1✔
187
188	-- \| Algorithm 2 in the paper
189	encodePrefixSumBuggy :: PrefixSum -> Integer -> [[BCLit]]
190	encodePrefixSumBuggy = f 0 0	1✔
191	where
192	f !_ !_ [] !c = if c > 0 then [[]] else []	×
193	f i0 d0 ((0,_,_) : bss) c = f i0 d0 bss c	×
194	f i0 d0 ((b,i,ls) : bss) c =
195	[ [(i, ls, max (maximum ds' + 1) d0)] \| not (null ds') ]	×
196	++
197	[ if d+1 > i then theta else (i, ls, d+1) : theta	×
198	\| d <- ds, theta <- f i d bss (fromIntegral (c - b * fromIntegral d))	1✔
199	]
200	where
201	bssMax d = bssMin d + sum [b' * fromIntegral (i' - i) \| (b', i', _) <- bss]	1✔
202	bssMin d = sum [b' \| (b', _, _) <- bss] * fromIntegral d	1✔
203	ds = [d \| d <- [d0 .. d0 + i - i0], let bd = b * fromIntegral d, c - bssMax d <= bd, bd < c - bssMin d]	1✔
204	ds' = [d \| d <- [0..i], b * fromIntegral d < c - bssMax d]	1✔
205
206	-- \| Algorithm 1 in the paper
207	encodePrefixSumNaive :: PrefixSum -> Integer -> [[BCLit]]
208	encodePrefixSumNaive = f	1✔
209	where
210	f [] !c = if c > 0 then [[]] else []	1✔
211	f ((0,_,_) : bss) c = f bss c	×
212	f ((b,i,ls) : bss) c =
213	[ [(i, ls, maximum ds' + 1)] \| not (null ds') ]	×
214	++
215	[ if d+1 > i then theta else (i, ls, d+1) : theta	×
216	\| d <- ds, theta <- f bss (fromIntegral (c - b * fromIntegral d))	1✔
217	]
218	where
219	bssMax = sum [b' * fromIntegral i' \| (b', i', _) <- bss]	1✔
220	bssMin = 0	1✔
221	ds = [d \| d <- [0..i], let bd = b * fromIntegral d, c - bssMax <= bd, bd < c - bssMin]	1✔
222	ds' = [d \| d <- [0..i], b * fromIntegral d < c - bssMax]	1✔
223
224	-- ------------------------------------------------------------------------
225
226	addPBLinAtLeastBCCNF :: PrimMonad m => Card.Encoder m -> PBLinAtLeast -> m ()
227	addPBLinAtLeastBCCNF enc constr = do	1✔
228	forM_ (encode constr) $ \clause -> do	1✔
229	addClause enc =<< mapM (Card.encodeAtLeast enc) clause	1✔
230
231	encodePBLinAtLeastWithPolarityBCCNF :: PrimMonad m => Card.Encoder m -> Tseitin.Polarity -> PBLinAtLeast -> m Lit
232	encodePBLinAtLeastWithPolarityBCCNF enc polarity constr = do	1✔
233	let tseitin = Card.getTseitinEncoder enc	1✔
234	ls <- forM (encode constr) $ \clause -> do	1✔
235	Tseitin.encodeDisjWithPolarity tseitin polarity =<< mapM (Card.encodeAtLeastWithPolarity enc polarity) clause	1✔
236	Tseitin.encodeConjWithPolarity tseitin polarity ls	1✔
237
238	-- ------------------------------------------------------------------------

msakai / toysolver / 496

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous