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

85.14

/src/ToySolver/SAT/Encoder/Cardinality/Internal/Totalizer.hs

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

  , Definitions
  , getDefinitions
  , evalDefinitions

  , addAtLeast
  , encodeAtLeastWithPolarity

  , addCardinality
  , encodeCardinalityWithPolarity

  , encodeSum
  ) where

import Control.Monad
import Control.Monad.Primitive
import Control.Monad.State.Strict
import qualified Data.IntSet as IntSet
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Primitive.MutVar
import Data.Vector.Unboxed (Vector)
import qualified Data.Vector.Unboxed as V
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin


data Encoder m = Encoder (Tseitin.Encoder m) (MutVar (PrimState m) (Map SAT.LitSet (Vector SAT.Var)))

instance Monad m => SAT.NewVar m (Encoder m) where
  newVar   (Encoder a _) = SAT.newVar a
  newVars  (Encoder a _) = SAT.newVars a
  newVars_ (Encoder a _) = SAT.newVars_ a

instance Monad m => SAT.AddClause m (Encoder m) where
  addClause (Encoder a _) = SAT.addClause a

newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
newEncoder tseitin = do
  tableRef <- newMutVar Map.empty
  return $ Encoder tseitin tableRef


type Definitions = [(Vector SAT.Var, SAT.LitSet)]

getDefinitions :: PrimMonad m => Encoder m -> m Definitions
getDefinitions (Encoder _ tableRef) = do
  m <- readMutVar tableRef
  return [(vars', lits) | (lits, vars') <- Map.toList m]


