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

84.82

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

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.PB.Internal.Sorter
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
--   Constraints into SAT. JSAT 2:1–26, 2006.
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.PB.Internal.Sorter
  ( Base
  , UDigit
  , UNumber
  , isRepresentable
  , encode
  , decode

  , Cost
  , optimizeBase

  , genSorterCircuit
  , sortVector

  , addPBLinAtLeastSorter
  , encodePBLinAtLeastSorter
  ) where

import Control.Monad
import Control.Monad.Primitive
import Control.Monad.State
import Control.Monad.Writer
import Data.List
import Data.Maybe
import Data.Ord
import Data.Vector (Vector, (!))
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import ToySolver.Data.Boolean
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))

-- ------------------------------------------------------------------------
-- Circuit-like implementation of Batcher's odd-even mergesort

genSorterCircuit :: Int -> [(Int,Int)]
genSorterCircuit len = execWriter (mergeSort (V.iterateN len (+1) 0)) []
  where
    genCompareAndSwap i j = tell ((i,j) :)

    mergeSort is
      | V.length is <= 1 = return ()
      | V.length is == 2 = genCompareAndSwap (is!0) (is!1)
      | otherwise =
          case halve is of
            (is1,is2) -> do
              mergeSort is1
              mergeSort is2
              oddEvenMerge is

    oddEvenMerge is
      | V.length is <= 1 = return ()
      | V.length is == 2 = genCompareAndSwap (is!0) (is!1)
      | otherwise =
          case splitOddEven is of
            (os,es) -> do
              oddEvenMerge os
              oddEvenMerge es
              forM_ [2,3 .. V.length is-1] $ \i -> do
                genCompareAndSwap (is!(i-1)) (is!i)

halve :: Vector a -> (Vector a, Vector a)
halve v
  | V.length v <= 1 = (v, V.empty)
  | otherwise = (V.slice 0 len1 v, V.slice len1 len2 v)
      where
        n = head $ dropWhile (< V.length v) $ iterate (*2) 1
        len1 = n `div` 2
        len2 = V.length v - len1

splitOddEven :: Vector a -> (Vector a, Vector a)
splitOddEven v = (V.generate len1 (\i -> v V.! (i*2+1)), V.generate len2 (\i -> v V.! (i*2)))
  where
    len1 = V.length v `div` 2
    len2 = (V.length v + 1) `div` 2

sortVector :: (Ord a) => Vector a -> Vector a
sortVector v = V.create $ do
  m <- V.thaw v
  forM_ (genSorterCircuit (V.length v)) $ \(i,j) -> do
    vi <- MV.read m i
    vj <- MV.read m j
    when (vi > vj) $ do
      MV.write m i vj
      MV.write m j vi
  return m

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

type Base = [Int]
type UDigit = Int
type UNumber = [UDigit]

isRepresentable :: Base -> Integer -> Bool
isRepresentable _ 0 = True
isRepresentable [] x = x <= fromIntegral (maxBound :: UDigit)
isRepresentable (b:bs) x = isRepresentable bs (x `div` fromIntegral b)

encode :: Base -> Integer -> UNumber
encode _ 0 = []
encode [] x
  | x <= fromIntegral (maxBound :: UDigit) = [fromIntegral x]
  | otherwise = undefined
encode (b:bs) x = fromIntegral (x `mod` fromIntegral b) : encode bs (x `div` fromIntegral b)

decode :: Base -> UNumber -> Integer
decode _ [] = 0
decode [] [x] = fromIntegral x
decode (b:bs) (x:xs) = fromIntegral x + fromIntegral b * decode bs xs

{-
test1 = encode [3,5] 164 -- [2,4,10]
test2 = decode [3,5] [2,4,10] -- 164

test3 = optimizeBase [1,1,2,2,3,3,3,3,7]
-}

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

type Cost = Integer

primes :: [Int]
primes = [2, 3, 5, 7, 11, 13, 17]

