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

57.14

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

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.PB
-- 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
  ( Encoder (..)
  , newEncoder
  , newEncoderWithStrategy
  , encodePBLinAtLeast
  , encodePBLinAtLeastWithPolarity

  -- * Configulation
  , Strategy (..)
  , showStrategy
  , parseStrategy

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

import Control.Monad.Primitive
import Data.Char
import Data.Default.Class
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Cardinality as Card
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Polarity (..), negatePolarity, polarityPos, polarityNeg, polarityBoth, polarityNone)
import ToySolver.SAT.Encoder.PB.Internal.Adder (addPBLinAtLeastAdder, encodePBLinAtLeastWithPolarityAdder)
import ToySolver.SAT.Encoder.PB.Internal.BCCNF (addPBLinAtLeastBCCNF, encodePBLinAtLeastWithPolarityBCCNF)
import ToySolver.SAT.Encoder.PB.Internal.BDD (addPBLinAtLeastBDD, encodePBLinAtLeastWithPolarityBDD)
import ToySolver.SAT.Encoder.PB.Internal.Sorter (addPBLinAtLeastSorter, encodePBLinAtLeastSorter)

data Encoder m = Encoder (Card.Encoder m) Strategy

data Strategy
  = BDD
  | Adder
  | Sorter
  | BCCNF
  | Hybrid -- not implemented yet
  deriving (Show, Eq, Ord, Enum, Bounded)

instance Default Strategy where
  def = Hybrid

showStrategy :: Strategy -> String
showStrategy BDD = "bdd"
showStrategy Adder = "adder"
showStrategy Sorter = "sorter"
showStrategy BCCNF = "bccnf"
showStrategy Hybrid = "hybrid"

parseStrategy :: String -> Maybe Strategy
parseStrategy s =
  case map toLower s of
    "bdd"    -> Just BDD
    "adder"  -> Just Adder
    "sorter" -> Just Sorter
    "bccnf"  -> Just BCCNF
    "hybrid" -> Just Hybrid
    _ -> Nothing

newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
newEncoder tseitin = newEncoderWithStrategy tseitin Hybrid

newEncoderWithStrategy :: PrimMonad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy tseitin strategy = do
  card <- Card.newEncoderWithStrategy tseitin Card.SequentialCounter
  return (Encoder card strategy)

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

instance PrimMonad m => SAT.AddCardinality m (Encoder m) where
  addAtLeast enc lhs rhs = SAT.addPBAtLeast enc [(1, l) | l <- lhs] (fromIntegral rhs)

