Support model counting and model enumeration

CHANGELOG.markdown

@@ -5,6 +5,7 @@
   * allow both min and max keywords in the objective function
   * allow any usual relational operator in constraints
   * allow to use Unicode characters and the UTF-8 encoding for relational operators
+  * support model counting and model enumeration
 
 0.1.11.0
 -------

src/Data/PseudoBoolean.hs

@@ -23,6 +23,8 @@ module Data.PseudoBoolean
   (
   -- * Abstract Syntax
     Formula (..)
+  , ModelCountingOrEnumeration (..)
+  , Objective
   , Constraint
   , Op (..)
   , SoftFormula (..)

src/Data/PseudoBoolean/Attoparsec.hs

@@ -58,11 +58,13 @@ formula :: Parser Formula
 formula = do
   h <- optionMaybe hint
   sequence_of_comments
+  countOrEnum <- optionMaybe (count_or_enum_header <* sequence_of_comments)
   obj <- optionMaybe objective
   cs <- sequence_of_comments_or_constraints
   return $
     Formula
-    { pbObjectiveFunction = obj
+    { pbModelCountingOrEnumeration = countOrEnum
+    , pbObjectiveFunction = obj
     , pbConstraints = cs
     , pbNumVars = fromMaybe (pbComputeNumVars (fmap snd obj) cs) (fmap fst h)
     , pbNumConstraints = fromMaybe (length cs) (fmap snd h)
@@ -219,6 +221,32 @@ oneOrMoreLiterals = do
 literal :: Parser Lit
 literal = variablename <|> (char '~' >> liftM negate variablename)
 
+count_or_enum_header :: Parser (ModelCountingOrEnumeration, Maybe [Lit])
+count_or_enum_header = msum
+  [ do _ <- string "models:"
+       zeroOrMoreSpace
+       countOrEnum <- (string "count" >> pure ModelCounting) <|> (string "enumerate" >> pure ModelEnumeration)
+       zeroOrMoreSpace
+       semi
+       lits <- optionMaybe $ do
+         sequence_of_comments
+         _ <- string "project:"
+         zeroOrMoreSpace
+         lits <- oneOrMoreLiterals <|> pure []
+         zeroOrMoreSpace
+         semi
+         return lits
+       return (countOrEnum, lits)
+  , do countOrEnum <- (string "count" >> pure ModelCounting) <|> (string "enum" >> pure ModelEnumeration)
+       _ <- char ':'
+       zeroOrMoreSpace
+       lits <- oneOrMoreLiterals <|> pure []
+       zeroOrMoreSpace
+       semi
+       return (countOrEnum, if null lits then Nothing else Just lits)
+  ]
+
+
 -- | Parse a OPB format string containing pseudo boolean problem.
 parseOPBByteString :: BSLazy.ByteString -> Either String Formula
 parseOPBByteString s = L.eitherResult $ L.parse (formula <* endOfInput) s

src/Data/PseudoBoolean/Builder.hs

@@ -34,7 +34,7 @@ import Data.PseudoBoolean.Types
 
 -- | A builder which renders a OPB format in any String-like 'Monoid'.
 opbBuilder :: (Monoid a, IsString a) => Formula -> a
-opbBuilder opb = (size <> part1 <> part2)
+opbBuilder opb = size <> part1 <> part2 <> part3
   where
     nv = pbNumVars opb
     nc = pbNumConstraints opb
@@ -44,15 +44,27 @@ opbBuilder opb = (size <> part1 <> part2)
     size = fromString (printf "* #variable= %d #constraint= %d" nv nc)
          <> (if np >= 1 then fromString (printf " #product= %d sizeproduct= %d" np sp) else mempty)
          <> fromString "\n"
-    part1 = 
+    part1 =
+      case pbModelCountingOrEnumeration opb of
+        Nothing -> mempty
+        Just (prob, mlits) ->
+          fromString "models: "
+          <> (case prob of
+                ModelCounting -> fromString "count"
+                ModelEnumeration -> fromString "enumerate")
+          <> fromString " ;\n"
+          <> (case mlits of
+                Nothing -> mempty
+                Just lits -> fromString "project: " <> foldr (\f g -> f <> fromString " " <> g) mempty (map showLit lits) <> fromString ";\n")
+    part2 =
       case pbObjectiveFunction opb of
         Nothing -> mempty
         Just (dir, o) ->
           (case dir of
             OptMin -> fromString "min"
             OptMax -> fromString "max")
           <> fromString ": " <> showSum o <> fromString ";\n"
-    part2 = mconcat $ map showConstraint (pbConstraints opb)
+    part3 = mconcat $ map showConstraint (pbConstraints opb)
 
 -- | A builder which renders a WBO format in any String-like 'Monoid'.
 wboBuilder :: (Monoid a, IsString a) => SoftFormula -> a

src/Data/PseudoBoolean/ByteStringBuilder.hs

@@ -40,7 +40,7 @@ import Data.PseudoBoolean.Types
 
 -- | A ByteString Builder which renders a OPB format byte-string containing pseudo boolean problem.
 opbBuilder :: Formula -> Builder
-opbBuilder opb = (size <> part1 <> part2)
+opbBuilder opb = (size <> part1 <> part2 <> part3)
   where
     nv = pbNumVars opb
     nc = pbNumConstraints opb
@@ -50,15 +50,28 @@ opbBuilder opb = (size <> part1 <> part2)
     size = string7 "* #variable= " <> intDec nv <> string7 " #constraint= " <> intDec nc
          <> (if np >= 1 then string7 " #product= " <> intDec np <> string7 " sizeproduct= " <> intDec sp else mempty)
          <> char7 '\n'
-    part1 = 
+    part1 =
+      case pbModelCountingOrEnumeration opb of
+        Nothing -> mempty
+        Just (prob, mlits) ->
+          string7 "models: "
+          <> (case prob of
+                ModelCounting -> string7 "count"
+                ModelEnumeration -> string7 "enumerate")
+          <> string7 " ;\n"
+          <> (case mlits of
+                Nothing -> mempty
+                Just lits -> string7 "project: " <> foldr (\f g -> f <> char7 ' ' <> g) mempty (map showLit lits) <> string7 ";\n")
+
+    part2 =
       case pbObjectiveFunction opb of
         Nothing -> mempty
         Just (dir, o) ->
           (case dir of
             OptMin -> string7 "min"
             OptMax -> string7 "max")
           <> string7 ": " <> showSum o <> string7 ";\n"
-    part2 = mconcat $ map showConstraint (pbConstraints opb)
+    part3 = mconcat $ map showConstraint (pbConstraints opb)
 
 -- | A ByteString Builder which renders a WBO format byte-string containing weighted boolean optimization problem.
 wboBuilder :: SoftFormula -> Builder

src/Data/PseudoBoolean/Megaparsec.hs

@@ -77,11 +77,13 @@ formula :: C e s m => m Formula
 formula = do
   h <- optional hint
   sequence_of_comments
+  countOrEnum <- optional (count_or_enum_header <* sequence_of_comments)
   obj <- optional objective
   cs <- sequence_of_comments_or_constraints
   return $
     Formula
-    { pbObjectiveFunction = obj
+    { pbModelCountingOrEnumeration = countOrEnum
+    , pbObjectiveFunction = obj
     , pbConstraints = cs
     , pbNumVars = fromMaybe (pbComputeNumVars (fmap snd obj) cs) (fmap fst h)
     , pbNumConstraints = fromMaybe (length cs) (fmap snd h)
@@ -236,6 +238,31 @@ oneOrMoreLiterals = do
 literal :: C e s m => m Lit
 literal = variablename <|> (char8 '~' >> liftM negate variablename)
 
+count_or_enum_header :: C e s m => m (ModelCountingOrEnumeration, Maybe [Lit])
+count_or_enum_header = msum
+  [ do _ <- string "models:"
+       zeroOrMoreSpace
+       countOrEnum <- (string "count" >> pure ModelCounting) <|> (string "enumerate" >> pure ModelEnumeration)
+       zeroOrMoreSpace
+       semi
+       lits <- optional $ do
+         sequence_of_comments
+         _ <- string "project:"
+         zeroOrMoreSpace
+         lits <- oneOrMoreLiterals <|> pure []
+         zeroOrMoreSpace
+         semi
+         return lits
+       return (countOrEnum, lits)
+  , do countOrEnum <- (string "count" >> pure ModelCounting) <|> (string "enum" >> pure ModelEnumeration)
+       _ <- char8 ':'
+       zeroOrMoreSpace
+       lits <- oneOrMoreLiterals <|> pure []
+       zeroOrMoreSpace
+       semi
+       return (countOrEnum, if null lits then Nothing else Just lits)
+  ]
+
 type ParseError = MP.ParseErrorBundle BL.ByteString Void
 
 -- | Parse a OPB format string containing pseudo boolean problem.

src/Data/PseudoBoolean/Parsec.hs

@@ -57,11 +57,13 @@ formula :: Stream s m Char => ParsecT s u m Formula
 formula = do
   h <- optionMaybe hint
   sequence_of_comments
+  countOrEnum <- optionMaybe (try count_or_enum_header <* sequence_of_comments)
   obj <- optionMaybe objective
   cs <- sequence_of_comments_or_constraints
   return $
     Formula
-    { pbObjectiveFunction = obj
+    { pbModelCountingOrEnumeration = countOrEnum
+    , pbObjectiveFunction = obj
     , pbConstraints = cs
     , pbNumVars = fromMaybe (pbComputeNumVars (fmap snd obj) cs) (fmap fst h)
     , pbNumConstraints = fromMaybe (length cs) (fmap snd h)
@@ -216,6 +218,32 @@ oneOrMoreLiterals = do
 literal :: Stream s m Char => ParsecT s u m Lit
 literal = variablename <|> (char '~' >> liftM negate variablename)
 
+count_or_enum_header :: Stream s m Char => ParsecT s u m (ModelCountingOrEnumeration, Maybe [Lit])
+count_or_enum_header = msum
+  [ do _ <- string "models:"
+       zeroOrMoreSpace
+       countOrEnum <- (string "count" >> pure ModelCounting) <|> (string "enumerate" >> pure ModelEnumeration)
+       zeroOrMoreSpace
+       semi
+       lits <- optionMaybe $ try $ do
+         sequence_of_comments
+         _ <- string "project:"
+         zeroOrMoreSpace
+         lits <- oneOrMoreLiterals <|> pure []
+         zeroOrMoreSpace
+         semi
+         return lits
+       return (countOrEnum, lits)
+  , do countOrEnum <- (string "count" >> pure ModelCounting) <|> (string "enum" >> pure ModelEnumeration)
+       _ <- char ':'
+       zeroOrMoreSpace
+       lits <- oneOrMoreLiterals <|> pure []
+       zeroOrMoreSpace
+       semi
+       return (countOrEnum, if null lits then Nothing else Just lits)
+  ]
+
+
 -- | Parse a OPB format string containing pseudo boolean problem.
 parseOPBString :: SourceName -> String -> Either ParseError Formula
 parseOPBString = parse (formula <* eof)

src/Data/PseudoBoolean/Types.hs

@@ -21,6 +21,7 @@ module Data.PseudoBoolean.Types
   (
   -- * Abstract Syntax
     Formula (..)
+  , ModelCountingOrEnumeration (..)
   , Objective
   , Constraint
   , OptDir (..)
@@ -56,7 +57,8 @@ import Data.Maybe
 -- | Pair of /objective function/ and a list of constraints.
 data Formula
   = Formula
-  { pbObjectiveFunction :: Maybe Objective
+  { pbModelCountingOrEnumeration :: Maybe (ModelCountingOrEnumeration, Maybe [Lit])
+  , pbObjectiveFunction :: Maybe Objective
   , pbConstraints :: [Constraint]
   , pbNumVars :: !Int
   , pbNumConstraints :: !Int
@@ -66,6 +68,15 @@ data Formula
 instance NFData Formula
 instance Hashable Formula
 
+-- | Specifier for model counting/enumeration problems
+data ModelCountingOrEnumeration
+  = ModelCounting
+  | ModelEnumeration
+  deriving (Eq, Ord, Show, Read, Enum, Bounded, Typeable, Data, Generic)
+
+instance NFData ModelCountingOrEnumeration
+instance Hashable ModelCountingOrEnumeration
+
 -- | Objective type and sum of weighted terms.
 type Objective = (OptDir, Sum)
 

test/TestPBFile.hs

@@ -13,17 +13,17 @@
 import qualified Data.PseudoBoolean.Megaparsec as M
 import Data.PseudoBoolean.Internal.TextUtil
 
 case_exampleLIN  = checkOPBString "exampleLIN"  exampleLIN
 case_exampleNLC1 = checkOPBString "exampleNLC1" exampleNLC1
 case_exampleNLC2 = checkOPBString "exampleNLC2" exampleNLC2
 case_exampleWBO1 = checkWBOString "exampleWBO1" exampleWBO1
 case_exampleWBO2 = checkWBOString "exampleWBO2" exampleWBO2
 case_exampleWBO3 = checkWBOString "exampleWBO3" exampleWBO3
 
 case_exampleLIN_file  = checkOPBFile "test/samples/example-lin.opb"
 case_exampleNLC1_file = checkOPBFile "test/samples/example-nlc-1.opb"
 case_exampleNLC2_file = checkOPBFile "test/samples/example-nlc-2.opb"
 case_exampleWBO1_file = checkWBOFile "test/samples/example1.wbo"
 case_exampleWBO2_file = checkWBOFile "test/samples/example2.wbo"
 case_exampleWBO3_file = checkWBOFile "test/samples/example3.wbo"
 
@@ -48,11 +48,22 @@
 case_invalid_lhs_empty_sum_wbo = checkWBOFile "test/samples/invalid-lhs-empty-sum.wbo"
 
 case_general_testlin_max_file  = checkOPBFile "test/samples/general/testlin-max.pb"
+
 case_general_relational_operator_file  = checkOPBFile "test/samples/general/test-relational-operator.pb"
 case_general_relational_operator_unicode_file  = checkOPBFile "test/samples/general/test-relational-operator-unicode.pb"
 case_general_relational_operator = checkOPBString "general relational operator" exampleGeneralRelationalOperator
 case_general_relational_operator_unicode = checkOPBString "general relational operator unicode" exampleGeneralRelationalOperatorUnicode
 
+case_general_enum_file = checkOPBFile "test/samples/general/test-enum.opb"
+case_general_enum_2_file = checkOPBFile "test/samples/general/test-enum-2.opb"
+case_general_enum_proj_file = checkOPBFile "test/samples/general/test-enum-proj.opb"
+case_general_enum_proj_2_file = checkOPBFile "test/samples/general/test-enum-proj-2.opb"
+
+case_general_count_file = checkOPBFile "test/samples/general/test-count.opb"
+case_general_count_2_file = checkOPBFile "test/samples/general/test-count-2.opb"
+case_general_count_proj_file = checkOPBFile "test/samples/general/test-count-proj.opb"
+case_general_count_proj_2_file = checkOPBFile "test/samples/general/test-count-proj-2.opb"
+
 case_general_relational_operator_unicode_equivalence = do
   Right expected <- parseOPBFile "test/samples/general/test-relational-operator.pb"
   Right opbP <- parseOPBFile "test/samples/general/test-relational-operator-unicode.pb"

test/samples/general/test-count-2.opb

@@ -0,0 +1,7 @@
+* request model counting on all variables
+count: ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;

test/samples/general/test-count-proj-2.opb

@@ -0,0 +1,7 @@
+* request model counting on x1, x3 and x3
+count: x1 x2 x3 ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;

test/samples/general/test-count-proj.opb

@@ -0,0 +1,8 @@
+* comment
+models: count ;
+project: x1 x2 x3 ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;

test/samples/general/test-count.opb

@@ -0,0 +1,7 @@
+* comment
+models: count ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;

test/samples/general/test-enum-2.opb

@@ -0,0 +1,7 @@
+* request model emumeration on all variables
+enum: ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;

test/samples/general/test-enum-proj-2.opb

@@ -0,0 +1,7 @@
+* request model enumeration on x1, x3 and x3
+enum: x1 x2 x3 ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;

test/samples/general/test-enum-proj.opb

@@ -0,0 +1,10 @@
+* comment
+
+models: enumerate ;
+
+project: x1 x2 x3 ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;

test/samples/general/test-enum.opb

@@ -0,0 +1,7 @@
+* comment
+models: enumerate ;
+1 x1 +4 x2 -2 x5 >= 2;
+-1 x1 +4 x2 -2 x5 >= +3;
+12345678901234567890 x4 +4 x3 >= 10;
+* an equality constraint
+2 x2 +3 x4 +2 x1 +3 x5 = 5;