toysolver-0.5.0: test/Test/SAT.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, FlexibleContexts #-}
module Test.SAT (satTestGroup) where
import Control.Monad
import Data.Array.IArray
import Data.Default.Class
import qualified Data.Foldable as F
import Data.IORef
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.Traversable as Traversable
import qualified Data.Vector as V
import qualified System.Random.MWC as Rand
import Test.Tasty
import Test.Tasty.QuickCheck hiding ((.&&.), (.||.))
import Test.Tasty.HUnit
import Test.Tasty.TH
import qualified Test.QuickCheck.Monadic as QM
import ToySolver.Data.LBool
import ToySolver.Data.BoolExpr
import ToySolver.Data.Boolean
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import ToySolver.SAT.TheorySolver
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import qualified ToySolver.SAT.Encoder.PB as PB
import qualified ToySolver.SAT.Encoder.PB.Internal.Sorter as PBEncSorter
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
import qualified ToySolver.SAT.MUS as MUS
import qualified ToySolver.SAT.MUS.Enum as MUSEnum
import qualified ToySolver.SAT.PBO as PBO
import qualified ToySolver.SAT.Store.CNF as CNFStore
import qualified ToySolver.SAT.ExistentialQuantification as ExistentialQuantification
import qualified Data.PseudoBoolean as PBFile
import qualified ToySolver.Converter.PB2SAT as PB2SAT
import qualified ToySolver.Converter.WBO2MaxSAT as WBO2MaxSAT
import qualified ToySolver.Converter.WBO2PB as WBO2PB
import qualified ToySolver.Converter.SAT2KSAT as SAT2KSAT
import qualified ToySolver.Text.CNF as CNF
import qualified ToySolver.Text.MaxSAT as MaxSAT
import ToySolver.Data.OrdRel
import qualified ToySolver.Data.LA as LA
import qualified ToySolver.Arith.Simplex as Simplex
import qualified ToySolver.EUF.EUFSolver as EUF
allAssignments :: Int -> [SAT.Model]
allAssignments nv = [array (1,nv) (zip [1..nv] xs) | xs <- replicateM nv [True,False]]
prop_solveCNF :: Property
prop_solveCNF = QM.monadicIO $ do
cnf <- QM.pick arbitraryCNF
solver <- arbitrarySolver
ret <- QM.run $ solveCNF solver cnf
case ret of
Just m -> QM.assert $ evalCNF m cnf
Nothing -> do
forM_ (allAssignments (CNF.numVars cnf)) $ \m -> do
QM.assert $ not (evalCNF m cnf)
solveCNF :: SAT.Solver -> CNF.CNF -> IO (Maybe SAT.Model)
solveCNF solver cnf = do
SAT.newVars_ solver (CNF.numVars cnf)
forM_ (CNF.clauses cnf) $ \c -> SAT.addClause solver c
ret <- SAT.solve solver
if ret then do
m <- SAT.getModel solver
return (Just m)
else do
return Nothing
arbitraryCNF :: Gen CNF.CNF
arbitraryCNF = do
nv <- choose (0,10)
nc <- choose (0,50)
cs <- replicateM nc $ do
len <- choose (0,10)
if nv == 0 then
return []
else
replicateM len $ choose (-nv, nv) `suchThat` (/= 0)
return $
CNF.CNF
{ CNF.numVars = nv
, CNF.numClauses = nc
, CNF.clauses = cs
}
evalCNF :: SAT.Model -> CNF.CNF -> Bool
evalCNF m cnf = all (SAT.evalClause m) (CNF.clauses cnf)
prop_solvePB :: Property
prop_solvePB = QM.monadicIO $ do
prob@(nv,_) <- QM.pick arbitraryPB
solver <- arbitrarySolver
ret <- QM.run $ solvePB solver prob
case ret of
Just m -> QM.assert $ evalPB m prob
Nothing -> do
forM_ (allAssignments nv) $ \m -> do
QM.assert $ not (evalPB m prob)
data PBRel = PBRelGE | PBRelEQ | PBRelLE deriving (Eq, Ord, Enum, Bounded, Show)
instance Arbitrary PBRel where
arbitrary = arbitraryBoundedEnum
evalPBRel :: Ord a => PBRel -> a -> a -> Bool
evalPBRel PBRelGE = (>=)
evalPBRel PBRelLE = (<=)
evalPBRel PBRelEQ = (==)
solvePB :: SAT.Solver -> (Int,[(PBRel,SAT.PBLinSum,Integer)]) -> IO (Maybe SAT.Model)
solvePB solver (nv,cs) = do
SAT.newVars_ solver nv
forM_ cs $ \(o,lhs,rhs) -> do
case o of
PBRelGE -> SAT.addPBAtLeast solver lhs rhs
PBRelLE -> SAT.addPBAtMost solver lhs rhs
PBRelEQ -> SAT.addPBExactly solver lhs rhs
ret <- SAT.solve solver
if ret then do
m <- SAT.getModel solver
return (Just m)
else do
return Nothing
arbitraryPB :: Gen (Int,[(PBRel,SAT.PBLinSum,Integer)])
arbitraryPB = do
nv <- choose (0,10)
nc <- choose (0,50)
cs <- replicateM nc $ do
rel <- arbitrary
lhs <- arbitraryPBLinSum nv
rhs <- arbitrary
return $ (rel,lhs,rhs)
return (nv, cs)
arbitraryPBLinSum :: Int -> Gen SAT.PBLinSum
arbitraryPBLinSum nv = do
len <- choose (0,10)
if nv == 0 then
return []
else
replicateM len $ do
l <- choose (-nv, nv) `suchThat` (/= 0)
c <- arbitrary
return (c,l)
evalPB :: SAT.Model -> (Int,[(PBRel,SAT.PBLinSum,Integer)]) -> Bool
evalPB m (_,cs) = all (\(o,lhs,rhs) -> evalPBRel o (SAT.evalPBLinSum m lhs) rhs) cs
prop_optimizePBO :: Property
prop_optimizePBO = QM.monadicIO $ do
prob@(nv,_) <- QM.pick arbitraryPB
obj <- QM.pick $ arbitraryPBLinSum nv
solver <- arbitrarySolver
opt <- arbitraryOptimizer solver obj
ret <- QM.run $ optimizePBO solver opt prob
case ret of
Just (m, v) -> do
QM.assert $ evalPB m prob
QM.assert $ SAT.evalPBLinSum m obj == v
forM_ (allAssignments nv) $ \m2 -> do
QM.assert $ not (evalPB m2 prob) || SAT.evalPBLinSum m obj <= SAT.evalPBLinSum m2 obj
Nothing -> do
forM_ (allAssignments nv) $ \m -> do
QM.assert $ not (evalPB m prob)
optimizePBO :: SAT.Solver -> PBO.Optimizer -> (Int,[(PBRel,SAT.PBLinSum,Integer)]) -> IO (Maybe (SAT.Model, Integer))
optimizePBO solver opt (nv,cs) = do
SAT.newVars_ solver nv
forM_ cs $ \(o,lhs,rhs) -> do
case o of
PBRelGE -> SAT.addPBAtLeast solver lhs rhs
PBRelLE -> SAT.addPBAtMost solver lhs rhs
PBRelEQ -> SAT.addPBExactly solver lhs rhs
PBO.optimize opt
PBO.getBestSolution opt
evalWBO :: SAT.Model -> (Int, [(Maybe Integer, (PBRel,SAT.PBLinSum,Integer))], Maybe Integer) -> Maybe Integer
evalWBO m (nv,cs,top) = do
cost <- liftM sum $ forM cs $ \(w,(o,lhs,rhs)) -> do
if evalPBRel o (SAT.evalPBLinSum m lhs) rhs then
return 0
else
w
case top of
Just t -> guard (cost < t)
Nothing -> return ()
return cost
arbitraryWBO :: Gen (Int, [(Maybe Integer, (PBRel,SAT.PBLinSum,Integer))], Maybe Integer)
arbitraryWBO = do
(nv,cs) <- arbitraryPB
cs2 <- forM cs $ \c -> do
b <- arbitrary
cost <- if b then return Nothing
else liftM (Just . (1+) . abs) arbitrary
return (cost, c)
b <- arbitrary
top <- if b then return Nothing
else liftM (Just . (1+) . abs) arbitrary
return (nv,cs2,top)
optimizeWBO
:: SAT.Solver
-> PBO.Method
-> (Int, [(Maybe Integer, (PBRel,SAT.PBLinSum,Integer))], Maybe Integer)
-> IO (Maybe (SAT.Model, Integer))
optimizeWBO solver method (nv,cs,top) = do
SAT.newVars_ solver nv
obj <- liftM catMaybes $ forM cs $ \(cost, (o,lhs,rhs)) -> do
case cost of
Nothing -> do
case o of
PBRelGE -> SAT.addPBAtLeast solver lhs rhs
PBRelLE -> SAT.addPBAtMost solver lhs rhs
PBRelEQ -> SAT.addPBExactly solver lhs rhs
return Nothing
Just w -> do
sel <- SAT.newVar solver
case o of
PBRelGE -> SAT.addPBAtLeastSoft solver sel lhs rhs
PBRelLE -> SAT.addPBAtMostSoft solver sel lhs rhs
PBRelEQ -> SAT.addPBExactlySoft solver sel lhs rhs
return $ Just (w,-sel)
case top of
Nothing -> return ()
Just c -> SAT.addPBAtMost solver obj (c-1)
opt <- PBO.newOptimizer solver obj
PBO.optimize opt
liftM (fmap (\(m, val) -> (SAT.restrictModel nv m, val))) $ PBO.getBestSolution opt
prop_solvePBNLC :: Property
prop_solvePBNLC = QM.monadicIO $ do
prob@(nv,_) <- QM.pick arbitraryPBNLC
solver <- arbitrarySolver
ret <- QM.run $ solvePBNLC solver prob
case ret of
Just m -> QM.assert $ evalPBNLC m prob
Nothing -> do
forM_ (allAssignments nv) $ \m -> do
QM.assert $ not (evalPBNLC m prob)
solvePBNLC :: SAT.Solver -> (Int,[(PBRel,SAT.PBSum,Integer)]) -> IO (Maybe SAT.Model)
solvePBNLC solver (nv,cs) = do
SAT.newVars_ solver nv
enc <- PBNLC.newEncoder solver =<< Tseitin.newEncoder solver
forM_ cs $ \(o,lhs,rhs) -> do
case o of
PBRelGE -> PBNLC.addPBNLAtLeast enc lhs rhs
PBRelLE -> PBNLC.addPBNLAtMost enc lhs rhs
PBRelEQ -> PBNLC.addPBNLExactly enc lhs rhs
ret <- SAT.solve solver
if ret then do
m <- SAT.getModel solver
return $ Just $ SAT.restrictModel nv m
else do
return Nothing
optimizePBNLC
:: SAT.Solver
-> PBO.Method
-> (Int, SAT.PBSum, [(PBRel,SAT.PBSum,Integer)])
-> IO (Maybe (SAT.Model, Integer))
optimizePBNLC solver method (nv,obj,cs) = do
SAT.newVars_ solver nv
enc <- PBNLC.newEncoder solver =<< Tseitin.newEncoder solver
forM_ cs $ \(o,lhs,rhs) -> do
case o of
PBRelGE -> PBNLC.addPBNLAtLeast enc lhs rhs
PBRelLE -> PBNLC.addPBNLAtMost enc lhs rhs
PBRelEQ -> PBNLC.addPBNLExactly enc lhs rhs
obj2 <- PBNLC.linearizePBSumWithPolarity enc Tseitin.polarityNeg obj
opt <- PBO.newOptimizer2 solver obj2 (\m -> SAT.evalPBSum m obj)
PBO.setMethod opt method
PBO.optimize opt
liftM (fmap (\(m, val) -> (SAT.restrictModel nv m, val))) $ PBO.getBestSolution opt
arbitraryPBNLC :: Gen (Int,[(PBRel,SAT.PBSum,Integer)])
arbitraryPBNLC = do
nv <- choose (0,10)
nc <- choose (0,50)
cs <- replicateM nc $ do
rel <- arbitrary
len <- choose (0,10)
lhs <-
if nv == 0 then
return []
else
replicateM len $ do
ls <- listOf $ choose (-nv, nv) `suchThat` (/= 0)
c <- arbitrary
return (c,ls)
rhs <- arbitrary
return $ (rel,lhs,rhs)
return (nv, cs)
evalPBNLC :: SAT.Model -> (Int,[(PBRel,SAT.PBSum,Integer)]) -> Bool
evalPBNLC m (_,cs) = all (\(o,lhs,rhs) -> evalPBRel o (SAT.evalPBSum m lhs) rhs) cs
prop_solveXOR :: Property
prop_solveXOR = QM.monadicIO $ do
prob@(nv,_) <- QM.pick arbitraryXOR
solver <- arbitrarySolver
ret <- QM.run $ solveXOR solver prob
case ret of
Just m -> QM.assert $ evalXOR m prob
Nothing -> do
forM_ (allAssignments nv) $ \m -> do
QM.assert $ not (evalXOR m prob)
solveXOR :: SAT.Solver -> (Int,[SAT.XORClause]) -> IO (Maybe SAT.Model)
solveXOR solver (nv,cs) = do
SAT.modifyConfig solver $ \config -> config{ SAT.configCheckModel = True }
SAT.newVars_ solver nv
forM_ cs $ \c -> SAT.addXORClause solver (fst c) (snd c)
ret <- SAT.solve solver
if ret then do
m <- SAT.getModel solver
return (Just m)
else do
return Nothing
arbitraryXOR :: Gen (Int,[SAT.XORClause])
arbitraryXOR = do
nv <- choose (0,10)
nc <- choose (0,50)
cs <- replicateM nc $ do
len <- choose (0,10)
lhs <-
if nv == 0 then
return []
else
replicateM len $ choose (-nv, nv) `suchThat` (/= 0)
rhs <- arbitrary
return (lhs,rhs)
return (nv, cs)
evalXOR :: SAT.Model -> (Int,[SAT.XORClause]) -> Bool
evalXOR m (_,cs) = all (SAT.evalXORClause m) cs
newTheorySolver :: CNF.CNF -> IO TheorySolver
newTheorySolver cnf = do
let nv = CNF.numVars cnf
cs = CNF.clauses cnf
solver <- SAT.newSolver
SAT.newVars_ solver nv
forM_ cs $ \c -> SAT.addClause solver c
ref <- newIORef []
let tsolver =
TheorySolver
{ thAssertLit = \_ l -> do
if abs l > nv then
return True
else do
m <- readIORef ref
case m of
[] -> SAT.addClause solver [l]
xs : xss -> writeIORef ref ((l : xs) : xss)
return True
, thCheck = \_ -> do
xs <- liftM concat $ readIORef ref
SAT.solveWith solver xs
, thExplain = \m -> do
case m of
Nothing -> SAT.getFailedAssumptions solver
Just _ -> return []
, thPushBacktrackPoint = modifyIORef ref ([] :)
, thPopBacktrackPoint = modifyIORef ref tail
, thConstructModel = return ()
}
return tsolver
prop_solveCNF_using_BooleanTheory :: Property
prop_solveCNF_using_BooleanTheory = QM.monadicIO $ do
cnf <- QM.pick arbitraryCNF
let nv = CNF.numVars cnf
nc = CNF.numClauses cnf
cs = CNF.clauses cnf
cnf1 = cnf{ CNF.clauses = [c | (i,c) <- zip [0..] cs, i `mod` 2 == 0], CNF.numClauses = nc - (nc `div` 2) }
cnf2 = cnf{ CNF.clauses = [c | (i,c) <- zip [0..] cs, i `mod` 2 /= 0], CNF.numClauses = nc `div` 2 }
solver <- arbitrarySolver
ret <- QM.run $ do
SAT.newVars_ solver nv
tsolver <- newTheorySolver cnf1
SAT.setTheory solver tsolver
forM_ (CNF.clauses cnf2) $ \c -> SAT.addClause solver c
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
Nothing -> do
forM_ (allAssignments nv) $ \m -> do
QM.assert $ not (evalCNF m cnf)
case_QF_LRA :: Assertion
case_QF_LRA = do
satSolver <- SAT.newSolver
lraSolver <- Simplex.newSolver
tblRef <- newIORef $ Map.empty
defsRef <- newIORef $ IntMap.empty
let abstractLAAtom :: LA.Atom Rational -> IO SAT.Lit
abstractLAAtom atom = do
(v,op,rhs) <- Simplex.simplifyAtom lraSolver atom
tbl <- readIORef tblRef
(vLt, vEq, vGt) <-
case Map.lookup (v,rhs) tbl of
Just (vLt, vEq, vGt) -> return (vLt, vEq, vGt)
Nothing -> do
vLt <- SAT.newVar satSolver
vEq <- SAT.newVar satSolver
vGt <- SAT.newVar satSolver
SAT.addClause satSolver [vLt,vEq,vGt]
SAT.addClause satSolver [-vLt, -vEq]
SAT.addClause satSolver [-vLt, -vGt]
SAT.addClause satSolver [-vEq, -vGt]
writeIORef tblRef (Map.insert (v,rhs) (vLt, vEq, vGt) tbl)
let xs = IntMap.fromList
[ (vEq, LA.var v .==. LA.constant rhs)
, (vLt, LA.var v .<. LA.constant rhs)
, (vGt, LA.var v .>. LA.constant rhs)
, (-vLt, LA.var v .>=. LA.constant rhs)
, (-vGt, LA.var v .<=. LA.constant rhs)
]
modifyIORef defsRef (IntMap.union xs)
return (vLt, vEq, vGt)
case op of
Lt -> return vLt
Gt -> return vGt
Eql -> return vEq
Le -> return (-vGt)
Ge -> return (-vLt)
NEq -> return (-vEq)
abstract :: BoolExpr (Either SAT.Lit (LA.Atom Rational)) -> IO (BoolExpr SAT.Lit)
abstract = Traversable.mapM f
where
f (Left lit) = return lit
f (Right atom) = abstractLAAtom atom
let tsolver =
TheorySolver
{ thAssertLit = \_ l -> do
defs <- readIORef defsRef
case IntMap.lookup l defs of
Nothing -> return True
Just atom -> do
Simplex.assertAtomEx' lraSolver atom (Just l)
return True
, thCheck = \_ -> do
Simplex.check lraSolver
, thExplain = \m -> do
case m of
Nothing -> liftM IntSet.toList $ Simplex.explain lraSolver
Just _ -> return []
, thPushBacktrackPoint = do
Simplex.pushBacktrackPoint lraSolver
, thPopBacktrackPoint = do
Simplex.popBacktrackPoint lraSolver
, thConstructModel = do
return ()
}
SAT.setTheory satSolver tsolver
enc <- Tseitin.newEncoder satSolver
let addFormula :: BoolExpr (Either SAT.Lit (LA.Atom Rational)) -> IO ()
addFormula c = Tseitin.addFormula enc =<< abstract c
a <- SAT.newVar satSolver
x <- Simplex.newVar lraSolver
y <- Simplex.newVar lraSolver
let le1 = LA.fromTerms [(2,x), (1/3,y)] .<=. LA.constant (-4) -- 2 x + (1/3) y <= -4
eq2 = LA.fromTerms [(1.5,x)] .==. LA.fromTerms [(-2,x)] -- 1.5 y = -2 x
gt3 = LA.var x .>. LA.var y -- x > y
lt4 = LA.fromTerms [(3,x)] .<. LA.fromTerms [(-1,LA.unitVar), (1/5,x), (1/5,y)] -- 3 x < -1 + (1/5) (x + y)
c1, c2 :: BoolExpr (Either SAT.Lit (LA.Atom Rational))
c1 = ite (Atom (Left a) :: BoolExpr (Either SAT.Lit (LA.Atom Rational))) (Atom $ Right le1) (Atom $ Right eq2)
c2 = Atom (Right gt3) .||. (Atom (Left a) .<=>. Atom (Right lt4))
addFormula c1
addFormula c2
ret <- SAT.solve satSolver
ret @?= True
m1 <- SAT.getModel satSolver
m2 <- Simplex.getModel lraSolver
defs <- readIORef defsRef
let f (Left lit) = SAT.evalLit m1 lit
f (Right atom) = LA.eval m2 atom
fold f c1 @?= True
fold f c2 @?= True
case_QF_EUF :: Assertion
case_QF_EUF = do
satSolver <- SAT.newSolver
eufSolver <- EUF.newSolver
enc <- Tseitin.newEncoder satSolver
tblRef <- newIORef (Map.empty :: Map (EUF.Term, EUF.Term) SAT.Var)
defsRef <- newIORef (IntMap.empty :: IntMap (EUF.Term, EUF.Term))
eufModelRef <- newIORef (undefined :: EUF.Model)
let abstractEUFAtom :: (EUF.Term, EUF.Term) -> IO SAT.Lit
abstractEUFAtom (t1,t2) | t1 >= t2 = abstractEUFAtom (t2,t1)
abstractEUFAtom (t1,t2) = do
tbl <- readIORef tblRef
case Map.lookup (t1,t2) tbl of
Just v -> return v
Nothing -> do
v <- SAT.newVar satSolver
writeIORef tblRef $! Map.insert (t1,t2) v tbl
modifyIORef' defsRef $! IntMap.insert v (t1,t2)
return v
abstract :: BoolExpr (Either SAT.Lit (EUF.Term, EUF.Term)) -> IO (BoolExpr SAT.Lit)
abstract = Traversable.mapM f
where
f (Left lit) = return lit
f (Right atom) = abstractEUFAtom atom
let tsolver =
TheorySolver
{ thAssertLit = \_ l -> do
defs <- readIORef defsRef
case IntMap.lookup (SAT.litVar l) defs of
Nothing -> return True
Just (t1,t2) -> do
if SAT.litPolarity l then
EUF.assertEqual' eufSolver t1 t2 (Just l)
else
EUF.assertNotEqual' eufSolver t1 t2 (Just l)
return True
, thCheck = \callback -> do
b <- EUF.check eufSolver
when b $ do
defs <- readIORef defsRef
forM_ (IntMap.toList defs) $ \(v, (t1, t2)) -> do
b2 <- EUF.areEqual eufSolver t1 t2
when b2 $ do
callback v
return ()
return b
, thExplain = \m -> do
case m of
Nothing -> liftM IntSet.toList $ EUF.explain eufSolver Nothing
Just v -> do
defs <- readIORef defsRef
case IntMap.lookup v defs of
Nothing -> error "should not happen"
Just (t1,t2) -> do
liftM IntSet.toList $ EUF.explain eufSolver (Just (t1,t2))
, thPushBacktrackPoint = do
EUF.pushBacktrackPoint eufSolver
, thPopBacktrackPoint = do
EUF.popBacktrackPoint eufSolver
, thConstructModel = do
writeIORef eufModelRef =<< EUF.getModel eufSolver
return ()
}
SAT.setTheory satSolver tsolver
true <- EUF.newConst eufSolver
false <- EUF.newConst eufSolver
EUF.assertNotEqual eufSolver true false
boolToTermRef <- newIORef (IntMap.empty :: IntMap EUF.Term)
termToBoolRef <- newIORef (Map.empty :: Map EUF.Term SAT.Lit)
let connectBoolTerm :: SAT.Lit -> EUF.Term -> IO ()
connectBoolTerm lit t = do
lit1 <- abstractEUFAtom (t, true)
lit2 <- abstractEUFAtom (t, false)
SAT.addClause satSolver [-lit, lit1] -- lit -> lit1
SAT.addClause satSolver [-lit1, lit] -- lit1 -> lit
SAT.addClause satSolver [lit, lit2] -- -lit -> lit2
SAT.addClause satSolver [-lit2, -lit] -- lit2 -> -lit
modifyIORef' boolToTermRef $ IntMap.insert lit t
modifyIORef' termToBoolRef $ Map.insert t lit
boolToTerm :: SAT.Lit -> IO EUF.Term
boolToTerm lit = do
tbl <- readIORef boolToTermRef
case IntMap.lookup lit tbl of
Just t -> return t
Nothing -> do
t <- EUF.newConst eufSolver
connectBoolTerm lit t
return t
termToBool :: EUF.Term -> IO SAT.Lit
termToBool t = do
tbl <- readIORef termToBoolRef
case Map.lookup t tbl of
Just lit -> return lit
Nothing -> do
lit <- SAT.newVar satSolver
connectBoolTerm lit t
return lit
let addFormula :: BoolExpr (Either SAT.Lit (EUF.Term, EUF.Term)) -> IO ()
addFormula c = Tseitin.addFormula enc =<< abstract c
do
x <- SAT.newVar satSolver
x' <- boolToTerm x
f <- EUF.newFun eufSolver
fx <- termToBool (f x')
ftt <- abstractEUFAtom (f true, true)
ret <- SAT.solveWith satSolver [-fx, ftt]
ret @?= True
m1 <- SAT.getModel satSolver
m2 <- readIORef eufModelRef
let e (Left lit) = SAT.evalLit m1 lit
e (Right (lhs,rhs)) = EUF.eval m2 lhs == EUF.eval m2 rhs
fold e (notB (Atom (Left fx)) .||. (Atom (Right (f true, true)))) @?= True
SAT.evalLit m1 x @?= False
ret <- SAT.solveWith satSolver [-fx, ftt, x]
ret @?= False
do
-- a : Bool
-- f : U -> U
-- x : U
-- y : U
-- (a or x=y)
-- f x /= f y
a <- SAT.newVar satSolver
f <- EUF.newFun eufSolver
x <- EUF.newConst eufSolver
y <- EUF.newConst eufSolver
let c1, c2 :: BoolExpr (Either SAT.Lit (EUF.Term, EUF.Term))
c1 = Atom (Left a) .||. Atom (Right (x,y))
c2 = notB $ Atom (Right (f x, f y))
addFormula c1
addFormula c2
ret <- SAT.solve satSolver
ret @?= True
m1 <- SAT.getModel satSolver
m2 <- readIORef eufModelRef
let e (Left lit) = SAT.evalLit m1 lit
e (Right (lhs,rhs)) = EUF.eval m2 lhs == EUF.eval m2 rhs
fold e c1 @?= True
fold e c2 @?= True
ret <- SAT.solveWith satSolver [-a]
ret @?= False
-- should be SAT
case_solve_SAT :: Assertion
case_solve_SAT = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addClause solver [x1, x2] -- x1 or x2
SAT.addClause solver [x1, -x2] -- x1 or not x2
SAT.addClause solver [-x1, -x2] -- not x1 or not x2
ret <- SAT.solve solver
ret @?= True
-- shuld be UNSAT
case_solve_UNSAT :: Assertion
case_solve_UNSAT = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addClause solver [x1, x2] -- x1 or x2
SAT.addClause solver [-x1, x2] -- not x1 or x2
SAT.addClause solver [x1, -x2] -- x1 or not x2
SAT.addClause solver [-x1, -x2] -- not x2 or not x2
ret <- SAT.solve solver
ret @?= False
-- top level でいきなり矛盾
case_root_inconsistent :: Assertion
case_root_inconsistent = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
SAT.addClause solver [x1]
SAT.addClause solver [-x1]
ret <- SAT.solve solver -- unsat
ret @?= False
-- incremental に制約を追加
case_incremental_solving :: Assertion
case_incremental_solving = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addClause solver [x1, x2] -- x1 or x2
SAT.addClause solver [x1, -x2] -- x1 or not x2
SAT.addClause solver [-x1, -x2] -- not x1 or not x2
ret <- SAT.solve solver -- sat
ret @?= True
SAT.addClause solver [-x1, x2] -- not x1 or x2
ret <- SAT.solve solver -- unsat
ret @?= False
-- 制約なし
case_empty_constraint :: Assertion
case_empty_constraint = do
solver <- SAT.newSolver
ret <- SAT.solve solver
ret @?= True
-- 空の節
case_empty_claue :: Assertion
case_empty_claue = do
solver <- SAT.newSolver
SAT.addClause solver []
ret <- SAT.solve solver
ret @?= False
-- 自明に真な節
case_excluded_middle_claue :: Assertion
case_excluded_middle_claue = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
SAT.addClause solver [x1, -x1] -- x1 or not x1
ret <- SAT.solve solver
ret @?= True
-- 冗長な節
case_redundant_clause :: Assertion
case_redundant_clause = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
SAT.addClause solver [x1,x1] -- x1 or x1
ret <- SAT.solve solver
ret @?= True
case_instantiateClause :: Assertion
case_instantiateClause = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addClause solver [x1]
SAT.addClause solver [x1,x2]
SAT.addClause solver [-x1,x2]
ret <- SAT.solve solver
ret @?= True
case_instantiateAtLeast :: Assertion
case_instantiateAtLeast = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
x4 <- SAT.newVar solver
SAT.addClause solver [x1]
SAT.addAtLeast solver [x1,x2,x3,x4] 2
ret <- SAT.solve solver
ret @?= True
SAT.addAtLeast solver [-x1,-x2,-x3,-x4] 2
ret <- SAT.solve solver
ret @?= True
case_inconsistent_AtLeast :: Assertion
case_inconsistent_AtLeast = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addAtLeast solver [x1,x2] 3
ret <- SAT.solve solver -- unsat
ret @?= False
case_trivial_AtLeast :: Assertion
case_trivial_AtLeast = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addAtLeast solver [x1,x2] 0
ret <- SAT.solve solver
ret @?= True
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addAtLeast solver [x1,x2] (-1)
ret <- SAT.solve solver
ret @?= True
case_AtLeast_1 :: Assertion
case_AtLeast_1 = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
SAT.addAtLeast solver [x1,x2,x3] 2
SAT.addAtLeast solver [-x1,-x2,-x3] 2
ret <- SAT.solve solver -- unsat
ret @?= False
case_AtLeast_2 :: Assertion
case_AtLeast_2 = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
x4 <- SAT.newVar solver
SAT.addAtLeast solver [x1,x2,x3,x4] 2
SAT.addClause solver [-x1,-x2]
SAT.addClause solver [-x1,-x3]
ret <- SAT.solve solver
ret @?= True
case_AtLeast_3 :: Assertion
case_AtLeast_3 = do
forM_ [(-1) .. 3] $ \n -> do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addAtLeast solver [x1,x2] n
ret <- SAT.solve solver
assertEqual ("case_AtLeast3_" ++ show n) (n <= 2) ret
-- from http://www.cril.univ-artois.fr/PB11/format.pdf
case_PB_sample1 :: Assertion
case_PB_sample1 = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
x4 <- SAT.newVar solver
x5 <- SAT.newVar solver
SAT.addPBAtLeast solver [(1,x1),(4,x2),(-2,x5)] 2
SAT.addPBAtLeast solver [(-1,x1),(4,x2),(-2,x5)] 3
SAT.addPBAtLeast solver [(12345678901234567890,x4),(4,x3)] 10
SAT.addPBExactly solver [(2,x2),(3,x4),(2,x1),(3,x5)] 5
ret <- SAT.solve solver
ret @?= True
-- 一部の変数を否定に置き換えたもの
case_PB_sample1' :: Assertion
case_PB_sample1' = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
x4 <- SAT.newVar solver
x5 <- SAT.newVar solver
SAT.addPBAtLeast solver [(1,x1),(4,-x2),(-2,x5)] 2
SAT.addPBAtLeast solver [(-1,x1),(4,-x2),(-2,x5)] 3
SAT.addPBAtLeast solver [(12345678901234567890,-x4),(4,x3)] 10
SAT.addPBExactly solver [(2,-x2),(3,-x4),(2,x1),(3,x5)] 5
ret <- SAT.solve solver
ret @?= True
-- いきなり矛盾したPB制約
case_root_inconsistent_PB :: Assertion
case_root_inconsistent_PB = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addPBAtLeast solver [(2,x1),(3,x2)] 6
ret <- SAT.solve solver
ret @?= False
case_pb_propagate :: Assertion
case_pb_propagate = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addPBAtLeast solver [(1,x1),(3,x2)] 3
SAT.addClause solver [-x1]
ret <- SAT.solve solver
ret @?= True
case_solveWith_1 :: Assertion
case_solveWith_1 = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
SAT.addClause solver [x1, x2] -- x1 or x2
SAT.addClause solver [x1, -x2] -- x1 or not x2
SAT.addClause solver [-x1, -x2] -- not x1 or not x2
SAT.addClause solver [-x3, -x1, x2] -- not x3 or not x1 or x2
ret <- SAT.solve solver -- sat
ret @?= True
ret <- SAT.solveWith solver [x3] -- unsat
ret @?= False
ret <- SAT.solve solver -- sat
ret @?= True
case_solveWith_2 :: Assertion
case_solveWith_2 = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addClause solver [-x1, x2] -- -x1 or x2
SAT.addClause solver [x1] -- x1
ret <- SAT.solveWith solver [x2]
ret @?= True
ret <- SAT.solveWith solver [-x2]
ret @?= False
case_getVarFixed :: Assertion
case_getVarFixed = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
SAT.addClause solver [x1,x2]
ret <- SAT.getVarFixed solver x1
ret @?= lUndef
SAT.addClause solver [-x1]
ret <- SAT.getVarFixed solver x1
ret @?= lFalse
ret <- SAT.getLitFixed solver (-x1)
ret @?= lTrue
ret <- SAT.getLitFixed solver x2
ret @?= lTrue
case_getAssumptionsImplications_case1 :: Assertion
case_getAssumptionsImplications_case1 = do
solver <- SAT.newSolver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
SAT.addClause solver [x1,x2,x3]
SAT.addClause solver [-x1]
ret <- SAT.solveWith solver [-x2]
ret @?= True
xs <- SAT.getAssumptionsImplications solver
xs @?= [x3]
prop_getAssumptionsImplications :: Property
prop_getAssumptionsImplications = QM.monadicIO $ do
cnf <- QM.pick arbitraryCNF
solver <- arbitrarySolver
ls <- QM.pick $ liftM concat $ mapM (\v -> elements [[],[-v],[v]]) [1..CNF.numVars cnf]
ret <- QM.run $ do
SAT.newVars_ solver (CNF.numVars cnf)
forM_ (CNF.clauses cnf) $ \c -> SAT.addClause solver c
SAT.solveWith solver ls
when ret $ do
xs <- QM.run $ SAT.getAssumptionsImplications solver
forM_ xs $ \x -> do
ret2 <- QM.run $ SAT.solveWith solver (-x : ls)
QM.assert $ not ret2
------------------------------------------------------------------------
-- -4*(not x1) + 3*x1 + 10*(not x2)
-- = -4*(1 - x1) + 3*x1 + 10*(not x2)
-- = -4 + 4*x1 + 3*x1 + 10*(not x2)
-- = 7*x1 + 10*(not x2) - 4
case_normalizePBLinSum_1 :: Assertion
case_normalizePBLinSum_1 = do
sort e @?= sort [(7,x1),(10,-x2)]
c @?= -4
where
x1 = 1
x2 = 2
(e,c) = SAT.normalizePBLinSum ([(-4,-x1),(3,x1),(10,-x2)], 0)
prop_normalizePBLinSum :: Property
prop_normalizePBLinSum = forAll g $ \(nv, (s,n)) ->
let (s2,n2) = SAT.normalizePBLinSum (s,n)
in flip all (allAssignments nv) $ \m ->
SAT.evalPBLinSum m s + n == SAT.evalPBLinSum m s2 + n2
where
g :: Gen (Int, (SAT.PBLinSum, Integer))
g = do
nv <- choose (0, 10)
s <- forM [1..nv] $ \x -> do
c <- arbitrary
p <- arbitrary
return (c, SAT.literal x p)
n <- arbitrary
return (nv, (s,n))
-- -4*(not x1) + 3*x1 + 10*(not x2) >= 3
-- ⇔ -4*(1 - x1) + 3*x1 + 10*(not x2) >= 3
-- ⇔ -4 + 4*x1 + 3*x1 + 10*(not x2) >= 3
-- ⇔ 7*x1 + 10*(not x2) >= 7
-- ⇔ 7*x1 + 7*(not x2) >= 7
-- ⇔ x1 + (not x2) >= 1
case_normalizePBLinAtLeast_1 :: Assertion
case_normalizePBLinAtLeast_1 = (sort lhs, rhs) @?= (sort [(1,x1),(1,-x2)], 1)
where
x1 = 1
x2 = 2
(lhs,rhs) = SAT.normalizePBLinAtLeast ([(-4,-x1),(3,x1),(10,-x2)], 3)
prop_normalizePBLinAtLeast :: Property
prop_normalizePBLinAtLeast = forAll g $ \(nv, c) ->
let c2 = SAT.normalizePBLinAtLeast c
in flip all (allAssignments nv) $ \m ->
SAT.evalPBLinAtLeast m c == SAT.evalPBLinAtLeast m c2
where
g :: Gen (Int, SAT.PBLinAtLeast)
g = do
nv <- choose (0, 10)
lhs <- forM [1..nv] $ \x -> do
c <- arbitrary
p <- arbitrary
return (c, SAT.literal x p)
rhs <- arbitrary
return (nv, (lhs,rhs))
case_normalizePBLinExactly_1 :: Assertion
case_normalizePBLinExactly_1 = (sort lhs, rhs) @?= ([], 1)
where
x1 = 1
x2 = 2
(lhs,rhs) = SAT.normalizePBLinExactly ([(6,x1),(4,x2)], 2)
case_normalizePBLinExactly_2 :: Assertion
case_normalizePBLinExactly_2 = (sort lhs, rhs) @?= ([], 1)
where
x1 = 1
x2 = 2
x3 = 3
(lhs,rhs) = SAT.normalizePBLinExactly ([(2,x1),(2,x2),(2,x3)], 3)
prop_normalizePBLinExactly :: Property
prop_normalizePBLinExactly = forAll g $ \(nv, c) ->
let c2 = SAT.normalizePBLinExactly c
in flip all (allAssignments nv) $ \m ->
SAT.evalPBLinExactly m c == SAT.evalPBLinExactly m c2
where
g :: Gen (Int, SAT.PBLinExactly)
g = do
nv <- choose (0, 10)
lhs <- forM [1..nv] $ \x -> do
c <- arbitrary
p <- arbitrary
return (c, SAT.literal x p)
rhs <- arbitrary
return (nv, (lhs,rhs))
prop_cutResolve :: Property
prop_cutResolve =
forAll (choose (1, 10)) $ \nv ->
forAll (g nv True) $ \c1 ->
forAll (g nv False) $ \c2 ->
let c3 = SAT.cutResolve c1 c2 1
in flip all (allAssignments nv) $ \m ->
not (SAT.evalPBLinExactly m c1 && SAT.evalPBLinExactly m c2) || SAT.evalPBLinExactly m c3
where
g :: Int -> Bool -> Gen SAT.PBLinExactly
g nv b = do
lhs <- forM [1..nv] $ \x -> do
if x==1 then do
c <- liftM ((1+) . abs) arbitrary
return (c, SAT.literal x b)
else do
c <- arbitrary
p <- arbitrary
return (c, SAT.literal x p)
rhs <- arbitrary
return (lhs, rhs)
case_cutResolve_1 :: Assertion
case_cutResolve_1 = (sort lhs, rhs) @?= (sort [(1,x3),(1,x4)], 1)
where
x1 = 1
x2 = 2
x3 = 3
x4 = 4
pb1 = ([(1,x1), (1,x2), (1,x3)], 1)
pb2 = ([(2,-x1), (2,-x2), (1,x4)], 3)
(lhs,rhs) = SAT.cutResolve pb1 pb2 x1
case_cutResolve_2 :: Assertion
case_cutResolve_2 = (sort lhs, rhs) @?= (sort lhs2, rhs2)
where
x1 = 1
x2 = 2
x3 = 3
x4 = 4
pb1 = ([(3,x1), (2,-x2), (1,x3), (1,x4)], 3)
pb2 = ([(1,-x3), (1,x4)], 1)
(lhs,rhs) = SAT.cutResolve pb1 pb2 x3
(lhs2,rhs2) = ([(2,x1),(1,-x2),(1,x4)],2) -- ([(3,x1),(2,-x2),(2,x4)], 3)
case_cardinalityReduction :: Assertion
case_cardinalityReduction = (sort lhs, rhs) @?= ([1,2,3,4,5],4)
where
(lhs, rhs) = SAT.cardinalityReduction ([(6,1),(5,2),(4,3),(3,4),(2,5),(1,6)], 17)
case_pbSubsume_clause :: Assertion
case_pbSubsume_clause = SAT.pbSubsume ([(1,1),(1,-3)],1) ([(1,1),(1,2),(1,-3),(1,4)],1) @?= True
case_pbSubsume_1 :: Assertion
case_pbSubsume_1 = SAT.pbSubsume ([(1,1),(1,2),(1,-3)],2) ([(1,1),(2,2),(1,-3),(1,4)],1) @?= True
case_pbSubsume_2 :: Assertion
case_pbSubsume_2 = SAT.pbSubsume ([(1,1),(1,2),(1,-3)],2) ([(1,1),(2,2),(1,-3),(1,4)],3) @?= False
------------------------------------------------------------------------
case_normalizeXORClause_False =
SAT.normalizeXORClause ([],True) @?= ([],True)
case_normalizeXORClause_True =
SAT.normalizeXORClause ([],False) @?= ([],False)
-- x ⊕ y ⊕ x = y
case_normalizeXORClause_case1 =
SAT.normalizeXORClause ([1,2,1],True) @?= ([2],True)
-- x ⊕ ¬x = x ⊕ x ⊕ 1 = 1
case_normalizeXORClause_case2 =
SAT.normalizeXORClause ([1,-1],True) @?= ([],False)
prop_normalizeXORClause :: Property
prop_normalizeXORClause = forAll g $ \(nv, c) ->
let c2 = SAT.normalizeXORClause c
in flip all (allAssignments nv) $ \m ->
SAT.evalXORClause m c == SAT.evalXORClause m c2
where
g :: Gen (Int, SAT.XORClause)
g = do
nv <- choose (0, 10)
len <- choose (0, nv)
lhs <- replicateM len $ choose (-nv, nv) `suchThat` (/= 0)
rhs <- arbitrary
return (nv, (lhs,rhs))
case_evalXORClause_case1 =
SAT.evalXORClause (array (1,2) [(1,True),(2,True)] :: Array Int Bool) ([1,2], True) @?= False
case_evalXORClause_case2 =
SAT.evalXORClause (array (1,2) [(1,False),(2,True)] :: Array Int Bool) ([1,2], True) @?= True
case_xor_case1 = do
solver <- SAT.newSolver
SAT.modifyConfig solver $ \config -> config{ SAT.configCheckModel = True }
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
SAT.addXORClause solver [x1, x2] True -- x1 ⊕ x2 = True
SAT.addXORClause solver [x2, x3] True -- x2 ⊕ x3 = True
SAT.addXORClause solver [x3, x1] True -- x3 ⊕ x1 = True
ret <- SAT.solve solver
ret @?= False
case_xor_case2 = do
solver <- SAT.newSolver
SAT.modifyConfig solver $ \config -> config{ SAT.configCheckModel = True }
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
SAT.addXORClause solver [x1, x2] True -- x1 ⊕ x2 = True
SAT.addXORClause solver [x1, x3] True -- x1 ⊕ x3 = True
SAT.addClause solver [x2]
ret <- SAT.solve solver
ret @?= True
m <- SAT.getModel solver
m ! x1 @?= False
m ! x2 @?= True
m ! x3 @?= True
case_xor_case3 = do
solver <- SAT.newSolver
SAT.modifyConfig solver $ \config -> config{ SAT.configCheckModel = True }
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- SAT.newVar solver
x4 <- SAT.newVar solver
SAT.addXORClause solver [x1,x2,x3,x4] True
SAT.addAtLeast solver [x1,x2,x3,x4] 2
ret <- SAT.solve solver
ret @?= True
------------------------------------------------------------------------
-- from "Pueblo: A Hybrid Pseudo-Boolean SAT Solver"
-- clauseがunitになるレベルで、PB制約が違反状態のままという例。
case_hybridLearning_1 :: Assertion
case_hybridLearning_1 = do
solver <- SAT.newSolver
[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11] <- replicateM 11 (SAT.newVar solver)
SAT.addClause solver [x11, x10, x9] -- C1
SAT.addClause solver [x8, x7, x6] -- C2
SAT.addClause solver [x5, x4, x3] -- C3
SAT.addAtLeast solver [-x2, -x5, -x8, -x11] 3 -- C4
SAT.addAtLeast solver [-x1, -x4, -x7, -x10] 3 -- C5
replicateM 3 (SAT.varBumpActivity solver x3)
SAT.setVarPolarity solver x3 False
replicateM 2 (SAT.varBumpActivity solver x6)
SAT.setVarPolarity solver x6 False
replicateM 1 (SAT.varBumpActivity solver x9)
SAT.setVarPolarity solver x9 False
SAT.setVarPolarity solver x1 True
SAT.modifyConfig solver $ \config -> config{ SAT.configLearningStrategy = SAT.LearningHybrid }
ret <- SAT.solve solver
ret @?= True
-- from "Pueblo: A Hybrid Pseudo-Boolean SAT Solver"
-- clauseがunitになるレベルで、PB制約が違反状態のままという例。
-- さらに、学習したPB制約はunitにはならない。
case_hybridLearning_2 :: Assertion
case_hybridLearning_2 = do
solver <- SAT.newSolver
[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12] <- replicateM 12 (SAT.newVar solver)
SAT.addClause solver [x11, x10, x9] -- C1
SAT.addClause solver [x8, x7, x6] -- C2
SAT.addClause solver [x5, x4, x3] -- C3
SAT.addAtLeast solver [-x2, -x5, -x8, -x11] 3 -- C4
SAT.addAtLeast solver [-x1, -x4, -x7, -x10] 3 -- C5
SAT.addClause solver [x12, -x3]
SAT.addClause solver [x12, -x6]
SAT.addClause solver [x12, -x9]
SAT.varBumpActivity solver x12
SAT.setVarPolarity solver x12 False
SAT.modifyConfig solver $ \config -> config{ SAT.configLearningStrategy = SAT.LearningHybrid }
ret <- SAT.solve solver
ret @?= True
-- regression test for the bug triggered by normalized-blast-floppy1-8.ucl.opb.bz2
case_addPBAtLeast_regression :: Assertion
case_addPBAtLeast_regression = do
solver <- SAT.newSolver
[x1,x2,x3,x4] <- replicateM 4 (SAT.newVar solver)
SAT.addClause solver [-x1]
SAT.addClause solver [-x2, -x3]
SAT.addClause solver [-x2, -x4]
SAT.addPBAtLeast solver [(1,x1),(2,x2),(1,x3),(1,x4)] 3
ret <- SAT.solve solver
ret @?= False
------------------------------------------------------------------------
case_addFormula = do
solver <- SAT.newSolver
enc <- Tseitin.newEncoder solver
[x1,x2,x3,x4,x5] <- replicateM 5 $ liftM Atom $ SAT.newVar solver
Tseitin.addFormula enc $ orB [x1 .=>. x3 .&&. x4, x2 .=>. x3 .&&. x5]
-- x6 = x3 ∧ x4
-- x7 = x3 ∧ x5
Tseitin.addFormula enc $ x1 .||. x2
Tseitin.addFormula enc $ x4 .=>. notB x5
ret <- SAT.solve solver
ret @?= True
Tseitin.addFormula enc $ x2 .<=>. x4
ret <- SAT.solve solver
ret @?= True
Tseitin.addFormula enc $ x1 .<=>. x5
ret <- SAT.solve solver
ret @?= True
Tseitin.addFormula enc $ notB x1 .=>. x3 .&&. x5
ret <- SAT.solve solver
ret @?= True
Tseitin.addFormula enc $ notB x2 .=>. x3 .&&. x4
ret <- SAT.solve solver
ret @?= False
case_addFormula_Peirces_Law = do
solver <- SAT.newSolver
enc <- Tseitin.newEncoder solver
[x1,x2] <- replicateM 2 $ liftM Atom $ SAT.newVar solver
Tseitin.addFormula enc $ notB $ ((x1 .=>. x2) .=>. x1) .=>. x1
ret <- SAT.solve solver
ret @?= False
case_encodeConj = do
solver <- SAT.newSolver
enc <- Tseitin.newEncoder solver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- Tseitin.encodeConj enc [x1,x2]
ret <- SAT.solveWith solver [x3]
ret @?= True
m <- SAT.getModel solver
SAT.evalLit m x1 @?= True
SAT.evalLit m x2 @?= True
SAT.evalLit m x3 @?= True
ret <- SAT.solveWith solver [-x3]
ret @?= True
m <- SAT.getModel solver
(SAT.evalLit m x1 && SAT.evalLit m x2) @?= False
SAT.evalLit m x3 @?= False
case_encodeDisj = do
solver <- SAT.newSolver
enc <- Tseitin.newEncoder solver
x1 <- SAT.newVar solver
x2 <- SAT.newVar solver
x3 <- Tseitin.encodeDisj enc [x1,x2]
ret <- SAT.solveWith solver [x3]
ret @?= True
m <- SAT.getModel solver
(SAT.evalLit m x1 || SAT.evalLit m x2) @?= True
SAT.evalLit m x3 @?= True
ret <- SAT.solveWith solver [-x3]
ret @?= True
m <- SAT.getModel solver
SAT.evalLit m x1 @?= False
SAT.evalLit m x2 @?= False
SAT.evalLit m x3 @?= False
case_evalFormula = do
solver <- SAT.newSolver
xs <- SAT.newVars solver 5
let f = (x1 .=>. x3 .&&. x4) .||. (x2 .=>. x3 .&&. x5)
where
[x1,x2,x3,x4,x5] = map Atom xs
g :: SAT.Model -> Bool
g m = (not x1 || (x3 && x4)) || (not x2 || (x3 && x5))
where
[x1,x2,x3,x4,x5] = elems m
forM_ (allAssignments 5) $ \m -> do
Tseitin.evalFormula m f @?= g m
prop_PBEncoder_addPBAtLeast = QM.monadicIO $ do
let nv = 4
(lhs,rhs) <- QM.pick $ do
lhs <- arbitraryPBLinSum nv
rhs <- arbitrary
return $ SAT.normalizePBLinAtLeast (lhs, rhs)
strategy <- QM.pick arbitrary
(cnf,defs) <- QM.run $ do
db <- CNFStore.newCNFStore
SAT.newVars_ db nv
tseitin <- Tseitin.newEncoder db
pb <- PB.newEncoderWithStrategy tseitin strategy
SAT.addPBAtLeast pb lhs rhs
cnf <- CNFStore.getCNFFormula db
defs <- Tseitin.getDefinitions tseitin
return (cnf, defs)
forM_ (allAssignments 4) $ \m -> do
let m2 :: Array SAT.Var Bool
m2 = array (1, CNF.numVars cnf) $ assocs m ++ [(v, Tseitin.evalFormula m2 phi) | (v,phi) <- defs]
b1 = SAT.evalPBLinAtLeast m (lhs,rhs)
b2 = evalCNF (array (bounds m2) (assocs m2)) cnf
QM.assert $ b1 == b2
prop_PBEncoder_Sorter_genSorter :: [Int] -> Bool
prop_PBEncoder_Sorter_genSorter xs =
V.toList (PBEncSorter.sortVector (V.fromList xs)) == sort xs
prop_PBEncoder_Sorter_decode_encode :: Property
prop_PBEncoder_Sorter_decode_encode =
forAll arbitrary $ \base' ->
forAll arbitrary $ \(NonNegative x) ->
let base = [b | Positive b <- base']
in PBEncSorter.isRepresentable base x
==>
(PBEncSorter.decode base . PBEncSorter.encode base) x == x
------------------------------------------------------------------------
findMUSAssumptions_case1 :: MUS.Method -> IO ()
findMUSAssumptions_case1 method = do
solver <- SAT.newSolver
[x1,x2,x3] <- SAT.newVars solver 3
sels@[y1,y2,y3,y4,y5,y6] <- SAT.newVars solver 6
SAT.addClause solver [-y1, x1]
SAT.addClause solver [-y2, -x1]
SAT.addClause solver [-y3, -x1, x2]
SAT.addClause solver [-y4, -x2]
SAT.addClause solver [-y5, -x1, x3]
SAT.addClause solver [-y6, -x3]
ret <- SAT.solveWith solver sels
ret @?= False
actual <- MUS.findMUSAssumptions solver def{ MUS.optMethod = method }
let actual' = IntSet.map (\x -> x-3) actual
expected = map IntSet.fromList [[1, 2], [1, 3, 4], [1, 5, 6]]
actual' `elem` expected @?= True
case_findMUSAssumptions_Deletion = findMUSAssumptions_case1 MUS.Deletion
case_findMUSAssumptions_Insertion = findMUSAssumptions_case1 MUS.Insertion
case_findMUSAssumptions_QuickXplain = findMUSAssumptions_case1 MUS.QuickXplain
------------------------------------------------------------------------
{-
c http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf
c φ= (x1) ∧ (¬x1) ∧ (¬x1∨x2) ∧ (¬x2) ∧ (¬x1∨x3) ∧ (¬x3)
c MUSes(φ) = {{C1, C2}, {C1, C3, C4}, {C1, C5, C6}}
c MCSes(φ) = {{C1}, {C2, C3, C5}, {C2, C3, C6}, {C2, C4, C5}, {C2, C4, C6}}
p cnf 3 6
1 0
-1 0
-1 2 0
-2 0
-1 3 0
-3 0
-}
allMUSAssumptions_case1 :: MUSEnum.Method -> IO ()
allMUSAssumptions_case1 method = do
solver <- SAT.newSolver
[x1,x2,x3] <- SAT.newVars solver 3
sels@[y1,y2,y3,y4,y5,y6] <- SAT.newVars solver 6
SAT.addClause solver [-y1, x1]
SAT.addClause solver [-y2, -x1]
SAT.addClause solver [-y3, -x1, x2]
SAT.addClause solver [-y4, -x2]
SAT.addClause solver [-y5, -x1, x3]
SAT.addClause solver [-y6, -x3]
(muses, mcses) <- MUSEnum.allMUSAssumptions solver sels def{ MUSEnum.optMethod = method }
Set.fromList muses @?= Set.fromList (map (IntSet.fromList . map (+3)) [[1,2], [1,3,4], [1,5,6]])
Set.fromList mcses @?= Set.fromList (map (IntSet.fromList . map (+3)) [[1], [2,3,5], [2,3,6], [2,4,5], [2,4,6]])
case_allMUSAssumptions_CAMUS = allMUSAssumptions_case1 MUSEnum.CAMUS
case_allMUSAssumptions_DAA = allMUSAssumptions_case1 MUSEnum.DAA
case_allMUSAssumptions_MARCO = allMUSAssumptions_case1 MUSEnum.MARCO
case_allMUSAssumptions_GurvichKhachiyan1999 = allMUSAssumptions_case1 MUSEnum.GurvichKhachiyan1999
{-
Boosting a Complete Technique to Find MSS and MUS thanks to a Local Search Oracle
http://www.cril.univ-artois.fr/~piette/IJCAI07_HYCAM.pdf
Example 3.
C0 : (d)
C1 : (b ∨ c)
C2 : (a ∨ b)
C3 : (a ∨ ¬c)
C4 : (¬b ∨ ¬e)
C5 : (¬a ∨ ¬b)
C6 : (a ∨ e)
C7 : (¬a ∨ ¬e)
C8 : (b ∨ e)
C9 : (¬a ∨ b ∨ ¬c)
C10 : (¬a ∨ b ∨ ¬d)
C11 : (a ∨ ¬b ∨ c)
C12 : (a ∨ ¬b ∨ ¬d)
-}
allMUSAssumptions_case2 :: MUSEnum.Method -> IO ()
allMUSAssumptions_case2 method = do
solver <- SAT.newSolver
[a,b,c,d,e] <- SAT.newVars solver 5
sels@[y0,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12] <- SAT.newVars solver 13
SAT.addClause solver [-y0, d]
SAT.addClause solver [-y1, b, c]
SAT.addClause solver [-y2, a, b]
SAT.addClause solver [-y3, a, -c]
SAT.addClause solver [-y4, -b, -e]
SAT.addClause solver [-y5, -a, -b]
SAT.addClause solver [-y6, a, e]
SAT.addClause solver [-y7, -a, -e]
SAT.addClause solver [-y8, b, e]
SAT.addClause solver [-y9, -a, b, -c]
SAT.addClause solver [-y10, -a, b, -d]
SAT.addClause solver [-y11, a, -b, c]
SAT.addClause solver [-y12, a, -b, -d]
-- Only three of the MUSes (marked with asterisks) are on the paper.
let cores =
[ [y0,y1,y2,y5,y9,y12]
, [y0,y1,y3,y4,y5,y6,y10]
, [y0,y1,y3,y5,y7,y8,y12]
, [y0,y1,y3,y5,y9,y12]
, [y0,y1,y3,y5,y10,y11]
, [y0,y1,y3,y5,y10,y12]
, [y0,y2,y3,y5,y10,y11]
, [y0,y2,y4,y5,y6,y10]
, [y0,y2,y5,y7,y8,y12]
, [y0,y2,y5,y10,y12] -- (*)
, [y1,y2,y4,y5,y6,y9]
, [y1,y3,y4,y5,y6,y7,y8]
, [y1,y3,y4,y5,y6,y9]
, [y1,y3,y5,y7,y8,y11]
, [y1,y3,y5,y9,y11] -- (*)
, [y2,y3,y5,y7,y8,y11]
, [y2,y4,y5,y6,y7,y8] -- (*)
]
let remove1 :: [a] -> [[a]]
remove1 [] = []
remove1 (x:xs) = xs : [x : ys | ys <- remove1 xs]
forM_ cores $ \core -> do
ret <- SAT.solveWith solver core
assertBool (show core ++ " should be a core") (not ret)
forM (remove1 core) $ \xs -> do
ret <- SAT.solveWith solver xs
assertBool (show core ++ " should be satisfiable") ret
(actual,_) <- MUSEnum.allMUSAssumptions solver sels def{ MUSEnum.optMethod = method }
let actual' = Set.fromList actual
expected' = Set.fromList $ map IntSet.fromList $ cores
actual' @?= expected'
case_allMUSAssumptions_2_CAMUS = allMUSAssumptions_case2 MUSEnum.CAMUS
case_allMUSAssumptions_2_DAA = allMUSAssumptions_case2 MUSEnum.DAA
case_allMUSAssumptions_2_MARCO = allMUSAssumptions_case2 MUSEnum.MARCO
case_allMUSAssumptions_2_GurvichKhachiyan1999 = allMUSAssumptions_case2 MUSEnum.GurvichKhachiyan1999
case_allMUSAssumptions_2_HYCAM = do
solver <- SAT.newSolver
[a,b,c,d,e] <- SAT.newVars solver 5
sels@[y0,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12] <- SAT.newVars solver 13
SAT.addClause solver [-y0, d]
SAT.addClause solver [-y1, b, c]
SAT.addClause solver [-y2, a, b]
SAT.addClause solver [-y3, a, -c]
SAT.addClause solver [-y4, -b, -e]
SAT.addClause solver [-y5, -a, -b]
SAT.addClause solver [-y6, a, e]
SAT.addClause solver [-y7, -a, -e]
SAT.addClause solver [-y8, b, e]
SAT.addClause solver [-y9, -a, b, -c]
SAT.addClause solver [-y10, -a, b, -d]
SAT.addClause solver [-y11, a, -b, c]
SAT.addClause solver [-y12, a, -b, -d]
-- Only three of the MUSes (marked with asterisks) are on the paper.
let cores =
[ [y0,y1,y2,y5,y9,y12]
, [y0,y1,y3,y4,y5,y6,y10]
, [y0,y1,y3,y5,y7,y8,y12]
, [y0,y1,y3,y5,y9,y12]
, [y0,y1,y3,y5,y10,y11]
, [y0,y1,y3,y5,y10,y12]
, [y0,y2,y3,y5,y10,y11]
, [y0,y2,y4,y5,y6,y10]
, [y0,y2,y5,y7,y8,y12]
, [y0,y2,y5,y10,y12] -- (*)
, [y1,y2,y4,y5,y6,y9]
, [y1,y3,y4,y5,y6,y7,y8]
, [y1,y3,y4,y5,y6,y9]
, [y1,y3,y5,y7,y8,y11]
, [y1,y3,y5,y9,y11] -- (*)
, [y2,y3,y5,y7,y8,y11]
, [y2,y4,y5,y6,y7,y8] -- (*)
]
mcses =
[ [y0,y1,y7]
, [y0,y1,y8]
, [y0,y3,y4]
, [y0,y3,y6]
, [y0,y4,y11]
, [y0,y6,y11]
, [y0,y7,y9]
, [y0,y8,y9]
, [y1,y2]
, [y1,y7,y10]
, [y1,y8,y10]
, [y2,y3]
, [y3,y4,y12]
, [y3,y6,y12]
, [y4,y11,y12]
, [y5]
, [y6,y11,y12]
, [y7,y9,y10]
, [y8,y9,y10]
]
-- HYCAM paper wrongly treated {C3,C8,C10} as a candidate MCS (CoMSS).
-- Its complement {C0,C1,C2,C4,C5,C6,C7,C9,C11,C12} is unsatisfiable
-- and hence not MSS.
ret <- SAT.solveWith solver [y0,y1,y2,y4,y5,y6,y7,y9,y11,y12]
assertBool "failed to prove the bug of HYCAM paper" (not ret)
let cand = map IntSet.fromList [[y5], [y3,y2], [y0,y1,y2]]
(actual,_) <- MUSEnum.allMUSAssumptions solver sels def{ MUSEnum.optMethod = MUSEnum.CAMUS, MUSEnum.optKnownCSes = cand }
let actual' = Set.fromList $ actual
expected' = Set.fromList $ map IntSet.fromList cores
actual' @?= expected'
------------------------------------------------------------------------
prop_ExistentialQuantification :: Property
prop_ExistentialQuantification = QM.monadicIO $ do
phi <- QM.pick arbitraryCNF
xs <- QM.pick $ liftM IntSet.fromList $ sublistOf [1 .. CNF.numVars phi]
let ys = IntSet.fromList [1 .. CNF.numVars phi] IntSet.\\ xs
psi <- QM.run $ ExistentialQuantification.project xs phi
forM_ (replicateM (IntSet.size ys) [False,True]) $ \bs -> do
let m :: SAT.Model
m = array (1, if IntSet.null ys then 0 else IntSet.findMax ys) (zip (IntSet.toList ys) bs)
b1 <- QM.run $ do
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.numVars phi)
forM_ (CNF.clauses phi) $ \c -> SAT.addClause solver c
SAT.solveWith solver [if SAT.evalLit m y then y else -y | y <- IntSet.toList ys]
let b2 = evalCNF m psi
QM.assert $ b1 == b2
brauer11_phi :: CNF.CNF
brauer11_phi =
CNF.CNF
{ CNF.numVars = 13
, CNF.numClauses = 23
, CNF.clauses =
[
-- μ
[-x2, -y2]
, [-y2, -y1]
, [-x4, -x6, y1]
, [-x3, y4], [x3, -y4]
, [-x4, y3], [x4, -y3]
, [-x5, y6], [x5, -y6]
, [-x6, y5], [x6, -y5]
-- ξ
, [-x13, x1]
, [-x13, -x2]
, [-x13, x3]
, [-x13, -x4]
, [-x13, x5]
, [-x13, -x6]
, [x13, x1]
, [x13, -x2]
, [x13, -x3]
, [x13, x4]
, [x13, -x5]
, [x13, x6]
]
}
where
[y1,y2,y3,y4,y5,y6] = [1..6]
[x1,x2,x3,x4,x5,x6,x13] = [7..13]
{-
ξ(m'1) = (¬y1 ∧ ¬y3 ∧ y4 ∧ ¬y5 ∧ y6)
ξ(m'2) = (y1 ∧ ¬y2 ∧ ¬y3 ∧ y4 ∧ ¬y5 ∧ y6)
ξ(m'3) = (y1 ∧ ¬y2 ∧ y3 ∧ ¬y4 ∧ y5 ∧ ¬y6)
ω = ¬(ξ(m'1) ∨ ξ(m'2) ∨ ξ(m'3))
-}
brauer11_omega :: CNF.CNF
brauer11_omega =
CNF.CNF
{ CNF.numVars = 6
, CNF.numClauses = 3
, CNF.clauses =
[ [y1, y3, -y4, y5, -y6]
, [-y1, y2, y3, -y4, y5, -y6]
, [-y1, y2, -y3, y4, -y5, y6]
]
}
where
[y1,y2,y3,y4,y5,y6] = [1..6]
case_ExistentialQuantification_project_phi :: Assertion
case_ExistentialQuantification_project_phi = do
psi <- ExistentialQuantification.project (IntSet.fromList [7..13]) brauer11_phi
forM_ (replicateM 6 [False,True]) $ \bs -> do
let m :: SAT.Model
m = array (1,13) (zip [1..] bs)
b1 <- do
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.numVars brauer11_phi)
forM_ (CNF.clauses brauer11_phi) $ \c -> SAT.addClause solver c
SAT.solveWith solver [if SAT.evalLit m y then y else -y | y <- [1..6]]
let b2 = all (SAT.evalClause m) (CNF.clauses psi)
(b1 == b2) @?= True
case_ExistentialQuantification_project_phi' :: Assertion
case_ExistentialQuantification_project_phi' = do
let [y1,y2,y3,y4,y5,y6] = [1..6]
psi = CNF.CNF
{ CNF.numVars = 6
, CNF.numClauses = 8
, CNF.clauses =
[ [-y2, y6]
, [-y3, -y6]
, [y5, y6]
, [y3, -y5]
, [y4, -y6]
, [y1, y6]
, [-y1, -y2]
, [-y4, y6]
]
}
forM_ (replicateM 6 [False,True]) $ \bs -> do
let m :: SAT.Model
m = array (1,13) (zip [1..] bs)
b1 <- do
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.numVars brauer11_phi)
forM_ (CNF.clauses brauer11_phi) $ \c -> SAT.addClause solver c
SAT.solveWith solver [if SAT.evalLit m y then y else -y | y <- [1..6]]
let b2 = all (SAT.evalClause m) (CNF.clauses psi)
(b1 == b2) @?= True
case_shortestImplicants_phi :: Assertion
case_shortestImplicants_phi = do
xss <- ExistentialQuantification.shortestImplicants (IntSet.fromList [1..6]) brauer11_phi
forM_ (replicateM 6 [False,True]) $ \bs -> do
let m :: SAT.Model
m = array (1,6) (zip [1..] bs)
b1 <- do
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.numVars brauer11_phi)
forM_ (CNF.clauses brauer11_phi) $ \c -> SAT.addClause solver c
SAT.solveWith solver [if SAT.evalLit m y then y else -y | y <- [1..6]]
let b2 = any (all (SAT.evalLit m) . IntSet.toList) xss
(b1 == b2) @?= True
case_shortestImplicants_phi' :: Assertion
case_shortestImplicants_phi' = do
let [y1,y2,y3,y4,y5,y6] = [1..6]
xss = map IntSet.fromList
[ [-y1, -y3, y4, -y5, y6]
, [y1, -y2, -y3, y4, -y5, y6]
, [y1, -y2, y3, -y4, y5, -y6]
]
forM_ (replicateM 6 [False,True]) $ \bs -> do
let m :: SAT.Model
m = array (1,6) (zip [1..] bs)
b1 <- do
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.numVars brauer11_phi)
forM_ (CNF.clauses brauer11_phi) $ \c -> SAT.addClause solver c
SAT.solveWith solver [if SAT.evalLit m y then y else -y | y <- [1..6]]
let b2 = any (all (SAT.evalLit m) . IntSet.toList) xss
(b1 == b2) @?= True
case_shortestImplicants_omega :: Assertion
case_shortestImplicants_omega = do
xss <- ExistentialQuantification.shortestImplicants (IntSet.fromList [1..6]) brauer11_omega
forM_ (replicateM 6 [False,True]) $ \bs -> do
let m :: SAT.Model
m = array (1,6) (zip [1..] bs)
b1 <- do
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.numVars brauer11_omega)
forM_ (CNF.clauses brauer11_omega) $ \c -> SAT.addClause solver c
SAT.solveWith solver [if SAT.evalLit m y then y else -y | y <- [1..6]]
let b2 = any (all (SAT.evalLit m) . IntSet.toList) xss
unless (b1 == b2) $ print m
case_shortestImplicants_omega' :: Assertion
case_shortestImplicants_omega' = do
let [y1,y2,y3,y4,y5,y6] = [1..6]
xss = map IntSet.fromList
[ [y2, -y6]
, [y3, y6]
, [-y5, -y6]
, [-y3, y5]
, [-y4, y6]
, [-y1, -y6]
, [y1, y2]
, [y4, -y6]
]
forM_ (replicateM 6 [False,True]) $ \bs -> do
let m :: SAT.Model
m = array (1,6) (zip [1..] bs)
b1 <- do
solver <- SAT.newSolver
SAT.newVars_ solver (CNF.numVars brauer11_omega)
forM_ (CNF.clauses brauer11_omega) $ \c -> SAT.addClause solver c
SAT.solveWith solver [if SAT.evalLit m y then y else -y | y <- [1..6]]
let b2 = any (all (SAT.evalLit m) . IntSet.toList) xss
(b1 == b2) @?= True
------------------------------------------------------------------------
prop_pb2sat :: Property
prop_pb2sat = QM.monadicIO $ do
pb@(nv,cs) <- QM.pick arbitraryPB
let f (PBRelGE,lhs,rhs) = ([(c,[l]) | (c,l) <- lhs], PBFile.Ge, rhs)
f (PBRelLE,lhs,rhs) = ([(-c,[l]) | (c,l) <- lhs], PBFile.Ge, -rhs)
f (PBRelEQ,lhs,rhs) = ([(c,[l]) | (c,l) <- lhs], PBFile.Eq, rhs)
let opb = PBFile.Formula
{ PBFile.pbObjectiveFunction = Nothing
, PBFile.pbNumVars = nv
, PBFile.pbNumConstraints = length cs
, PBFile.pbConstraints = map f cs
}
let (cnf, mforth, mback) = PB2SAT.convert opb
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
ret1 <- QM.run $ solvePB solver1 pb
ret2 <- QM.run $ solveCNF solver2 cnf
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just m1 -> do
let m2 = mforth m1
QM.assert $ bounds m2 == (1, CNF.numVars cnf)
QM.assert $ evalCNF m2 cnf
case ret2 of
Nothing -> return ()
Just m2 -> do
let m1 = mback m2
QM.assert $ bounds m1 == (1, nv)
QM.assert $ evalPB m1 pb
prop_wbo2maxsat :: Property
prop_wbo2maxsat = QM.monadicIO $ do
wbo1@(nv,cs,top) <- QM.pick arbitraryWBO
let f (w,(PBRelGE,lhs,rhs)) = (w,([(c,[l]) | (c,l) <- lhs], PBFile.Ge, rhs))
f (w,(PBRelLE,lhs,rhs)) = (w,([(-c,[l]) | (c,l) <- lhs], PBFile.Ge, -rhs))
f (w,(PBRelEQ,lhs,rhs)) = (w,([(c,[l]) | (c,l) <- lhs], PBFile.Eq, rhs))
let wbo1' = PBFile.SoftFormula
{ PBFile.wboNumVars = nv
, PBFile.wboNumConstraints = length cs
, PBFile.wboConstraints = map f cs
, PBFile.wboTopCost = top
}
let (wcnf, mforth, mback) = WBO2MaxSAT.convert wbo1'
wbo2 = ( MaxSAT.numVars wcnf
, [ ( if w == MaxSAT.topCost wcnf then Nothing else Just w
, (PBRelGE, [(1,l) | l <- clause], 1)
)
| (w,clause) <- MaxSAT.clauses wcnf
]
, Nothing
)
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
method <- QM.pick arbitrary
ret1 <- QM.run $ optimizeWBO solver1 method wbo1
ret2 <- QM.run $ optimizeWBO solver2 method wbo2
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just (m1,val) -> do
let m2 = mforth m1
QM.assert $ bounds m2 == (1, MaxSAT.numVars wcnf)
QM.assert $ evalWBO m2 wbo2 == Just val
case ret2 of
Nothing -> return ()
Just (m2,val) -> do
let m1 = mback m2
QM.assert $ bounds m1 == (1, nv)
QM.assert $ evalWBO m1 wbo1 == Just val
prop_wbo2pb :: Property
prop_wbo2pb = QM.monadicIO $ do
wbo@(nv,cs,top) <- QM.pick arbitraryWBO
let f (w,(PBRelGE,lhs,rhs)) = (w,([(c,[l]) | (c,l) <- lhs], PBFile.Ge, rhs))
f (w,(PBRelLE,lhs,rhs)) = (w,([(-c,[l]) | (c,l) <- lhs], PBFile.Ge, -rhs))
f (w,(PBRelEQ,lhs,rhs)) = (w,([(c,[l]) | (c,l) <- lhs], PBFile.Eq, rhs))
let wbo' = PBFile.SoftFormula
{ PBFile.wboNumVars = nv
, PBFile.wboNumConstraints = length cs
, PBFile.wboConstraints = map f cs
, PBFile.wboTopCost = top
}
let (opb, mforth, mback) = WBO2PB.convert wbo'
obj = fromMaybe [] $ PBFile.pbObjectiveFunction opb
f (lhs, PBFile.Ge, rhs) = (PBRelGE, lhs, rhs)
f (lhs, PBFile.Eq, rhs) = (PBRelEQ, lhs, rhs)
cs2 = map f (PBFile.pbConstraints opb)
pb = (PBFile.pbNumVars opb, obj, cs2)
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
method <- QM.pick arbitrary
ret1 <- QM.run $ optimizeWBO solver1 method wbo
ret2 <- QM.run $ optimizePBNLC solver2 method pb
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just (m1,val1) -> do
let m2 = mforth m1
QM.assert $ bounds m2 == (1, PBFile.pbNumVars opb)
QM.assert $ evalPBNLC m2 (PBFile.pbNumVars opb, cs2)
QM.assert $ SAT.evalPBSum m2 obj == val1
case ret2 of
Nothing -> return ()
Just (m2,val2) -> do
let m1 = mback m2
QM.assert $ bounds m1 == (1,nv)
QM.assert $ evalWBO m1 wbo == Just val2
prop_sat2ksat :: Property
prop_sat2ksat = QM.monadicIO $ do
k <- QM.pick $ choose (3,10)
cnf1 <- QM.pick arbitraryCNF
let (cnf2, mforth, mback) = SAT2KSAT.convert k cnf1
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
ret1 <- QM.run $ solveCNF solver1 cnf1
ret2 <- QM.run $ solveCNF solver2 cnf2
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just m1 -> do
let m2 = mforth m1
QM.assert $ bounds m2 == (1, CNF.numVars cnf2)
QM.assert $ evalCNF m2 cnf2
case ret2 of
Nothing -> return ()
Just m2 -> do
let m1 = mback m2
QM.assert $ bounds m1 == (1, CNF.numVars cnf1)
QM.assert $ evalCNF m1 cnf1
------------------------------------------------------------------------
instance Arbitrary SAT.LearningStrategy where
arbitrary = arbitraryBoundedEnum
instance Arbitrary SAT.RestartStrategy where
arbitrary = arbitraryBoundedEnum
instance Arbitrary SAT.BranchingStrategy where
arbitrary = arbitraryBoundedEnum
instance Arbitrary SAT.PBHandlerType where
arbitrary = arbitraryBoundedEnum
instance Arbitrary SAT.Config where
arbitrary = do
restartStrategy <- arbitrary
restartFirst <- arbitrary
restartInc <- liftM ((1.01 +) . abs) arbitrary
learningStrategy <- arbitrary
learntSizeFirst <- arbitrary
learntSizeInc <- liftM ((1.01 +) . abs) arbitrary
branchingStrategy <- arbitrary
erwaStepSizeFirst <- choose (0, 1)
erwaStepSizeMin <- choose (0, 1)
erwaStepSizeDec <- choose (0, 1)
pbhandler <- arbitrary
ccmin <- choose (0,2)
phaseSaving <- arbitrary
forwardSubsumptionRemoval <- arbitrary
backwardSubsumptionRemoval <- arbitrary
randomFreq <- choose (0,1)
splitClausePart <- arbitrary
return $ def
{ SAT.configRestartStrategy = restartStrategy
, SAT.configRestartFirst = restartFirst
, SAT.configRestartInc = restartInc
, SAT.configLearningStrategy = learningStrategy
, SAT.configLearntSizeFirst = learntSizeFirst
, SAT.configLearntSizeInc = learntSizeInc
, SAT.configPBHandlerType = pbhandler
, SAT.configCCMin = ccmin
, SAT.configBranchingStrategy = branchingStrategy
, SAT.configERWAStepSizeFirst = erwaStepSizeFirst
, SAT.configERWAStepSizeDec = erwaStepSizeDec
, SAT.configERWAStepSizeMin = erwaStepSizeMin
, SAT.configEnablePhaseSaving = phaseSaving
, SAT.configEnableForwardSubsumptionRemoval = forwardSubsumptionRemoval
, SAT.configEnableBackwardSubsumptionRemoval = backwardSubsumptionRemoval
, SAT.configRandomFreq = randomFreq
, SAT.configEnablePBSplitClausePart = splitClausePart
}
arbitrarySolver :: QM.PropertyM IO SAT.Solver
arbitrarySolver = do
seed <- QM.pick arbitrary
config <- QM.pick arbitrary
QM.run $ do
solver <- SAT.newSolverWithConfig config{ SAT.configCheckModel = True }
SAT.setRandomGen solver =<< Rand.initialize (V.singleton seed)
return solver
arbitraryOptimizer :: SAT.Solver -> SAT.PBLinSum -> QM.PropertyM IO PBO.Optimizer
arbitraryOptimizer solver obj = do
method <- QM.pick arbitrary
QM.run $ do
opt <- PBO.newOptimizer solver obj
PBO.setMethod opt method
return opt
instance Arbitrary PBO.Method where
arbitrary = arbitraryBoundedEnum
instance Arbitrary PB.Strategy where
arbitrary = arbitraryBoundedEnum
-- ---------------------------------------------------------------------
#if !MIN_VERSION_QuickCheck(2,8,0)
sublistOf :: [a] -> Gen [a]
sublistOf xs = filterM (\_ -> choose (False, True)) xs
#endif
------------------------------------------------------------------------
-- Test harness
satTestGroup :: TestTree
satTestGroup = $(testGroupGenerator)