add BCCNF strategy to ToySolver.SAT.Encoder.PB

msakai · Aug 7, 2022 · d8c4ab6 · d8c4ab6
1 parent 711182d
commit d8c4ab6
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 9 deletions.
diff --git a/src/ToySolver/SAT/Encoder/Cardinality.hs b/src/ToySolver/SAT/Encoder/Cardinality.hs
@@ -20,6 +20,7 @@ module ToySolver.SAT.Encoder.Cardinality
   , newEncoder
   , newEncoderWithStrategy
   , encodeAtLeast
+  , getTseitinEncoder
 
     -- XXX
   , TotalizerDefinitions
@@ -72,8 +73,8 @@ 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 tseitin _) = tseitin
+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

diff --git a/src/ToySolver/SAT/Encoder/PB.hs b/src/ToySolver/SAT/Encoder/PB.hs
@@ -36,17 +36,20 @@ 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.PB.Internal.Adder (addPBLinAtLeastAdder, encodePBLinAtLeastAdder)
+import ToySolver.SAT.Encoder.PB.Internal.BCCNF (addPBLinAtLeastBCCNF, encodePBLinAtLeastBCCNF)
 import ToySolver.SAT.Encoder.PB.Internal.BDD (addPBLinAtLeastBDD, encodePBLinAtLeastBDD)
 import ToySolver.SAT.Encoder.PB.Internal.Sorter (addPBLinAtLeastSorter, encodePBLinAtLeastSorter)
 
-data Encoder m = Encoder (Tseitin.Encoder m) Strategy
+data Encoder m = Encoder (Card.Encoder m) Strategy
 
 data Strategy
   = BDD
   | Adder
   | Sorter
+  | BCCNF
   | Hybrid -- not implemented yet
   deriving (Show, Eq, Ord, Enum, Bounded)
 
@@ -57,6 +60,7 @@ showStrategy :: Strategy -> String
 showStrategy BDD = "bdd"
 showStrategy Adder = "adder"
 showStrategy Sorter = "sorter"
+showStrategy BCCNF = "bccnf"
 showStrategy Hybrid = "hybrid"
 
 parseStrategy :: String -> Maybe Strategy
@@ -65,14 +69,17 @@ parseStrategy s =
     "bdd"    -> Just BDD
     "adder"  -> Just Adder
     "sorter" -> Just Sorter
+    "bccnf"  -> Just BCCNF
     "hybrid" -> Just Hybrid
     _ -> Nothing
 
-newEncoder :: Monad m => Tseitin.Encoder m -> m (Encoder m)
+newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
 newEncoder tseitin = newEncoderWithStrategy tseitin Hybrid
 
-newEncoderWithStrategy :: Monad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
-newEncoderWithStrategy tseitin strategy = return (Encoder tseitin strategy)
+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
@@ -100,17 +107,21 @@ encodePBLinAtLeast enc constr =
 -- -----------------------------------------------------------------------
 
 addPBLinAtLeast' :: PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m ()
-addPBLinAtLeast' (Encoder tseitin strategy) =
+addPBLinAtLeast' (Encoder card strategy) = do
+  let tseitin = Card.getTseitinEncoder card
   case strategy of
     Adder -> addPBLinAtLeastAdder tseitin
     Sorter -> addPBLinAtLeastSorter tseitin
+    BCCNF -> addPBLinAtLeastBCCNF card
     _ -> addPBLinAtLeastBDD tseitin
 
 encodePBLinAtLeast' :: PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
-encodePBLinAtLeast' (Encoder tseitin strategy) =
+encodePBLinAtLeast' (Encoder card strategy) = do
+  let tseitin = Card.getTseitinEncoder card
   case strategy of
     Adder -> encodePBLinAtLeastAdder tseitin
     Sorter -> encodePBLinAtLeastSorter tseitin
+    BCCNF -> encodePBLinAtLeastBCCNF card
     _ -> encodePBLinAtLeastBDD tseitin
 
 -- -----------------------------------------------------------------------

diff --git a/src/ToySolver/SAT/Encoder/PB/Internal/BCCNF.hs b/src/ToySolver/SAT/Encoder/PB/Internal/BCCNF.hs
@@ -23,8 +23,12 @@
 -----------------------------------------------------------------------------
 module ToySolver.SAT.Encoder.PB.Internal.BCCNF
   (
+  -- * Monadic interface
+    addPBLinAtLeastBCCNF
+  , encodePBLinAtLeastBCCNF
+
   -- * High-level pure encoder
-    encode
+  , encode
 
   -- * Low-level implementation
   , preprocess
@@ -52,12 +56,16 @@ module ToySolver.SAT.Encoder.PB.Internal.BCCNF
   ) where
 
 import Control.Exception (assert)
+import Control.Monad
+import Control.Monad.Primitive
 import Data.Function (on)
 import Data.List (sortBy)
 import Data.Maybe (listToMaybe)
 import Data.Ord (comparing)
 
 import ToySolver.SAT.Types
+import qualified ToySolver.SAT.Encoder.Cardinality as Card
+import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
 
 -- ------------------------------------------------------------------------
 
@@ -214,3 +222,17 @@ encodePrefixSumNaive = f
         ds' = [d | d <- [0..i], b * fromIntegral d < c - bssMax]
 
 -- ------------------------------------------------------------------------
+
+addPBLinAtLeastBCCNF :: PrimMonad m => Card.Encoder m -> PBLinAtLeast -> m ()
+addPBLinAtLeastBCCNF enc constr = do
+  forM_ (encode constr) $ \clause -> do
+    addClause enc =<< mapM (Card.encodeAtLeast enc) clause
+
+encodePBLinAtLeastBCCNF :: PrimMonad m => Card.Encoder m -> PBLinAtLeast -> m Lit
+encodePBLinAtLeastBCCNF enc constr = do
+  let tseitin = Card.getTseitinEncoder enc
+  ls <- forM (encode constr) $ \clause -> do
+    Tseitin.encodeDisjWithPolarity tseitin Tseitin.polarityPos =<< mapM (Card.encodeAtLeast enc) clause
+  Tseitin.encodeConjWithPolarity tseitin Tseitin.polarityPos ls
+
+-- ------------------------------------------------------------------------