add addSOS2 and evalSOS2 to ToySolver.SAT.Types

src/ToySolver/Converter/MIP2PB.hs

@@ -236,8 +236,7 @@ addMIP' enc mip = do
           lift $ SAT.addAtMost enc ys 1
         MIP.S2 -> do
           ys <- mapM (isNonZero . fst) $ sortBy (comparing snd) xs
-          forM_ (nonAdjacentPairs ys) $ \(x1,x2) -> do
-            lift $ SAT.addClause enc [SAT.litNot v | v <- [x1,x2]]
+          lift $ SAT.addSOS2 enc ys
 
     let obj = MIP.objectiveFunction mip
         d = foldl' lcm 1 [denominator r | MIP.Term r _ <- MIP.terms (MIP.objExpr obj)] *
@@ -252,10 +251,6 @@ addMIP' enc mip = do
     ivs = MIP.integerVariables mip
     nivs = MIP.variables mip `Set.difference` ivs
 
-    nonAdjacentPairs :: [a] -> [(a,a)]
-    nonAdjacentPairs (x1:x2:xs) = [(x1,x3) | x3 <- xs] ++ nonAdjacentPairs (x2:xs)
-    nonAdjacentPairs _ = []
-
     asBin :: Integer.Expr -> SAT.Lit
     asBin (Integer.Expr [(1,[lit])]) = lit
     asBin _ = error "asBin: failure"

src/ToySolver/SAT/Solver/CDCL.hs

@@ -81,6 +81,9 @@ module ToySolver.SAT.Solver.CDCL
   , AddXORClause (..)
   , XORClause
   , evalXORClause
+  -- ** Type-2 SOS constraints
+  , addSOS2
+  , evalSOS2
   -- ** Theory
   , setTheory
 

src/ToySolver/SAT/Types.hs

@@ -109,6 +109,10 @@ module ToySolver.SAT.Types
   , AddPBLin (..)
   , AddPBNL (..)
   , AddXORClause (..)
+
+  -- * Type-2 SOS constraints
+  , addSOS2
+  , evalSOS2
   ) where
 
 import Control.Monad
@@ -751,3 +755,25 @@ class AddClause m a => AddXORClause m a | a -> m where
     reified <- newVar a
     addXORClause a (litNot reified : lits) rhs
     addClause a [litNot sel, reified] -- sel ⇒ reified
+
+-- | Add a type-2 SOS constraint
+--
+-- At most two adjacnt literals can be true.
+addSOS2 :: AddClause m a => a -> [Lit] -> m ()
+addSOS2 a xs =
+  forM_ (nonAdjacentPairs xs) $ \(x1,x2) -> do
+    addClause a [litNot v | v <- [x1,x2]]
+  where
+    nonAdjacentPairs :: [a] -> [(a,a)]
+    nonAdjacentPairs (x1:x2:xs) = [(x1,x3) | x3 <- xs] ++ nonAdjacentPairs (x2:xs)
+    nonAdjacentPairs _ = []
+
+-- | Evaluate type-2 SOS constraint
+evalSOS2 :: IModel m => m -> [Lit] -> Bool
+evalSOS2 m = f
+  where
+    f [] = True
+    f [_] = True
+    f (l1 : l2 : ls)
+      | evalLit m l1 = all (not . evalLit m) ls
+      | otherwise = f (l2 : ls)

test/Test/SAT.hs

@@ -656,6 +656,33 @@ case_clearLearnCallback = do
   learnt <- readIORef learntRef
   assertBool "learn callback should not have been called" (null learnt)
 
+------------------------------------------------------------------------
+
+prop_SOS2 :: Property
+prop_SOS2 = QM.monadicIO $ do
+  cnf <- QM.pick arbitraryCNF
+  sos2 <- QM.pick $ do
+    n <- choose (0, CNF.cnfNumVars cnf)
+    replicateM n (arbitraryLit (CNF.cnfNumVars cnf))
+
+  solver <- arbitrarySolver
+  ret <- QM.run $ do
+    SAT.newVars_ solver (CNF.cnfNumVars cnf)
+    forM_ (CNF.cnfClauses cnf) $ \c -> SAT.addClause solver (SAT.unpackClause c)
+    SAT.addSOS2 solver sos2
+    ret <- SAT.solve solver
+    if ret then do
+      m <- SAT.getModel solver
+      return (Just m)
+    else do
+      return Nothing
+
+  case ret of
+    Just m -> QM.assert $ evalCNF m cnf && SAT.evalSOS2 m sos2
+    Nothing -> do
+      forM_ (allAssignments (CNF.cnfNumVars cnf)) $ \m -> do
+        QM.assert $ not (evalCNF m cnf && SAT.evalSOS2 m sos2)
+
 ------------------------------------------------------------------------
 -- Test harness