instance PrimMonad m => SAT.AddPBLin m (Encoder m) where
  addPBAtLeast enc lhs rhs = do
    let (lhs',rhs') = SAT.normalizePBLinAtLeast (lhs,rhs)
    if rhs' == 1 && and [c==1 | (c,_) <- lhs'] then
      SAT.addClause enc [l | (_,l) <- lhs']
    else do
      addPBLinAtLeast' enc (lhs',rhs')

encodePBLinAtLeast :: forall m. PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeast enc constr = encodePBLinAtLeastWithPolarity enc polarityBoth constr

encodePBLinAtLeastWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastWithPolarity enc polarity constr =
  encodePBLinAtLeastWithPolarity' enc polarity $ SAT.normalizePBLinAtLeast constr

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

addPBLinAtLeast' :: PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m ()
addPBLinAtLeast' (Encoder card strategy) = do
  let tseitin = Card.getTseitinEncoder card
  case strategy of
    Adder -> addPBLinAtLeastAdder tseitin
    Sorter -> addPBLinAtLeastSorter tseitin
    BCCNF -> addPBLinAtLeastBCCNF card
    _ -> addPBLinAtLeastBDD tseitin

encodePBLinAtLeastWithPolarity' :: PrimMonad m => Encoder m -> Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastWithPolarity' (Encoder card strategy) polarity constr = do
  let tseitin = Card.getTseitinEncoder card
  case strategy of
    Adder -> encodePBLinAtLeastWithPolarityAdder tseitin polarity constr
    Sorter -> encodePBLinAtLeastSorter tseitin constr
    BCCNF -> encodePBLinAtLeastWithPolarityBCCNF card polarity constr
    _ -> encodePBLinAtLeastWithPolarityBDD tseitin polarity constr

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


1	{-# LANGUAGE BangPatterns #-}
2	{-# LANGUAGE FlexibleInstances #-}
3	{-# LANGUAGE MultiParamTypeClasses #-}
4	{-# LANGUAGE ScopedTypeVariables #-}
5	{-# OPTIONS_GHC -Wall #-}
6	{-# OPTIONS_HADDOCK show-extensions #-}
7	-----------------------------------------------------------------------------
8	-- \|
9	-- Module : ToySolver.SAT.Encoder.PB
10	-- Copyright : (c) Masahiro Sakai 2016
11	-- License : BSD-style
12	--
13	-- Maintainer : masahiro.sakai@gmail.com
14	-- Stability : provisional
15	-- Portability : non-portable
16	--
17	-- References:
18	--
19	-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
20	-- Constraints into SAT. JSAT 2:1–26, 2006.
21	--
22	-----------------------------------------------------------------------------
23	module ToySolver.SAT.Encoder.PB
24	( Encoder (..)
25	, newEncoder
26	, newEncoderWithStrategy
27	, encodePBLinAtLeast
28	, encodePBLinAtLeastWithPolarity
29
30	-- * Configulation
31	, Strategy (..)
32	, showStrategy
33	, parseStrategy
34
35	-- * Polarity
36	, Polarity (..)
37	, negatePolarity
38	, polarityPos
39	, polarityNeg
40	, polarityBoth
41	, polarityNone
42	) where
43
44	import Control.Monad.Primitive
45	import Data.Char
46	import Data.Default.Class
47	import qualified ToySolver.SAT.Types as SAT
48	import qualified ToySolver.SAT.Encoder.Cardinality as Card
49	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
50	import ToySolver.SAT.Encoder.Tseitin (Polarity (..), negatePolarity, polarityPos, polarityNeg, polarityBoth, polarityNone)
51	import ToySolver.SAT.Encoder.PB.Internal.Adder (addPBLinAtLeastAdder, encodePBLinAtLeastWithPolarityAdder)
52	import ToySolver.SAT.Encoder.PB.Internal.BCCNF (addPBLinAtLeastBCCNF, encodePBLinAtLeastWithPolarityBCCNF)
53	import ToySolver.SAT.Encoder.PB.Internal.BDD (addPBLinAtLeastBDD, encodePBLinAtLeastWithPolarityBDD)
54	import ToySolver.SAT.Encoder.PB.Internal.Sorter (addPBLinAtLeastSorter, encodePBLinAtLeastSorter)
55
56	data Encoder m = Encoder (Card.Encoder m) Strategy
57
58	data Strategy
59	= BDD
60	\| Adder
61	\| Sorter
62	\| BCCNF
63	\| Hybrid -- not implemented yet
64	deriving (Show, Eq, Ord, Enum, Bounded)	×
65
66	instance Default Strategy where
67	def = Hybrid	1✔
68
69	showStrategy :: Strategy -> String
70	showStrategy BDD = "bdd"	×
71	showStrategy Adder = "adder"	×
72	showStrategy Sorter = "sorter"	×
73	showStrategy BCCNF = "bccnf"	×
74	showStrategy Hybrid = "hybrid"	×
75
76	parseStrategy :: String -> Maybe Strategy
77	parseStrategy s =	×
78	case map toLower s of	×
79	"bdd" -> Just BDD	×
80	"adder" -> Just Adder	×
81	"sorter" -> Just Sorter	×
82	"bccnf" -> Just BCCNF	×
83	"hybrid" -> Just Hybrid	×
84	_ -> Nothing	×
85
86	newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
87	newEncoder tseitin = newEncoderWithStrategy tseitin Hybrid	×
88
89	newEncoderWithStrategy :: PrimMonad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
90	newEncoderWithStrategy tseitin strategy = do	1✔
91	card <- Card.newEncoderWithStrategy tseitin Card.SequentialCounter	1✔
92	return (Encoder card strategy)	1✔
93
94	instance Monad m => SAT.NewVar m (Encoder m) where
95	newVar (Encoder a _) = SAT.newVar a	×
96	newVars (Encoder a _) = SAT.newVars a	×
97	newVars_ (Encoder a _) = SAT.newVars_ a	×
98
99	instance Monad m => SAT.AddClause m (Encoder m) where
100	addClause (Encoder a _) = SAT.addClause a	1✔
101
102	instance PrimMonad m => SAT.AddCardinality m (Encoder m) where	×
103	addAtLeast enc lhs rhs = SAT.addPBAtLeast enc [(1, l) \| l <- lhs] (fromIntegral rhs)	×
104
105	instance PrimMonad m => SAT.AddPBLin m (Encoder m) where	×
106	addPBAtLeast enc lhs rhs = do	1✔
107	let (lhs',rhs') = SAT.normalizePBLinAtLeast (lhs,rhs)	1✔
108	if rhs' == 1 && and [c==1 \| (c,_) <- lhs'] then	1✔
109	SAT.addClause enc [l \| (_,l) <- lhs']	1✔
110	else do	1✔
111	addPBLinAtLeast' enc (lhs',rhs')	1✔
112
113	encodePBLinAtLeast :: forall m. PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
114	encodePBLinAtLeast enc constr = encodePBLinAtLeastWithPolarity enc polarityBoth constr	1✔
115
116	encodePBLinAtLeastWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
117	encodePBLinAtLeastWithPolarity enc polarity constr =	1✔
118	encodePBLinAtLeastWithPolarity' enc polarity $ SAT.normalizePBLinAtLeast constr	1✔
119
120	-- -----------------------------------------------------------------------
121
122	addPBLinAtLeast' :: PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m ()
123	addPBLinAtLeast' (Encoder card strategy) = do	1✔
124	let tseitin = Card.getTseitinEncoder card	1✔
125	case strategy of	1✔
126	Adder -> addPBLinAtLeastAdder tseitin	1✔
127	Sorter -> addPBLinAtLeastSorter tseitin	1✔
128	BCCNF -> addPBLinAtLeastBCCNF card	1✔
129	_ -> addPBLinAtLeastBDD tseitin	1✔
130
131	encodePBLinAtLeastWithPolarity' :: PrimMonad m => Encoder m -> Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
132	encodePBLinAtLeastWithPolarity' (Encoder card strategy) polarity constr = do	1✔
133	let tseitin = Card.getTseitinEncoder card	1✔
134	case strategy of	1✔
135	Adder -> encodePBLinAtLeastWithPolarityAdder tseitin polarity constr	1✔
136	Sorter -> encodePBLinAtLeastSorter tseitin constr	1✔
137	BCCNF -> encodePBLinAtLeastWithPolarityBCCNF card polarity constr	1✔
138	_ -> encodePBLinAtLeastWithPolarityBDD tseitin polarity constr	1✔
139
140	-- -----------------------------------------------------------------------
141

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