optimizeBase :: [Integer] -> Base
optimizeBase xs = reverse $ fst $ fromJust $ execState (m xs [] 0) Nothing
  where
    m :: [Integer] -> Base -> Integer -> State (Maybe (Base, Cost)) ()
    m xs base cost = do
      let lb = cost + sum [1 | x <- xs, x > 0]
      best <- get
      case best of
        Just (_bestBase, bestCost) | bestCost <= lb -> return ()
        _ -> do
          when (sum xs <= 1024) $ do
            let cost' = cost + sum xs
            case best of
              Just (_bestBase, bestCost) | bestCost < cost' -> return ()
              _ -> put $ Just (base, cost')
          unless (null xs) $ do
            let delta = sortBy (comparing snd) [(p, sum [x `mod` fromIntegral p | x <- xs]) | p <- primes]
            case delta of
              (p,0) : _ -> do
                m [d | x <- xs, let d = x `div` fromIntegral p, d > 0] (p : base) cost
              _ -> do
                forM_ delta $ \(p,s) -> do
                  m [d | x <- xs, let d = x `div` fromIntegral p, d > 0] (p : base) (cost + s)

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

addPBLinAtLeastSorter :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
addPBLinAtLeastSorter enc constr = do
  formula <- encodePBLinAtLeastSorter' enc constr
  Tseitin.addFormula enc formula

encodePBLinAtLeastSorter :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastSorter enc constr = do
  formula <- encodePBLinAtLeastSorter' enc constr
  Tseitin.encodeFormula enc formula

encodePBLinAtLeastSorter' :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m Tseitin.Formula
encodePBLinAtLeastSorter' enc (lhs,rhs) = do
  let base = optimizeBase [c | (c,_) <- lhs]
  if isRepresentable base rhs then do
    sorters <- genSorters enc base [(encode base c, l) | (c,l) <- lhs] []
    return $ lexComp base sorters (encode base rhs)
  else do
    return false

genSorters :: PrimMonad m => Tseitin.Encoder m -> Base -> [(UNumber, SAT.Lit)] -> [SAT.Lit] -> m [Vector SAT.Lit]
genSorters enc base lhs carry = do
  let is = V.fromList carry <> V.concat [V.replicate (fromIntegral d) l | (d:_,l) <- lhs, d /= 0]
  buf <- V.thaw is
  forM_ (genSorterCircuit (V.length is)) $ \(i,j) -> do
    vi <- MV.read buf i
    vj <- MV.read buf j
    MV.write buf i =<< Tseitin.encodeDisj enc [vi,vj]
    MV.write buf j =<< Tseitin.encodeConj enc [vi,vj]
  os <- V.freeze buf
  case base of
    [] -> return [os]
    b:bs -> do
      oss <- genSorters enc bs [(ds,l) | (_:ds,l) <- lhs] [os!(i-1) | i <- takeWhile (<= V.length os) (iterate (+b) b)]
      return $ os : oss

isGE :: Vector SAT.Lit -> Int -> Tseitin.Formula
isGE out lim
  | lim <= 0 = true
  | lim - 1 < V.length out = Atom $ out ! (lim - 1)
  | otherwise = false

isGEMod :: Int -> Vector SAT.Lit -> Int -> Tseitin.Formula
isGEMod _n _out lim | lim <= 0 = true
isGEMod n out lim =
  orB [isGE out (j + lim) .&&. notB isGE out (j + n) | j <- [0, n .. V.length out - 1]]

lexComp :: Base -> [Vector SAT.Lit] -> UNumber -> Tseitin.Formula
lexComp base lhs rhs = f true base lhs rhs
  where
    f ret (b:bs) (out:os) ds = f (gt .||. (ge .&&. ret)) bs os (drop 1 ds)
      where
        d = if null ds then 0 else head ds
        gt = isGEMod b out (d+1)
        ge = isGEMod b out d
    f ret [] [out] ds = gt .||. (ge .&&. ret)
      where
        d = if null ds then 0 else head ds
        gt = isGE out (d+1)
        ge = isGE out d

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

1	{-# LANGUAGE FlexibleContexts #-}
2	{-# LANGUAGE ScopedTypeVariables #-}
3	{-# OPTIONS_GHC -Wall #-}
4	{-# OPTIONS_HADDOCK show-extensions #-}
5	-----------------------------------------------------------------------------
6	-- \|
7	-- Module : ToySolver.SAT.Encoder.PB.Internal.Sorter
8	-- Copyright : (c) Masahiro Sakai 2016
9	-- License : BSD-style
10	--
11	-- Maintainer : masahiro.sakai@gmail.com
12	-- Stability : provisional
13	-- Portability : non-portable
14	--
15	-- References:
16	--
17	-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
18	-- Constraints into SAT. JSAT 2:1–26, 2006.
19	--
20	-----------------------------------------------------------------------------
21	module ToySolver.SAT.Encoder.PB.Internal.Sorter
22	( Base
23	, UDigit
24	, UNumber
25	, isRepresentable
26	, encode
27	, decode
28
29	, Cost
30	, optimizeBase
31
32	, genSorterCircuit
33	, sortVector
34
35	, addPBLinAtLeastSorter
36	, encodePBLinAtLeastSorter
37	) where
38
39	import Control.Monad
40	import Control.Monad.Primitive
41	import Control.Monad.State
42	import Control.Monad.Writer
43	import Data.List
44	import Data.Maybe
45	import Data.Ord
46	import Data.Vector (Vector, (!))
47	import qualified Data.Vector as V
48	import qualified Data.Vector.Mutable as MV
49	import ToySolver.Data.Boolean
50	import qualified ToySolver.SAT.Types as SAT
51	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
52	import ToySolver.SAT.Encoder.Tseitin (Formula (..))
53
54	-- ------------------------------------------------------------------------
55	-- Circuit-like implementation of Batcher's odd-even mergesort
56
57	genSorterCircuit :: Int -> [(Int,Int)]
58	genSorterCircuit len = execWriter (mergeSort (V.iterateN len (+1) 0)) []	1✔
59	where
60	genCompareAndSwap i j = tell ((i,j) :)	1✔
61
62	mergeSort is	1✔
63	\| V.length is <= 1 = return ()	×
64	\| V.length is == 2 = genCompareAndSwap (is!0) (is!1)	1✔
65	\| otherwise =	×
66	case halve is of	1✔
67	(is1,is2) -> do	1✔
68	mergeSort is1	1✔
69	mergeSort is2	1✔
70	oddEvenMerge is	1✔
71
72	oddEvenMerge is	1✔
73	\| V.length is <= 1 = return ()	×
74	\| V.length is == 2 = genCompareAndSwap (is!0) (is!1)	1✔
75	\| otherwise =	×
76	case splitOddEven is of	1✔
77	(os,es) -> do	1✔
78	oddEvenMerge os	1✔
79	oddEvenMerge es	1✔
80	forM_ [2,3 .. V.length is-1] $ \i -> do	1✔
81	genCompareAndSwap (is!(i-1)) (is!i)	1✔
82
83	halve :: Vector a -> (Vector a, Vector a)
84	halve v	1✔
85	\| V.length v <= 1 = (v, V.empty)	×
86	\| otherwise = (V.slice 0 len1 v, V.slice len1 len2 v)	×
87	where
88	n = head $ dropWhile (< V.length v) $ iterate (*2) 1	1✔
89	len1 = n `div` 2	1✔
90	len2 = V.length v - len1	1✔
91
92	splitOddEven :: Vector a -> (Vector a, Vector a)
93	splitOddEven v = (V.generate len1 (\i -> v V.! (i2+1)), V.generate len2 (\i -> v V.! (i2)))	1✔
94	where
95	len1 = V.length v `div` 2	1✔
96	len2 = (V.length v + 1) `div` 2	1✔
97
98	sortVector :: (Ord a) => Vector a -> Vector a
99	sortVector v = V.create $ do	1✔
100	m <- V.thaw v	1✔
101	forM_ (genSorterCircuit (V.length v)) $ \(i,j) -> do	1✔
102	vi <- MV.read m i	1✔
103	vj <- MV.read m j	1✔
104	when (vi > vj) $ do	1✔
105	MV.write m i vj	1✔
106	MV.write m j vi	1✔
107	return m	1✔
108
109	-- ------------------------------------------------------------------------
110
111	type Base = [Int]
112	type UDigit = Int
113	type UNumber = [UDigit]
114
115	isRepresentable :: Base -> Integer -> Bool
116	isRepresentable _ 0 = True	1✔
117	isRepresentable [] x = x <= fromIntegral (maxBound :: UDigit)	1✔
118	isRepresentable (b:bs) x = isRepresentable bs (x `div` fromIntegral b)	1✔
119
120	encode :: Base -> Integer -> UNumber
121	encode _ 0 = []	1✔
122	encode [] x
123	\| x <= fromIntegral (maxBound :: UDigit) = [fromIntegral x]	×
124	\| otherwise = undefined	×
125	encode (b:bs) x = fromIntegral (x `mod` fromIntegral b) : encode bs (x `div` fromIntegral b)	1✔
126
127	decode :: Base -> UNumber -> Integer
128	decode _ [] = 0	1✔
129	decode [] [x] = fromIntegral x	1✔
130	decode (b:bs) (x:xs) = fromIntegral x + fromIntegral b * decode bs xs	1✔
131
132	{-
133	test1 = encode [3,5] 164 -- [2,4,10]
134	test2 = decode [3,5] [2,4,10] -- 164
135
136	test3 = optimizeBase [1,1,2,2,3,3,3,3,7]
137	-}
138
139	-- ------------------------------------------------------------------------
140
141	type Cost = Integer
142
143	primes :: [Int]
144	primes = [2, 3, 5, 7, 11, 13, 17]	1✔
145
146	optimizeBase :: [Integer] -> Base
147	optimizeBase xs = reverse $ fst $ fromJust $ execState (m xs [] 0) Nothing	1✔
148	where
149	m :: [Integer] -> Base -> Integer -> State (Maybe (Base, Cost)) ()
150	m xs base cost = do	1✔
151	let lb = cost + sum [1 \| x <- xs, x > 0]	×
152	best <- get	1✔
153	case best of	1✔
154	Just (_bestBase, bestCost) \| bestCost <= lb -> return ()	×
155	_ -> do	1✔
156	when (sum xs <= 1024) $ do	1✔
157	let cost' = cost + sum xs	1✔
158	case best of	1✔
159	Just (_bestBase, bestCost) \| bestCost < cost' -> return ()	×
160	_ -> put $ Just (base, cost')	1✔
161	unless (null xs) $ do	1✔
162	let delta = sortBy (comparing snd) [(p, sum [x `mod` fromIntegral p \| x <- xs]) \| p <- primes]	1✔
163	case delta of	1✔
164	(p,0) : _ -> do	1✔
165	m [d \| x <- xs, let d = x `div` fromIntegral p, d > 0] (p : base) cost	×
166	_ -> do	1✔
167	forM_ delta $ \(p,s) -> do	1✔
168	m [d \| x <- xs, let d = x `div` fromIntegral p, d > 0] (p : base) (cost + s)	1✔
169
170	-- ------------------------------------------------------------------------
171
172	addPBLinAtLeastSorter :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
173	addPBLinAtLeastSorter enc constr = do	1✔
174	formula <- encodePBLinAtLeastSorter' enc constr	1✔
175	Tseitin.addFormula enc formula	1✔
176
177	encodePBLinAtLeastSorter :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
178	encodePBLinAtLeastSorter enc constr = do	1✔
179	formula <- encodePBLinAtLeastSorter' enc constr	1✔
180	Tseitin.encodeFormula enc formula	1✔
181
182	encodePBLinAtLeastSorter' :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m Tseitin.Formula
183	encodePBLinAtLeastSorter' enc (lhs,rhs) = do	1✔
184	let base = optimizeBase [c \| (c,_) <- lhs]	1✔
185	if isRepresentable base rhs then do	×
186	sorters <- genSorters enc base [(encode base c, l) \| (c,l) <- lhs] []	1✔
187	return $ lexComp base sorters (encode base rhs)	1✔
188	else do	×
189	return false	×
190
191	genSorters :: PrimMonad m => Tseitin.Encoder m -> Base -> [(UNumber, SAT.Lit)] -> [SAT.Lit] -> m [Vector SAT.Lit]
192	genSorters enc base lhs carry = do	1✔
193	let is = V.fromList carry <> V.concat [V.replicate (fromIntegral d) l \| (d:_,l) <- lhs, d /= 0]	1✔
194	buf <- V.thaw is	1✔
195	forM_ (genSorterCircuit (V.length is)) $ \(i,j) -> do	1✔
196	vi <- MV.read buf i	1✔
197	vj <- MV.read buf j	1✔
198	MV.write buf i =<< Tseitin.encodeDisj enc [vi,vj]	1✔
199	MV.write buf j =<< Tseitin.encodeConj enc [vi,vj]	1✔
200	os <- V.freeze buf	1✔
201	case base of	1✔
202	[] -> return [os]	1✔
203	b:bs -> do	1✔
204	oss <- genSorters enc bs [(ds,l) \| (_:ds,l) <- lhs] [os!(i-1) \| i <- takeWhile (<= V.length os) (iterate (+b) b)]	1✔
205	return $ os : oss	1✔
206
207	isGE :: Vector SAT.Lit -> Int -> Tseitin.Formula
208	isGE out lim	1✔
209	\| lim <= 0 = true	1✔
210	\| lim - 1 < V.length out = Atom $ out ! (lim - 1)	1✔
211	\| otherwise = false	×
212
213	isGEMod :: Int -> Vector SAT.Lit -> Int -> Tseitin.Formula
214	isGEMod _n _out lim \| lim <= 0 = true	1✔
215	isGEMod n out lim =
216	orB [isGE out (j + lim) .&&. notB isGE out (j + n) \| j <- [0, n .. V.length out - 1]]	1✔
217
218	lexComp :: Base -> [Vector SAT.Lit] -> UNumber -> Tseitin.Formula
219	lexComp base lhs rhs = f true base lhs rhs	1✔
220	where
221	f ret (b:bs) (out:os) ds = f (gt .\|\|. (ge .&&. ret)) bs os (drop 1 ds)	1✔
222	where
223	d = if null ds then 0 else head ds	×
224	gt = isGEMod b out (d+1)	1✔
225	ge = isGEMod b out d	1✔
226	f ret [] [out] ds = gt .\|\|. (ge .&&. ret)	1✔
227	where
228	d = if null ds then 0 else head ds	1✔
229	gt = isGE out (d+1)	1✔
230	ge = isGE out d	1✔
231
232	-- ------------------------------------------------------------------------

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