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

71.43

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

{-# 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
  , encodeAtLeastWithPolarity
  , getTseitinEncoder

    -- XXX
  , TotalizerDefinitions
  , getTotalizerDefinitions
  , evalTotalizerDefinitions

  -- * Polarity
  , Polarity (..)
  , negatePolarity
  , polarityPos
  , polarityNeg
  , polarityBoth
  , polarityNone
  ) where

import Control.Monad.Primitive
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Polarity (..), negatePolarity, polarityPos, polarityNeg, polarityBoth, polarityNone)
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 (Show, Eq, Ord, Enum, 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 tseitin = newEncoderWithStrategy tseitin ParallelCounter

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

type TotalizerDefinitions = Totalizer.Definitions

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

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

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

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

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

instance PrimMonad m => SAT.AddCardinality m (Encoder m) where
  addAtLeast (Encoder base@(Totalizer.Encoder tseitin _) strategy) lhs rhs
    | rhs <= 0  = return ()
    | otherwise =
        case strategy of
          Naive -> addAtLeastNaive tseitin (lhs,rhs)
          ParallelCounter -> addAtLeastParallelCounter tseitin (lhs,rhs)
          SequentialCounter -> BDD.addPBLinAtLeastBDD tseitin ([(1,l) | l <- lhs], fromIntegral rhs)
          Totalizer -> Totalizer.addAtLeast base (lhs,rhs)

encodeAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m SAT.Lit
encodeAtLeast enc = encodeAtLeastWithPolarity enc polarityBoth

encodeAtLeastWithPolarity :: PrimMonad m => Encoder m -> Polarity -> SAT.AtLeast -> m SAT.Lit
encodeAtLeastWithPolarity (Encoder base@(Totalizer.Encoder tseitin _) strategy) polarity =
  case strategy of
    Naive -> encodeAtLeastWithPolarityNaive tseitin polarity
    ParallelCounter -> encodeAtLeastWithPolarityParallelCounter tseitin polarity
    SequentialCounter -> \(lhs,rhs) -> BDD.encodePBLinAtLeastWithPolarityBDD tseitin polarity ([(1,l) | l <- lhs], fromIntegral rhs)
    Totalizer -> Totalizer.encodeAtLeastWithPolarity base polarity

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE FlexibleContexts #-}
4	{-# LANGUAGE FlexibleInstances #-}
5	{-# LANGUAGE MultiParamTypeClasses #-}
6	-----------------------------------------------------------------------------
7	-- \|
8	-- Module : ToySolver.SAT.Encoder.Cardinality
9	-- Copyright : (c) Masahiro Sakai 2019
10	-- License : BSD-style
11	--
12	-- Maintainer : masahiro.sakai@gmail.com
13	-- Stability : provisional
14	-- Portability : non-portable
15	--
16	-----------------------------------------------------------------------------
17	module ToySolver.SAT.Encoder.Cardinality
18	( Encoder
19	, Strategy (..)
20	, newEncoder
21	, newEncoderWithStrategy
22	, encodeAtLeast
23	, encodeAtLeastWithPolarity
24	, getTseitinEncoder
25
26	-- XXX
27	, TotalizerDefinitions
28	, getTotalizerDefinitions
29	, evalTotalizerDefinitions
30
31	-- * Polarity
32	, Polarity (..)
33	, negatePolarity
34	, polarityPos
35	, polarityNeg
36	, polarityBoth
37	, polarityNone
38	) where
39
40	import Control.Monad.Primitive
41	import qualified ToySolver.SAT.Types as SAT
42	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
43	import ToySolver.SAT.Encoder.Tseitin (Polarity (..), negatePolarity, polarityPos, polarityNeg, polarityBoth, polarityNone)
44	import ToySolver.SAT.Encoder.Cardinality.Internal.Naive
45	import ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
46	import ToySolver.SAT.Encoder.PB.Internal.BDD as BDD
47	import qualified ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer as Totalizer
48
49	-- -------------------------------------------------------------------
50
51	-- XXX
52	data Encoder m = Encoder (Totalizer.Encoder m) Strategy
53
54	data Strategy
55	= Naive
56	\| SequentialCounter
57	\| ParallelCounter
58	\| Totalizer
59	deriving (Show, Eq, Ord, Enum, Bounded)	×
60	{-
61	"Sequential Counter" from "Towards an Optimal CNF Encoding of Boolean
62	Cardinality Constraints" is a special case of BDD-based encoding of
63	"Translating Pseudo-Boolean Constraints into SAT" (using the fact C→B
64	to represent ite(A,B,C) as (A∧B)∨C instead of (A∧B)∨(¬A∧C))?
65
66	http://www.carstensinz.de/papers/CP-2005.pdf
67	http://www.st.ewi.tudelft.nl/jsat/content/volume2/JSAT2_1_Een.pdf
68	-}
69
70	newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
71	newEncoder tseitin = newEncoderWithStrategy tseitin ParallelCounter	×
72
73	newEncoderWithStrategy :: PrimMonad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
74	newEncoderWithStrategy tseitin strategy = do	1✔
75	base <- Totalizer.newEncoder tseitin	1✔
76	return $ Encoder base strategy	1✔
77
78	type TotalizerDefinitions = Totalizer.Definitions
79
80	getTotalizerDefinitions :: PrimMonad m => Encoder m -> m TotalizerDefinitions
81	getTotalizerDefinitions (Encoder base _) = Totalizer.getDefinitions base	1✔
82
83	evalTotalizerDefinitions :: SAT.IModel m => m -> TotalizerDefinitions -> [(SAT.Var, Bool)]
84	evalTotalizerDefinitions m defs = Totalizer.evalDefinitions m defs	1✔
85
86	getTseitinEncoder :: Encoder m -> Tseitin.Encoder m
87	getTseitinEncoder (Encoder (Totalizer.Encoder tseitin _) _) = tseitin	1✔
88
89	instance Monad m => SAT.NewVar m (Encoder m) where
90	newVar (Encoder base _) = SAT.newVar base	×
91	newVars (Encoder base _) = SAT.newVars base	×
92	newVars_ (Encoder base _) = SAT.newVars_ base	×
93
94	instance Monad m => SAT.AddClause m (Encoder m) where
95	addClause (Encoder base _) = SAT.addClause base	1✔
96
97	instance PrimMonad m => SAT.AddCardinality m (Encoder m) where	×
98	addAtLeast (Encoder base@(Totalizer.Encoder tseitin _) strategy) lhs rhs	1✔
99	\| rhs <= 0 = return ()	×
100	\| otherwise =	×
101	case strategy of	1✔
102	Naive -> addAtLeastNaive tseitin (lhs,rhs)	1✔
103	ParallelCounter -> addAtLeastParallelCounter tseitin (lhs,rhs)	1✔
104	SequentialCounter -> BDD.addPBLinAtLeastBDD tseitin ([(1,l) \| l <- lhs], fromIntegral rhs)	1✔
105	Totalizer -> Totalizer.addAtLeast base (lhs,rhs)	1✔
106
107	encodeAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m SAT.Lit
108	encodeAtLeast enc = encodeAtLeastWithPolarity enc polarityBoth	1✔
109
110	encodeAtLeastWithPolarity :: PrimMonad m => Encoder m -> Polarity -> SAT.AtLeast -> m SAT.Lit
111	encodeAtLeastWithPolarity (Encoder base@(Totalizer.Encoder tseitin _) strategy) polarity =	1✔
112	case strategy of	1✔
113	Naive -> encodeAtLeastWithPolarityNaive tseitin polarity	1✔
114	ParallelCounter -> encodeAtLeastWithPolarityParallelCounter tseitin polarity	1✔
115	SequentialCounter -> \(lhs,rhs) -> BDD.encodePBLinAtLeastWithPolarityBDD tseitin polarity ([(1,l) \| l <- lhs], fromIntegral rhs)	1✔
116	Totalizer -> Totalizer.encodeAtLeastWithPolarity base polarity	1✔

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