evalDefinitions :: SAT.IModel m => m -> Definitions -> [(SAT.Var, Bool)]
evalDefinitions m defs = do
  (vars', lits) <- defs
  let n = length [() | l <- IntSet.toList lits, SAT.evalLit m l]
  (i, v) <- zip [1..] (V.toList vars')
  return (v, i <= n)


addAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m ()
addAtLeast enc (lhs, rhs) = do
  addCardinality enc lhs (rhs, length lhs)


addCardinality :: PrimMonad m => Encoder m -> [SAT.Lit] -> (Int, Int) -> m ()
addCardinality enc lits (lb, ub) = do
  let n = length lits
  if lb <= 0 && n <= ub then
    return ()
  else if n < lb || ub < 0 then
    SAT.addClause enc []
  else do
    lits' <- encodeSum enc lits
    forM_ (take lb lits') $ \l -> SAT.addClause enc [l]
    forM_ (drop ub lits') $ \l -> SAT.addClause enc [- l]



encodeAtLeastWithPolarity :: PrimMonad m => Encoder m -> Tseitin.Polarity -> SAT.AtLeast -> m SAT.Lit
encodeAtLeastWithPolarity enc polarity (lhs,rhs) = do
  encodeCardinalityWithPolarity enc polarity lhs (rhs, length lhs)


encodeCardinalityWithPolarity :: PrimMonad m => Encoder m -> Tseitin.Polarity -> [SAT.Lit] -> (Int, Int) -> m SAT.Lit
encodeCardinalityWithPolarity enc@(Encoder tseitin _) polarity lits (lb, ub) = do
  let n = length lits
  if lb <= 0 && n <= ub then
    Tseitin.encodeConjWithPolarity tseitin polarity []
  else if n < lb || ub < 0 then
    Tseitin.encodeDisjWithPolarity tseitin polarity []
  else do
    lits' <- encodeSum enc lits
    forM_ (zip lits' (tail lits')) $ \(l1, l2) -> do
      SAT.addClause enc [-l2, l1] -- l2→l1 or equivalently ¬l1→¬l2
    Tseitin.encodeConjWithPolarity tseitin polarity $
      [lits' !! (lb - 1) | lb > 0] ++ [- (lits' !! (ub + 1 - 1)) | ub < n]


encodeSum :: PrimMonad m => Encoder m -> [SAT.Lit] -> m [SAT.Lit]
encodeSum enc = liftM V.toList . encodeSumV enc . V.fromList


encodeSumV :: PrimMonad m => Encoder m -> Vector SAT.Lit -> m (Vector SAT.Lit)
encodeSumV (Encoder enc tableRef) = f
  where
    f lits
      | n <= 1 = return lits
      | otherwise = do
          m <- readMutVar tableRef
          let key = IntSet.fromList (V.toList lits)
          case Map.lookup key m of
            Just vars -> return vars
            Nothing -> do
              rs <- liftM V.fromList $ SAT.newVars enc n
              writeMutVar tableRef (Map.insert key rs m)
              case V.splitAt n1 lits of
                (lits1, lits2) -> do
                  lits1' <- f lits1
                  lits2' <- f lits2
                  forM_ [0 .. n] $ \sigma ->
                    -- a + b = sigma, 0 <= a <= n1, 0 <= b <= n2
                    forM_ [max 0 (sigma - n2) .. min n1 sigma] $ \a -> do
                      let b = sigma - a
                      -- card(lits1) >= a ∧ card(lits2) >= b → card(lits) >= sigma
                      -- ¬(card(lits1) >= a) ∨ ¬(card(lits2) >= b) ∨ card(lits) >= sigma
                      unless (sigma == 0) $ do
                        SAT.addClause enc $
                          [- (lits1' V.! (a - 1)) | a > 0] ++
                          [- (lits2' V.! (b - 1)) | b > 0] ++
                          [rs V.! (sigma - 1)]
                      -- card(lits) > sigma → (card(lits1) > a ∨ card(lits2) > b)
                      -- card(lits) >= sigma+1 → (card(lits1) >= a+1 ∨ card(lits2) >= b+1)
                      -- card(lits1) >= a+1 ∨ card(lits2) >= b+1 ∨ ¬(card(lits) >= sigma+1)
                      unless (sigma + 1 == n + 1) $ do
                        SAT.addClause enc $
                          [lits1' V.! (a + 1 - 1) | a + 1 < n1 + 1] ++
                          [lits2' V.! (b + 1 - 1) | b + 1 < n2 + 1] ++
                          [- (rs V.! (sigma + 1 - 1))]
                  return rs
     where
       n = V.length lits
       n1 = n `div` 2
       n2 = n - n1


1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE BangPatterns #-}
4	{-# LANGUAGE FlexibleInstances #-}
5	{-# LANGUAGE MultiParamTypeClasses #-}
6	{-# LANGUAGE ScopedTypeVariables #-}
7	-----------------------------------------------------------------------------
8	-- \|
9	-- Module : ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer
10	-- Copyright : (c) Masahiro Sakai 2020
11	-- License : BSD-style
12	--
13	-- Maintainer : masahiro.sakai@gmail.com
14	-- Stability : provisional
15	-- Portability : non-portable
16	--
17	-----------------------------------------------------------------------------
18	module ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer
19	( Encoder (..)
20	, newEncoder
21
22	, Definitions
23	, getDefinitions
24	, evalDefinitions
25
26	, addAtLeast
27	, encodeAtLeastWithPolarity
28
29	, addCardinality
30	, encodeCardinalityWithPolarity
31
32	, encodeSum
33	) where
34
35	import Control.Monad
36	import Control.Monad.Primitive
37	import Control.Monad.State.Strict
38	import qualified Data.IntSet as IntSet
39	import Data.Map.Strict (Map)
40	import qualified Data.Map.Strict as Map
41	import Data.Primitive.MutVar
42	import Data.Vector.Unboxed (Vector)
43	import qualified Data.Vector.Unboxed as V
44	import qualified ToySolver.SAT.Types as SAT
45	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
46
47
48	data Encoder m = Encoder (Tseitin.Encoder m) (MutVar (PrimState m) (Map SAT.LitSet (Vector SAT.Var)))
49
50	instance Monad m => SAT.NewVar m (Encoder m) where
51	newVar (Encoder a _) = SAT.newVar a	×
52	newVars (Encoder a _) = SAT.newVars a	×
53	newVars_ (Encoder a _) = SAT.newVars_ a	×
54
55	instance Monad m => SAT.AddClause m (Encoder m) where
56	addClause (Encoder a _) = SAT.addClause a	1✔
57
58	newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
59	newEncoder tseitin = do	1✔
60	tableRef <- newMutVar Map.empty	1✔
61	return $ Encoder tseitin tableRef	1✔
62
63
64	type Definitions = [(Vector SAT.Var, SAT.LitSet)]
65
66	getDefinitions :: PrimMonad m => Encoder m -> m Definitions
67	getDefinitions (Encoder _ tableRef) = do	1✔
68	m <- readMutVar tableRef	1✔
69	return [(vars', lits) \| (lits, vars') <- Map.toList m]	1✔
70
71
72	evalDefinitions :: SAT.IModel m => m -> Definitions -> [(SAT.Var, Bool)]
73	evalDefinitions m defs = do	1✔
74	(vars', lits) <- defs	1✔
75	let n = length [() \| l <- IntSet.toList lits, SAT.evalLit m l]	×
76	(i, v) <- zip [1..] (V.toList vars')	1✔
77	return (v, i <= n)	1✔
78
79
80	addAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m ()
81	addAtLeast enc (lhs, rhs) = do	1✔
82	addCardinality enc lhs (rhs, length lhs)	1✔
83
84
85	addCardinality :: PrimMonad m => Encoder m -> [SAT.Lit] -> (Int, Int) -> m ()
86	addCardinality enc lits (lb, ub) = do	1✔
87	let n = length lits	1✔
88	if lb <= 0 && n <= ub then	×
89	return ()	×
90	else if n < lb \|\| ub < 0 then	1✔
91	SAT.addClause enc []	1✔
92	else do	1✔
93	lits' <- encodeSum enc lits	1✔
94	forM_ (take lb lits') $ \l -> SAT.addClause enc [l]	1✔
95	forM_ (drop ub lits') $ \l -> SAT.addClause enc [- l]	×
96
97
98
99	encodeAtLeastWithPolarity :: PrimMonad m => Encoder m -> Tseitin.Polarity -> SAT.AtLeast -> m SAT.Lit
100	encodeAtLeastWithPolarity enc polarity (lhs,rhs) = do	1✔
101	encodeCardinalityWithPolarity enc polarity lhs (rhs, length lhs)	1✔
102
103
104	encodeCardinalityWithPolarity :: PrimMonad m => Encoder m -> Tseitin.Polarity -> [SAT.Lit] -> (Int, Int) -> m SAT.Lit
105	encodeCardinalityWithPolarity enc@(Encoder tseitin _) polarity lits (lb, ub) = do	1✔
106	let n = length lits	1✔
107	if lb <= 0 && n <= ub then	1✔
108	Tseitin.encodeConjWithPolarity tseitin polarity []	1✔
109	else if n < lb \|\| ub < 0 then	1✔
110	Tseitin.encodeDisjWithPolarity tseitin polarity []	1✔
111	else do	1✔
112	lits' <- encodeSum enc lits	1✔
113	forM_ (zip lits' (tail lits')) $ \(l1, l2) -> do	1✔
114	SAT.addClause enc [-l2, l1] -- l2→l1 or equivalently ¬l1→¬l2	1✔
115	Tseitin.encodeConjWithPolarity tseitin polarity $	×
116	[lits' !! (lb - 1) \| lb > 0] ++ [- (lits' !! (ub + 1 - 1)) \| ub < n]	×
117
118
119	encodeSum :: PrimMonad m => Encoder m -> [SAT.Lit] -> m [SAT.Lit]
120	encodeSum enc = liftM V.toList . encodeSumV enc . V.fromList	1✔
121
122
123	encodeSumV :: PrimMonad m => Encoder m -> Vector SAT.Lit -> m (Vector SAT.Lit)
124	encodeSumV (Encoder enc tableRef) = f	1✔
125	where
126	f lits	1✔
127	\| n <= 1 = return lits	1✔
128	\| otherwise = do	×
129	m <- readMutVar tableRef	1✔
130	let key = IntSet.fromList (V.toList lits)	1✔
131	case Map.lookup key m of	1✔
132	Just vars -> return vars	×
133	Nothing -> do	1✔
134	rs <- liftM V.fromList $ SAT.newVars enc n	1✔
135	writeMutVar tableRef (Map.insert key rs m)	1✔
136	case V.splitAt n1 lits of	1✔
137	(lits1, lits2) -> do	1✔
138	lits1' <- f lits1	1✔
139	lits2' <- f lits2	1✔
140	forM_ [0 .. n] $ \sigma ->	1✔
141	-- a + b = sigma, 0 <= a <= n1, 0 <= b <= n2
142	forM_ [max 0 (sigma - n2) .. min n1 sigma] $ \a -> do	1✔
143	let b = sigma - a	1✔
144	-- card(lits1) >= a ∧ card(lits2) >= b → card(lits) >= sigma
145	-- ¬(card(lits1) >= a) ∨ ¬(card(lits2) >= b) ∨ card(lits) >= sigma
146	unless (sigma == 0) $ do	1✔
147	SAT.addClause enc $	1✔
148	[- (lits1' V.! (a - 1)) \| a > 0] ++	1✔
149	[- (lits2' V.! (b - 1)) \| b > 0] ++	1✔
150	[rs V.! (sigma - 1)]	1✔
151	-- card(lits) > sigma → (card(lits1) > a ∨ card(lits2) > b)
152	-- card(lits) >= sigma+1 → (card(lits1) >= a+1 ∨ card(lits2) >= b+1)
153	-- card(lits1) >= a+1 ∨ card(lits2) >= b+1 ∨ ¬(card(lits) >= sigma+1)
154	unless (sigma + 1 == n + 1) $ do	1✔
155	SAT.addClause enc $	1✔
156	[lits1' V.! (a + 1 - 1) \| a + 1 < n1 + 1] ++	1✔
157	[lits2' V.! (b + 1 - 1) \| b + 1 < n2 + 1] ++	1✔
158	[- (rs V.! (sigma + 1 - 1))]	1✔
159	return rs	1✔
160	where
161	n = V.length lits	1✔
162	n1 = n `div` 2	1✔
163	n2 = n - n1	1✔
164

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